Reduction to primitive sets

erdos-402--h2-v2

proved

Hole h2 of erdos-402 (split by 20260917T141927Z-calib-402-f480-partial.lean).

Revises erdos-402--h2, which it replaced (D-8).

$\displaystyle \Bigl(\forall B \subset \mathbb{N}\ \text{finite}:\ 0 \notin B,\ |B| = |A|,\ \gcd(B) = 1 \Rightarrow \exists\, a, b \in B:\ \gcd(a,b) \le \tfrac{a}{|B|}\Bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

Assuming the Farey-structure claim as a hypothesis (for every finite A ⊂ ℕ with 0 ∉ A and every m, a ≤ m·gcd(a, b) for all a, b ∈ A implies that each pair has a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ m): for every finite nonempty A ⊂ ℕ with 0 ∉ A, if the bound holds for every set B of the same size whose elements have greatest common divisor 1, then it holds for A. gcd(B) is the greatest common divisor of all elements of B, both divisions are in ℚ, and a and b may coincide.

unverified · history

Lean

theorem erdos_402__h2 : (∀ (A : Finset ℕ) (m : ℕ),
    0 ∉ A →
      (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
        ∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u) →
  ∀ (A : Finset ℕ),
    0 ∉ A →
      A.Nonempty →
        (∀ (B : Finset ℕ), 0 ∉ B → B.card = A.card → B.gcd id = 1 → ∃ a ∈ B, ∃ b ∈ B, a.gcd b ≤ (a / B.card : ℚ)) →
          ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  sorry

Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000136, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000136.json, merge commit 90702603d49f.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

s1 obtain A.Nonempty
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A.
Lean, line 18
```
  obtain ⟨x, hx⟩ := hne
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 18 at 90702603d49f ↗
hx0 have x ≠ (0 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hx0 : x ≠ (0 : ℕ).
Uses library ne_of_mem_of_not_mem.
Lean, line 19
```
  have hx0 : x ≠ 0 := ne_of_mem_of_not_mem hx hA
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 19 at 90702603d49f ↗
hgdvd have ∀ a ∈ A, A.gcd id ∣ a
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgdvd : ∀ a ∈ A, A.gcd id ∣ a.
Uses library id, Finset.gcd_dvd.
Lean, line 20
```
  have hgdvd : ∀ a ∈ A, A.gcd id ∣ a := fun a ha => Finset.gcd_dvd (f := id) ha
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 20 at 90702603d49f ↗
hg0 have A.gcd id ≠ (0 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hg0 : A.gcd id ≠ (0 : ℕ).
Uses library id, Nat.eq_zero_of_zero_dvd.
Lean, lines 21–25
```
  have hg0 : A.gcd id ≠ 0 := by
    intro h0
    have h1 := hgdvd x hx
    rw [h0] at h1
    exact hx0 (Nat.eq_zero_of_zero_dvd h1)
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 21–25 at 90702603d49f ↗
1. hg0.h1 have A.gcd id ∣ x
  Leaves False, with h1 : A.gcd id ∣ x.
  Lean, line 23
  have h1 := hgdvd x hx
  targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 23 at 90702603d49f ↗
hgpos have (0 : ℕ) < A.gcd id
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgpos : (0 : ℕ) < A.gcd id.
Uses library id, Nat.pos_of_ne_zero.
Lean, line 26
```
  have hgpos : 0 < A.gcd id := Nat.pos_of_ne_zero hg0
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 26 at 90702603d49f ↗
hB0 have (0 : ℕ) ∉ Finset.image (fun (a : ℕ) => a / A.gcd id) A
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hB0 : (0 : ℕ) ∉ Finset.image (fun (a : ℕ) => a / A.gcd id) A.
Uses library id, MulZeroClass.mul_zero.
Lean, lines 27–37
```
  have hB0 : 0 ∉ A.image (fun a => a / A.gcd id) := by
    intro h
    obtain ⟨a, ha, hag⟩ := Finset.mem_image.mp h
    have ha0 : a ≠ 0 := ne_of_mem_of_not_mem ha hA
    obtain ⟨k, hk⟩ := hgdvd a ha
    have hk0 : k = 0 := by
      have h2 : a / A.gcd id = k := by
        conv_lhs => rw [hk]
        exact Nat.mul_div_cancel_left _ hgpos
      rw [← h2]; exact hag
    exact ha0 (by rw [hk, hk0, mul_zero])
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 27–37 at 90702603d49f ↗
1. hB0.s1 obtain ∃ a ∈ A, a / A.gcd id = (0 : ℕ)
  Leaves False, with a : ℕ, ha : a ∈ A, hag : a / A.gcd id = (0 : ℕ).
  Uses library Finset.mem_image.
  Lean, line 29
  obtain ⟨a, ha, hag⟩ := Finset.mem_image.mp h
  targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 29 at 90702603d49f ↗
2. hB0.ha0 have a ≠ (0 : ℕ)
  Leaves False, with ha0 : a ≠ (0 : ℕ).
  Uses library ne_of_mem_of_not_mem.
  Lean, line 30
  have ha0 : a ≠ 0 := ne_of_mem_of_not_mem ha hA
  targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 30 at 90702603d49f ↗
3. hB0.s3 obtain A.gcd id ∣ a
  Leaves False, with k : ℕ, hk : a = A.gcd id * k.
  Lean, line 31
  obtain ⟨k, hk⟩ := hgdvd a ha
  targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 31 at 90702603d49f ↗
4. hB0.hk0 have k = (0 : ℕ)
  Leaves False, with hk0 : k = (0 : ℕ).
  Lean, lines 32–36
  have hk0 : k = 0 := by have h2 : a / A.gcd id = k := by conv_lhs => rw [hk] exact Nat.mul_div_cancel_left _ hgpos rw [← h2]; exact hag
  targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 32–36 at 90702603d49f ↗
  hB0.hk0.h2 have a / A.gcd id = k
  Leaves k = (0 : ℕ), with h2 : a / A.gcd id = k.
  Uses library id, Nat.mul_div_cancel_left.
  Lean, lines 33–35
  have h2 : a / A.gcd id = k := by conv_lhs => rw [hk] exact Nat.mul_div_cancel_left _ hgpos
  targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 33–35 at 90702603d49f ↗
hcard have (Finset.image (fun (a : ℕ) => a / A.gcd id) A).card = A.card
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcard : (Finset.image (fun (a : ℕ) => a / A.gcd id) A).card = A.card.
Uses library id, Finset.card_image_of_injOn, Nat.div_left_inj.
Lean, lines 38–41
```
  have hcard : (A.image (fun a => a / A.gcd id)).card = A.card := by
    apply Finset.card_image_of_injOn
    intro a ha b hb hab
    exact (Nat.div_left_inj (hgdvd a ha) (hgdvd b hb)).mp hab
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 38–41 at 90702603d49f ↗
hgcd have (Finset.image (fun (a : ℕ) => a / A.gcd id) A).gcd id = (1 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgcd : (Finset.image (fun (a : ℕ) => a / A.gcd id) A).gcd id = (1 : ℕ).
Uses library id, Finset.gcd_image, Finset.gcd_div_id_eq_one.
Lean, lines 42–44
```
  have hgcd : (A.image (fun a => a / A.gcd id)).gcd id = 1 := by
    rw [Finset.gcd_image]
    exact Finset.gcd_div_id_eq_one hx hx0
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 42–44 at 90702603d49f ↗
s9 obtain ∃ a ∈ Finset.image (fun (a : ℕ) => a / A.gcd id) A, ∃ b ∈ Finset.image (fun (a : ℕ) => a / A.gcd id) A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑(Finset.image (fun (a : ℕ) => a / A.gcd id) A).card : ℚ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with a' : ℕ, ha' : a' ∈ Finset.image (fun (a : ℕ) => a / A.gcd id) A, b' : ℕ, hb' : b' ∈ Finset.image (fun (a : ℕ) => a / A.gcd id) A, hab : (↑(a'.gcd b') : ℚ) ≤ (↑a' : ℚ) / (↑(Finset.image (fun (a : ℕ) => a / A.gcd id) A).card : ℚ).
Lean, line 45
```
  obtain ⟨a', ha', b', hb', hab⟩ := hprim _ hB0 hcard hgcd
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 45 at 90702603d49f ↗
s10 obtain ∃ a ∈ A, a / A.gcd id = a'
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with a : ℕ, ha : a ∈ A, ha' : a / A.gcd id ∈ Finset.image (fun (a : ℕ) => a / A.gcd id) A, hab : (↑((a / A.gcd id).gcd b') : ℚ) ≤ (↑(a / A.gcd id) : ℚ) / (↑(Finset.image (fun (a : ℕ) => a / A.gcd id) A).card : ℚ).
Uses library Finset.mem_image.
Lean, line 46
```
  obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp ha'
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 46 at 90702603d49f ↗
s11 obtain ∃ a ∈ A, a / A.gcd id = b'
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with b : ℕ, hb : b ∈ A, hb' : b / A.gcd id ∈ Finset.image (fun (a : ℕ) => a / A.gcd id) A, hab : (↑((a / A.gcd id).gcd (b / A.gcd id)) : ℚ) ≤ (↑(a / A.gcd id) : ℚ) / (↑(Finset.image (fun (a : ℕ) => a / A.gcd id) A).card : ℚ).
Uses library Finset.mem_image.
Lean, line 47
```
  obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hb'
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 47 at 90702603d49f ↗
s12 obtain A.gcd id ∣ a
Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with k : ℕ, hk : a = A.gcd id * k.
Lean, line 49
```
  obtain ⟨k, hk⟩ := hgdvd a ha
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 49 at 90702603d49f ↗
s13 obtain A.gcd id ∣ b
Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with l : ℕ, hl : b = A.gcd id * l.
Lean, line 50
```
  obtain ⟨l, hl⟩ := hgdvd b hb
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 50 at 90702603d49f ↗
e1 have a / A.gcd id = k
Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with e1 : a / A.gcd id = k.
Uses library id, Nat.mul_div_cancel_left.
Lean, lines 51–53
```
  have e1 : a / A.gcd id = k := by
    conv_lhs => rw [hk]
    exact Nat.mul_div_cancel_left _ hgpos
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 51–53 at 90702603d49f ↗
e2 have b / A.gcd id = l
Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with e2 : b / A.gcd id = l.
Uses library id, Nat.mul_div_cancel_left.
Lean, lines 54–56
```
  have e2 : b / A.gcd id = l := by
    conv_lhs => rw [hl]
    exact Nat.mul_div_cancel_left _ hgpos
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 54–56 at 90702603d49f ↗
e3 have a.gcd b = A.gcd id * k.gcd l
Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with e3 : a.gcd b = A.gcd id * k.gcd l.
Uses library id, Nat.gcd_mul_left.
Lean, lines 58–60
```
  have e3 : a.gcd b = A.gcd id * k.gcd l := by
    conv_lhs => rw [hk, hl]
    exact Nat.gcd_mul_left _ _ _
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, lines 58–60 at 90702603d49f ↗
e4 have (↑a : ℚ) = (↑(A.gcd id) : ℚ) * (↑k : ℚ)
Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with e4 : (↑a : ℚ) = (↑(A.gcd id) : ℚ) * (↑k : ℚ).
Uses library id.
Lean, line 61
```
  have e4 : (a : ℚ) = ((A.gcd id : ℕ) : ℚ) * k := by exact_mod_cast hk
```
targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, line 61 at 90702603d49f ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000136.json, merge commit 90702603d49f.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean, sha256 00157500052a.

import Mathlib

open Filter

/-! Hole `h2` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_402__h2 : (∀ (A : Finset ℕ) (m : ℕ),
    0 ∉ A →
      (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
        ∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u) →
  ∀ (A : Finset ℕ),
    0 ∉ A →
      A.Nonempty →
        (∀ (B : Finset ℕ), 0 ∉ B → B.card = A.card → B.gcd id = 1 → ∃ a ∈ B, ∃ b ∈ B, a.gcd b ≤ (a / B.card : ℚ)) →
          ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro _ A hA hne hprim
  obtain ⟨x, hx⟩ := hne
  have hx0 : x ≠ 0 := ne_of_mem_of_not_mem hx hA
  have hgdvd : ∀ a ∈ A, A.gcd id ∣ a := fun a ha => Finset.gcd_dvd (f := id) ha
  have hg0 : A.gcd id ≠ 0 := by
    intro h0
    have h1 := hgdvd x hx
    rw [h0] at h1
    exact hx0 (Nat.eq_zero_of_zero_dvd h1)
  have hgpos : 0 < A.gcd id := Nat.pos_of_ne_zero hg0
  have hB0 : 0 ∉ A.image (fun a => a / A.gcd id) := by
    intro h
    obtain ⟨a, ha, hag⟩ := Finset.mem_image.mp h
    have ha0 : a ≠ 0 := ne_of_mem_of_not_mem ha hA
    obtain ⟨k, hk⟩ := hgdvd a ha
    have hk0 : k = 0 := by
      have h2 : a / A.gcd id = k := by
        conv_lhs => rw [hk]
        exact Nat.mul_div_cancel_left _ hgpos
      rw [← h2]; exact hag
    exact ha0 (by rw [hk, hk0, mul_zero])
  have hcard : (A.image (fun a => a / A.gcd id)).card = A.card := by
    apply Finset.card_image_of_injOn
    intro a ha b hb hab
    exact (Nat.div_left_inj (hgdvd a ha) (hgdvd b hb)).mp hab
  have hgcd : (A.image (fun a => a / A.gcd id)).gcd id = 1 := by
    rw [Finset.gcd_image]
    exact Finset.gcd_div_id_eq_one hx hx0
  obtain ⟨a', ha', b', hb', hab⟩ := hprim _ hB0 hcard hgcd
  obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp ha'
  obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hb'
  refine ⟨a, ha, b, hb, ?_⟩
  obtain ⟨k, hk⟩ := hgdvd a ha
  obtain ⟨l, hl⟩ := hgdvd b hb
  have e1 : a / A.gcd id = k := by
    conv_lhs => rw [hk]
    exact Nat.mul_div_cancel_left _ hgpos
  have e2 : b / A.gcd id = l := by
    conv_lhs => rw [hl]
    exact Nat.mul_div_cancel_left _ hgpos
  rw [hcard, e1, e2] at hab
  have e3 : a.gcd b = A.gcd id * k.gcd l := by
    conv_lhs => rw [hk, hl]
    exact Nat.gcd_mul_left _ _ _
  have e4 : (a : ℚ) = ((A.gcd id : ℕ) : ℚ) * k := by exact_mod_cast hk
  rw [e3, e4]
  push_cast
  rw [mul_div_assoc]
  exact mul_le_mul_of_nonneg_left hab (by positivity)

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib

open Filter

/-! Hole `h2` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_402__h2 : (∀ (A : Finset ℕ) (m : ℕ),
    0 ∉ A →
      (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
        ∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u) →
  ∀ (A : Finset ℕ),
    0 ∉ A →
      A.Nonempty →
        (∀ (B : Finset ℕ), 0 ∉ B → B.card = A.card → B.gcd id = 1 → ∃ a ∈ B, ∃ b ∈ B, a.gcd b ≤ (a / B.card : ℚ)) →
          ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  sorry

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

Rendered from gloss/654d0531aba3….md · Improve these words →

Rendered from targets/erdos-402/nodes/erdos-402--h2-v2/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000136.json, merge commit 90702603d49f.

Verdict pass, from attestations/000136.json.

Submitter: tester-402-e514
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000136.json, merge commit 90702603d49f.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/erdos-402--h2-v2/Witness.lean, sha256 281245ae9566.

import Mathlib

open Filter

theorem witness : ∃ A : Finset ℕ,
    (∀ (A : Finset ℕ) (m : ℕ), 0 ∉ A → (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
      ∀ a ∈ A, ∀ b ∈ A, ∃ u v : ℕ, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ Nat.Coprime u v ∧ a * v = b * u) ∧
    0 ∉ A ∧ A.Nonempty ∧
    (∀ B : Finset ℕ, 0 ∉ B → B.card = A.card → B.gcd id = 1 →
      ∃ a ∈ B, ∃ b ∈ B, a.gcd b ≤ (a / B.card : ℚ)) := by
  have hh1 : ∀ (A : Finset ℕ) (m : ℕ), 0 ∉ A → (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
      ∀ a ∈ A, ∀ b ∈ A, ∃ u v : ℕ, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ Nat.Coprime u v ∧ a * v = b * u := by
      intro A m hA hbound a ha b hb
      have ha0 : a ≠ 0 := ne_of_mem_of_not_mem ha hA
      have hb0 : b ≠ 0 := ne_of_mem_of_not_mem hb hA
      have hd : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
      obtain ⟨u, hu⟩ := Nat.gcd_dvd_left a b
      obtain ⟨v, hv⟩ := Nat.gcd_dvd_right a b
      refine ⟨u, v, ?_, ?_, ?_, ?_, ?_, ?_⟩
      · apply Nat.pos_of_ne_zero
        intro h0
        apply ha0
        rw [hu, h0, mul_zero]
      · have h1 : a.gcd b * u ≤ a.gcd b * m := by
          rw [← hu, mul_comm]
          exact hbound a ha b hb
        exact Nat.le_of_mul_le_mul_left h1 hd
      · apply Nat.pos_of_ne_zero
        intro h0
        apply hb0
        rw [hv, h0, mul_zero]
      · have h2 : a.gcd b * v ≤ a.gcd b * m := by
          rw [← hv, mul_comm, Nat.gcd_comm]
          exact hbound b hb a ha
        exact Nat.le_of_mul_le_mul_left h2 hd
      · have h3 : a.gcd b * u.gcd v = a.gcd b * 1 := by
          rw [← Nat.gcd_mul_left, ← hu, ← hv, mul_one]
        exact Nat.eq_of_mul_eq_mul_left hd h3
      · calc a * v = a.gcd b * u * v := by rw [← hu]
          _ = a.gcd b * v * u := by ring
          _ = b * u := by rw [← hv]
  refine ⟨{1}, hh1, by simp, by simp, ?_⟩
  intro B hB hcard hg
  rw [Finset.card_singleton] at hcard
  obtain ⟨c, rfl⟩ := Finset.card_eq_one.mp hcard
  exact ⟨c, by simp, c, by simp, by simp⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

How to read this page

How to read a statement’s page →