Open Proof Network

Problems / erdos-402 / variant-4ad214d0

Graham's bound for |A| = 15

variant-4ad214d0

proved

Definition.

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

Every set A of exactly fifteen positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

unverified · history

Lean
theorem Opn.erdos_402_card_fifteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 15 → ∃ 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, 000307, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000307.json, merge commit 6a97a4214037.

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.

  1. toQ have ∀ (a b : ℕ), (15 : ℕ) * a.gcd b ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with toQ : ∀ (a b : ℕ), (15 : ℕ) * a.gcd b ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

    Uses library le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. .

    Lean, lines 15–19
      have toQ : ∀ a b : ℕ, 15 * a.gcd b ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b hab
    have hN : ((A.card : ℕ) : ℚ) = 15 := by rw [hcard]; norm_num
    rw [hN, le_div_iff₀ (by norm_num : (0 : ℚ) < 15)]
    exact_mod_cast (by omega : a.gcd b * 15 ≤ a)

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 15–19 at 6a97a4214037 ↗

    1. toQ.hN have (↑A.card : ℚ) = (15 : ℚ)

      Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hN : (↑A.card : ℚ) = (15 : ℚ).

      Lean, line 17
          have hN : ((A.card : ℕ) : ℚ) = 15 := by rw [hcard]; norm_num

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 17 at 6a97a4214037 ↗

  2. hne have A.Nonempty

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hne : A.Nonempty.

    Uses library Finset.card_pos.

    Lean, line 20
      have hne : A.Nonempty := Finset.card_pos.mp (by omega)

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 20 at 6a97a4214037 ↗

  3. hMA have A.max' hne ∈ A

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hMA : A.max' hne ∈ A.

    Uses library Finset.max'_mem.

    Lean, line 21
      have hMA : A.max' hne ∈ A := Finset.max'_mem A hne

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 21 at 6a97a4214037 ↗

  4. hMpos have (0 : ℕ) < A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hMpos : (0 : ℕ) < A.max' hne.

    Uses library Nat.pos_of_ne_zero.

    Lean, line 22
      have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero fun h => h0 (h ▸ hMA)

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 22 at 6a97a4214037 ↗

  5. s5 case

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

    Uses library Exists.intro Existential introduction. .

    Lean, lines 24–25
      · obtain ⟨x, hxA, hx⟩ := hdirect
    exact ⟨A.max' hne, hMA, x, hxA, toQ _ x hx⟩

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 24–25 at 6a97a4214037 ↗

    1. s5.s1 obtain ∃ x ∈ A, (15 : ℕ) * (A.max' hne).gcd x ≤ A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hxA : x ∈ A, hx : (15 : ℕ) * (A.max' hne).gcd x ≤ A.max' hne.

      Lean, line 24
        · obtain ⟨x, hxA, hx⟩ := hdirect

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 24 at 6a97a4214037 ↗

  6. hval have ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hval : ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne.

    Uses library List Linked lists: ordered lists, in which each element has a reference to the next element. , Exists.intro Existential introduction. .

    Lean, lines 28–58
      have hval : ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ ([25740, 27720, 30030, 32760, 36036, 40040, 45045, 51480, 55440, 60060, 65520, 72072,
      77220, 80080, 83160, 90090, 98280, 102960, 108108, 110880, 120120, 128700, 131040,
      135135, 138600, 144144, 150150, 154440, 160160, 163800, 166320, 180180, 194040, 196560,
      200200, 205920, 210210, 216216, 221760, 225225, 229320, 231660, 240240, 249480, 252252,
      257400, 262080, 270270, 277200, 280280, 283140, 288288, 294840, 300300, 304920, 308880,
      315315, 320320, 324324, 327600, 330330, 332640, 334620] : List ℕ),
      360360 * x = c * A.max' hne := by
    intro x hx
    obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero fun h => h0 (h ▸ hxA)
    have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
    have hbig : A.max' hne < 15 * (A.max' hne).gcd x := hdirect x hxA
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
    have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    have hkN : k < 15 := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    have hjk : j < k := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    have hj0 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj
        omega
      · exact h
    refine ⟨360360 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 28–58 at 6a97a4214037 ↗

    1. hval.s1 obtain x ≠ A.max' hne ∧ x ∈ A

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hxM : x ≠ A.max' hne, hxA : x ∈ A.

      Uses library Finset.mem_erase.

      Lean, line 36
          obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 36 at 6a97a4214037 ↗

    2. hval.hxpos have (0 : ℕ) < x

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hxpos : (0 : ℕ) < x.

      Uses library Nat.pos_of_ne_zero.

      Lean, line 37
          have hxpos : 0 < x := Nat.pos_of_ne_zero fun h => h0 (h ▸ hxA)

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 37 at 6a97a4214037 ↗

    3. hval.hxlt have x < A.max' hne

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hxlt : x < A.max' hne.

      Uses library lt_of_le_of_ne, Finset.le_max'.

      Lean, line 38
          have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 38 at 6a97a4214037 ↗

    4. hval.hbig have A.max' hne < (15 : ℕ) * (A.max' hne).gcd x

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hbig : A.max' hne < (15 : ℕ) * (A.max' hne).gcd x.

      Lean, line 39
          have hbig : A.max' hne < 15 * (A.max' hne).gcd x := hdirect x hxA

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 39 at 6a97a4214037 ↗

    5. hval.s5 obtain (A.max' hne).gcd x ∣ A.max' hne

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.

      Uses library Nat.gcd_dvd_left.

      Lean, line 40
          obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 40 at 6a97a4214037 ↗

    6. hval.s6 obtain (A.max' hne).gcd x ∣ x

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.

      Uses library Nat.gcd_dvd_right.

      Lean, line 41
          obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 41 at 6a97a4214037 ↗

    7. hval.hgpos have (0 : ℕ) < (A.max' hne).gcd x

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hgpos : (0 : ℕ) < (A.max' hne).gcd x.

      Uses library Nat.gcd_pos_of_pos_right.

      Lean, line 42
          have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 42 at 6a97a4214037 ↗

    8. hval.hkN have k < (15 : ℕ)

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hkN : k < (15 : ℕ).

      Lean, lines 43–46
          have hkN : k < 15 := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 43–46 at 6a97a4214037 ↗

      1. hval.hkN.this have (A.max' hne).gcd x * (15 : ℕ) ≤ (A.max' hne).gcd x * k

        Leaves False, with this : (A.max' hne).gcd x * (15 : ℕ) ≤ (A.max' hne).gcd x * k.

        Uses library Nat.mul_le_mul_left, not_lt.

        Lean, line 45
              have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)

        targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 45 at 6a97a4214037 ↗

    9. hval.hjk have j < k

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hjk : j < k.

      Lean, lines 47–50
          have hjk : j < k := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 47–50 at 6a97a4214037 ↗

      1. hval.hjk.this have (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j

        Leaves False, with this : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j.

        Uses library Nat.mul_le_mul_left, not_lt.

        Lean, line 49
              have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)

        targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 49 at 6a97a4214037 ↗

    10. hval.hj0 have (0 : ℕ) < j

      Leaves ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne, with hj0 : (0 : ℕ) < j.

      Uses library Nat.eq_zero_or_pos.

      Lean, lines 51–55
          have hj0 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj
        omega
      · exact h

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 51–55 at 6a97a4214037 ↗

      1. hval.hj0.s1 case

        Leaves (0 : ℕ) < j.

        Uses library Nat.mul_zero.

        Lean, lines 53–54
              · rw [h, Nat.mul_zero] at hj
        omega

        targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 53–54 at 6a97a4214037 ↗

      2. hval.hj0.s2 case

        Leaves (0 : ℕ) < j.

        Lean, line 55
              · exact h

        targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 55 at 6a97a4214037 ↗

    11. hval.s11 case

      Leaves (360360 : ℕ) * j / k ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y.

      Lean, line 57
          · interval_cases k <;> interval_cases j <;> decide

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 57 at 6a97a4214037 ↗

    12. hval.s12 case

      Leaves (360360 : ℕ) * x = (360360 : ℕ) * j / k * A.max' hne.

      Lean, line 58
          · interval_cases k <;> interval_cases j <;> omega

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 58 at 6a97a4214037 ↗

  7. s7 obtain ∃ (cls : ℕ → List ℕ), cls = fun (i : ℕ) => [[(180180 : ℕ), (221760 : ℕ), (294840 : ℕ)], [(120120 : ℕ), (166320 : ℕ), (225225 : ℕ), (231660 : ℕ), (252252 : ℕ), (327600 : ℕ)], [(90090 : ℕ), (196560 : ℕ), (200200 : ℕ), (205920 : ℕ), (304920 : ℕ), (324324 : ℕ)], [(32760 : ℕ), (77220 : ℕ), (240240 : ℕ), (249480 : ℕ), (315315 : ℕ)], [(60060 : ℕ), (138600 : ℕ), (154440 : ℕ), (229320 : ℕ), (288288 : ℕ)], [(51480 : ℕ), (108108 : ℕ), (110880 : ℕ), (150150 : ℕ), (262080 : ℕ), (280280 : ℕ)], [(30030 : ℕ), (102960 : ℕ), (163800 : ℕ), (194040 : ℕ), (216216 : ℕ), (320320 : ℕ)], [(72072 : ℕ), (160160 : ℕ), (270270 : ℕ), (277200 : ℕ), (283140 : ℕ)], [(40040 : ℕ), (55440 : ℕ), (131040 : ℕ), (135135 : ℕ), (300300 : ℕ), (308880 : ℕ)], [(27720 : ℕ), (98280 : ℕ), (144144 : ℕ), (210210 : ℕ), (257400 : ℕ)], [(36036 : ℕ), (65520 : ℕ), (83160 : ℕ), (128700 : ℕ), (330330 : ℕ)], [(25740 : ℕ), (80080 : ℕ), (332640 : ℕ)], [(45045 : ℕ), (334620 : ℕ)]].getD i []

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with cls : ℕ → List ℕ, hcls : cls = fun (i : ℕ) => [[(180180 : ℕ), (221760 : ℕ), (294840 : ℕ)], [(120120 : ℕ), (166320 : ℕ), (225225 : ℕ), (231660 : ℕ), (252252 : ℕ), (327600 : ℕ)], [(90090 : ℕ), (196560 : ℕ), (200200 : ℕ), (205920 : ℕ), (304920 : ℕ), (324324 : ℕ)], [(32760 : ℕ), (77220 : ℕ), (240240 : ℕ), (249480 : ℕ), (315315 : ℕ)], [(60060 : ℕ), (138600 : ℕ), (154440 : ℕ), (229320 : ℕ), (288288 : ℕ)], [(51480 : ℕ), (108108 : ℕ), (110880 : ℕ), (150150 : ℕ), (262080 : ℕ), (280280 : ℕ)], [(30030 : ℕ), (102960 : ℕ), (163800 : ℕ), (194040 : ℕ), (216216 : ℕ), (320320 : ℕ)], [(72072 : ℕ), (160160 : ℕ), (270270 : ℕ), (277200 : ℕ), (283140 : ℕ)], [(40040 : ℕ), (55440 : ℕ), (131040 : ℕ), (135135 : ℕ), (300300 : ℕ), (308880 : ℕ)], [(27720 : ℕ), (98280 : ℕ), (144144 : ℕ), (210210 : ℕ), (257400 : ℕ)], [(36036 : ℕ), (65520 : ℕ), (83160 : ℕ), (128700 : ℕ), (330330 : ℕ)], [(25740 : ℕ), (80080 : ℕ), (332640 : ℕ)], [(45045 : ℕ), (334620 : ℕ)]].getD i [].

    Uses library List Linked lists: ordered lists, in which each element has a reference to the next element. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 60–73
      obtain ⟨cls, hcls⟩ : ∃ cls : ℕ → List ℕ, cls = fun i => [[180180, 221760, 294840],
      [120120, 166320, 225225, 231660, 252252, 327600],
      [90090, 196560, 200200, 205920, 304920, 324324],
      [32760, 77220, 240240, 249480, 315315],
      [60060, 138600, 154440, 229320, 288288],
      [51480, 108108, 110880, 150150, 262080, 280280],
      [30030, 102960, 163800, 194040, 216216, 320320],
      [72072, 160160, 270270, 277200, 283140],
      [40040, 55440, 131040, 135135, 300300, 308880],
      [27720, 98280, 144144, 210210, 257400],
      [36036, 65520, 83160, 128700, 330330],
      [25740, 80080, 332640],
      [45045, 334620]].getD i [] :=
    ⟨_, rfl⟩

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 60–73 at 6a97a4214037 ↗

  8. s8 obtain ∃ (col : ℕ → ℕ), col = fun (c : ℕ) => List.findIdx (fun (D : List ℕ) => D.contains c) [[(180180 : ℕ), (221760 : ℕ), (294840 : ℕ)], [(120120 : ℕ), (166320 : ℕ), (225225 : ℕ), (231660 : ℕ), (252252 : ℕ), (327600 : ℕ)], [(90090 : ℕ), (196560 : ℕ), (200200 : ℕ), (205920 : ℕ), (304920 : ℕ), (324324 : ℕ)], [(32760 : ℕ), (77220 : ℕ), (240240 : ℕ), (249480 : ℕ), (315315 : ℕ)], [(60060 : ℕ), (138600 : ℕ), (154440 : ℕ), (229320 : ℕ), (288288 : ℕ)], [(51480 : ℕ), (108108 : ℕ), (110880 : ℕ), (150150 : ℕ), (262080 : ℕ), (280280 : ℕ)], [(30030 : ℕ), (102960 : ℕ), (163800 : ℕ), (194040 : ℕ), (216216 : ℕ), (320320 : ℕ)], [(72072 : ℕ), (160160 : ℕ), (270270 : ℕ), (277200 : ℕ), (283140 : ℕ)], [(40040 : ℕ), (55440 : ℕ), (131040 : ℕ), (135135 : ℕ), (300300 : ℕ), (308880 : ℕ)], [(27720 : ℕ), (98280 : ℕ), (144144 : ℕ), (210210 : ℕ), (257400 : ℕ)], [(36036 : ℕ), (65520 : ℕ), (83160 : ℕ), (128700 : ℕ), (330330 : ℕ)], [(25740 : ℕ), (80080 : ℕ), (332640 : ℕ)], [(45045 : ℕ), (334620 : ℕ)]]

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with col : ℕ → ℕ, hcol : col = fun (c : ℕ) => List.findIdx (fun (D : List ℕ) => D.contains c) [[(180180 : ℕ), (221760 : ℕ), (294840 : ℕ)], [(120120 : ℕ), (166320 : ℕ), (225225 : ℕ), (231660 : ℕ), (252252 : ℕ), (327600 : ℕ)], [(90090 : ℕ), (196560 : ℕ), (200200 : ℕ), (205920 : ℕ), (304920 : ℕ), (324324 : ℕ)], [(32760 : ℕ), (77220 : ℕ), (240240 : ℕ), (249480 : ℕ), (315315 : ℕ)], [(60060 : ℕ), (138600 : ℕ), (154440 : ℕ), (229320 : ℕ), (288288 : ℕ)], [(51480 : ℕ), (108108 : ℕ), (110880 : ℕ), (150150 : ℕ), (262080 : ℕ), (280280 : ℕ)], [(30030 : ℕ), (102960 : ℕ), (163800 : ℕ), (194040 : ℕ), (216216 : ℕ), (320320 : ℕ)], [(72072 : ℕ), (160160 : ℕ), (270270 : ℕ), (277200 : ℕ), (283140 : ℕ)], [(40040 : ℕ), (55440 : ℕ), (131040 : ℕ), (135135 : ℕ), (300300 : ℕ), (308880 : ℕ)], [(27720 : ℕ), (98280 : ℕ), (144144 : ℕ), (210210 : ℕ), (257400 : ℕ)], [(36036 : ℕ), (65520 : ℕ), (83160 : ℕ), (128700 : ℕ), (330330 : ℕ)], [(25740 : ℕ), (80080 : ℕ), (332640 : ℕ)], [(45045 : ℕ), (334620 : ℕ)]].

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 74–87
      obtain ⟨col, hcol⟩ : ∃ col : ℕ → ℕ, col = fun c => [[180180, 221760, 294840],
      [120120, 166320, 225225, 231660, 252252, 327600],
      [90090, 196560, 200200, 205920, 304920, 324324],
      [32760, 77220, 240240, 249480, 315315],
      [60060, 138600, 154440, 229320, 288288],
      [51480, 108108, 110880, 150150, 262080, 280280],
      [30030, 102960, 163800, 194040, 216216, 320320],
      [72072, 160160, 270270, 277200, 283140],
      [40040, 55440, 131040, 135135, 300300, 308880],
      [27720, 98280, 144144, 210210, 257400],
      [36036, 65520, 83160, 128700, 330330],
      [25740, 80080, 332640],
      [45045, 334620]].findIdx
      (fun D => D.contains c) := ⟨_, rfl⟩

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 74–87 at 6a97a4214037 ↗

  9. hcover have ∀ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, col c < (13 : ℕ) ∧ c ∈ cls (col c)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcover : ∀ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, col c < (13 : ℕ) ∧ c ∈ cls (col c).

    Uses library List Linked lists: ordered lists, in which each element has a reference to the next element. .

    Lean, lines 88–96
      have hcover : ∀ c ∈ ([25740, 27720, 30030, 32760, 36036, 40040, 45045, 51480, 55440, 60060, 65520, 72072,
      77220, 80080, 83160, 90090, 98280, 102960, 108108, 110880, 120120, 128700, 131040,
      135135, 138600, 144144, 150150, 154440, 160160, 163800, 166320, 180180, 194040, 196560,
      200200, 205920, 210210, 216216, 221760, 225225, 229320, 231660, 240240, 249480, 252252,
      257400, 262080, 270270, 277200, 280280, 283140, 288288, 294840, 300300, 304920, 308880,
      315315, 320320, 324324, 327600, 330330, 332640, 334620] : List ℕ),
      col c < 13 ∧ c ∈ cls (col c) := by
    subst hcol hcls
    decide

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 88–96 at 6a97a4214037 ↗

  10. hgood have ∀ i < (13 : ℕ), ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ (15 : ℕ) * c.gcd d ≤ c ∨ (15 : ℕ) * c.gcd d ≤ d

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgood : ∀ i < (13 : ℕ), ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ (15 : ℕ) * c.gcd d ≤ c ∨ (15 : ℕ) * c.gcd d ≤ d.

    Lean, lines 97–99
      have hgood : ∀ i < 13, ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ 15 * c.gcd d ≤ c ∨ 15 * c.gcd d ≤ d := by
    subst hcls
    decide

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 97–99 at 6a97a4214037 ↗

  11. hmaps have ∀ x ∈ A.erase (A.max' hne), col ((360360 : ℕ) * x / A.max' hne) ∈ Finset.range (13 : ℕ)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase (A.max' hne), col ((360360 : ℕ) * x / A.max' hne) ∈ Finset.range (13 : ℕ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mem_range, Nat.mul_div_cancel.

    Lean, lines 101–105
      have hmaps : ∀ x ∈ A.erase (A.max' hne), col (360360 * x / A.max' hne) ∈ Finset.range 13 := by
    intro x hx
    obtain ⟨c, hc, hxc⟩ := hval x hx
    rw [Finset.mem_range, hxc, Nat.mul_div_cancel _ hMpos]
    exact (hcover c hc).1

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 101–105 at 6a97a4214037 ↗

    1. hmaps.s1 obtain ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne

      Leaves col ((360360 : ℕ) * x / A.max' hne) ∈ Finset.range (13 : ℕ), with c : ℕ, hc : c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, hxc : (360360 : ℕ) * x = c * A.max' hne.

      Lean, line 103
          obtain ⟨c, hc, hxc⟩ := hval x hx

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 103 at 6a97a4214037 ↗

  12. hlt have (Finset.range (13 : ℕ)).card < (A.erase (A.max' hne)).card

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hlt : (Finset.range (13 : ℕ)).card < (A.erase (A.max' hne)).card.

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.card_erase_of_mem $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. , Finset.card_range.

    Lean, lines 106–108
      have hlt : (Finset.range 13).card < (A.erase (A.max' hne)).card := by
    rw [Finset.card_erase_of_mem hMA, hcard, Finset.card_range]
    norm_num

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 106–108 at 6a97a4214037 ↗

  13. s13 obtain ∃ x ∈ A.erase (A.max' hne), ∃ y ∈ A.erase (A.max' hne), x ≠ y ∧ col ((360360 : ℕ) * x / A.max' hne) = col ((360360 : ℕ) * y / A.max' hne)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A.erase (A.max' hne), y : ℕ, hy : y ∈ A.erase (A.max' hne), hxy : x ≠ y, hxycol : col ((360360 : ℕ) * x / A.max' hne) = col ((360360 : ℕ) * y / A.max' hne).

    Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole. .

    Lean, line 109
      obtain ⟨x, hx, y, hy, hxy, hxycol⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hlt hmaps

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 109 at 6a97a4214037 ↗

  14. s14 obtain ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * x = c * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with c : ℕ, hc : c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, hxc : (360360 : ℕ) * x = c * A.max' hne.

    Lean, line 110
      obtain ⟨c, hc, hxc⟩ := hval x hx

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 110 at 6a97a4214037 ↗

  15. s15 obtain ∃ c ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, (360360 : ℕ) * y = c * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with d : ℕ, hd : d ∈ let y := let y := let y := let y := [(327600 : ℕ), (330330 : ℕ), (332640 : ℕ), (334620 : ℕ)]; (308880 : ℕ) :: (315315 : ℕ) :: (320320 : ℕ) :: (324324 : ℕ) :: y; let y := (288288 : ℕ) :: (294840 : ℕ) :: (300300 : ℕ) :: (304920 : ℕ) :: y; (270270 : ℕ) :: (277200 : ℕ) :: (280280 : ℕ) :: (283140 : ℕ) :: y; let y := let y := (249480 : ℕ) :: (252252 : ℕ) :: (257400 : ℕ) :: (262080 : ℕ) :: y; (225225 : ℕ) :: (229320 : ℕ) :: (231660 : ℕ) :: (240240 : ℕ) :: y; let y := (205920 : ℕ) :: (210210 : ℕ) :: (216216 : ℕ) :: (221760 : ℕ) :: y; (180180 : ℕ) :: (194040 : ℕ) :: (196560 : ℕ) :: (200200 : ℕ) :: y; let y := let y := let y := (154440 : ℕ) :: (160160 : ℕ) :: (163800 : ℕ) :: (166320 : ℕ) :: y; (135135 : ℕ) :: (138600 : ℕ) :: (144144 : ℕ) :: (150150 : ℕ) :: y; let y := (110880 : ℕ) :: (120120 : ℕ) :: (128700 : ℕ) :: (131040 : ℕ) :: y; (90090 : ℕ) :: (98280 : ℕ) :: (102960 : ℕ) :: (108108 : ℕ) :: y; let y := let y := (72072 : ℕ) :: (77220 : ℕ) :: (80080 : ℕ) :: (83160 : ℕ) :: y; (51480 : ℕ) :: (55440 : ℕ) :: (60060 : ℕ) :: (65520 : ℕ) :: y; (25740 : ℕ) :: (27720 : ℕ) :: (30030 : ℕ) :: (32760 : ℕ) :: (36036 : ℕ) :: (40040 : ℕ) :: (45045 : ℕ) :: y, hyd : (360360 : ℕ) * y = d * A.max' hne.

    Lean, line 111
      obtain ⟨d, hd, hyd⟩ := hval y hy

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 111 at 6a97a4214037 ↗

  16. hcd have c ≠ d

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcd : c ≠ d.

    Lean, lines 113–115
      have hcd : c ≠ d := by
    rintro rfl
    exact hxy (by omega)

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 113–115 at 6a97a4214037 ↗

  17. hcmem have c ∈ cls (col c)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcmem : c ∈ cls (col c).

    Lean, line 116
      have hcmem := (hcover c hc).2

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 116 at 6a97a4214037 ↗

  18. hdmem have d ∈ cls (col d)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hdmem : d ∈ cls (col d).

    Lean, line 117
      have hdmem := (hcover d hd).2

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 117 at 6a97a4214037 ↗

  19. hg have c.gcd d * A.max' hne = (360360 : ℕ) * x.gcd y

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hg : c.gcd d * A.max' hne = (360360 : ℕ) * x.gcd y.

    Uses library Nat.gcd_mul_right, Nat.gcd_mul_left.

    Lean, lines 120–121
      have hg : c.gcd d * A.max' hne = 360360 * x.gcd y := by
    rw [← Nat.gcd_mul_right, ← hxc, ← hyd, Nat.gcd_mul_left]

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 120–121 at 6a97a4214037 ↗

  20. hxA have x ∈ A

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hxA : x ∈ A.

    Uses library Finset.mem_erase.

    Lean, line 122
      have hxA : x ∈ A := (Finset.mem_erase.mp hx).2

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 122 at 6a97a4214037 ↗

  21. hyA have y ∈ A

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hyA : y ∈ A.

    Uses library Finset.mem_erase.

    Lean, line 123
      have hyA : y ∈ A := (Finset.mem_erase.mp hy).2

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 123 at 6a97a4214037 ↗

  22. s22 case

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

    Uses library absurd Anything follows from two contradictory hypotheses. .

    Lean, line 125
      · exact absurd h hcd

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 125 at 6a97a4214037 ↗

  23. s23 case

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

    Uses library Exists.intro Existential introduction. , Nat.mul_assoc.

    Lean, lines 126–129
      · refine ⟨x, hxA, y, hyA, toQ x y ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hxc] at h2
    omega

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 126–129 at 6a97a4214037 ↗

    1. s23.h2 have (15 : ℕ) * c.gcd d * A.max' hne ≤ c * A.max' hne

      Leaves (15 : ℕ) * x.gcd y ≤ x, with h2 : (15 : ℕ) * c.gcd d * A.max' hne ≤ c * A.max' hne.

      Uses library Nat.mul_le_mul_right.

      Lean, line 127
          have h2 := Nat.mul_le_mul_right (A.max' hne) h

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 127 at 6a97a4214037 ↗

  24. s24 case

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

    Uses library Exists.intro Existential introduction. , Nat.mul_assoc, Nat.gcd_comm.

    Lean, lines 130–134
      · refine ⟨y, hyA, x, hxA, toQ y x ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hyd] at h2
    rw [Nat.gcd_comm]
    omega

    targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, lines 130–134 at 6a97a4214037 ↗

    1. s24.h2 have (15 : ℕ) * c.gcd d * A.max' hne ≤ d * A.max' hne

      Leaves (15 : ℕ) * y.gcd x ≤ y, with h2 : (15 : ℕ) * c.gcd d * A.max' hne ≤ d * A.max' hne.

      Uses library Nat.mul_le_mul_right.

      Lean, line 131
          have h2 := Nat.mul_le_mul_right (A.max' hne) h

      targets/erdos-402/nodes/variant-4ad214d0/Proof.lean, line 131 at 6a97a4214037 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000307.json, merge commit 6a97a4214037.

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/variant-4ad214d0/Proof.lean, sha256 0ee6d9d10680.
import Mathlib
import Nodes.«variant-4ad214d0».Context

/-! Graham's gcd conjecture (Erdős problem 402) restricted to sets of exactly fifteen elements.
Route: let M be the largest element. Either some x has 15 · gcd(M, x) ≤ M, and the pair (M, x)
works, or every other x has M < 15 · gcd(M, x), so M = k·g and x = j·g with g = gcd(M, x) and
1 ≤ j < k ≤ 14; then 360360 · x / M (360360 = lcm(1..14)) takes one of 63 values. A computer
search finds a split of those 63 values into 13 classes in each of which two distinct values
c, d satisfy 15 · gcd(c, d) ≤ max(c, d); fourteen elements in thirteen classes force two into one
class, and gcd(x, y) · 360360 = gcd(c, d) · M carries the bound back to x and y. -/

theorem Opn.erdos_402_card_fifteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 15 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A h0 hcard
  have toQ : ∀ a b : ℕ, 15 * a.gcd b ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b hab
    have hN : ((A.card : ℕ) : ℚ) = 15 := by rw [hcard]; norm_num
    rw [hN, le_div_iff₀ (by norm_num : (0 : ℚ) < 15)]
    exact_mod_cast (by omega : a.gcd b * 15 ≤ a)
  have hne : A.Nonempty := Finset.card_pos.mp (by omega)
  have hMA : A.max' hne ∈ A := Finset.max'_mem A hne
  have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero fun h => h0 (h ▸ hMA)
  by_cases hdirect : ∃ x ∈ A, 15 * (A.max' hne).gcd x ≤ A.max' hne
  · obtain ⟨x, hxA, hx⟩ := hdirect
    exact ⟨A.max' hne, hMA, x, hxA, toQ _ x hx⟩
  simp only [not_exists, not_and, not_le] at hdirect
  -- every other element x has 360360 x = c M with c = 360360 j / k, 1 ≤ j < k ≤ 14
  have hval : ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ ([25740, 27720, 30030, 32760, 36036, 40040, 45045, 51480, 55440, 60060, 65520, 72072,
      77220, 80080, 83160, 90090, 98280, 102960, 108108, 110880, 120120, 128700, 131040,
      135135, 138600, 144144, 150150, 154440, 160160, 163800, 166320, 180180, 194040, 196560,
      200200, 205920, 210210, 216216, 221760, 225225, 229320, 231660, 240240, 249480, 252252,
      257400, 262080, 270270, 277200, 280280, 283140, 288288, 294840, 300300, 304920, 308880,
      315315, 320320, 324324, 327600, 330330, 332640, 334620] : List ℕ),
      360360 * x = c * A.max' hne := by
    intro x hx
    obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero fun h => h0 (h ▸ hxA)
    have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
    have hbig : A.max' hne < 15 * (A.max' hne).gcd x := hdirect x hxA
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
    have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    have hkN : k < 15 := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    have hjk : j < k := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    have hj0 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj
        omega
      · exact h
    refine ⟨360360 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega
  -- a split of the 63 values into 13 classes, each pairwise good (found by computer search)
  obtain ⟨cls, hcls⟩ : ∃ cls : ℕ → List ℕ, cls = fun i => [[180180, 221760, 294840],
      [120120, 166320, 225225, 231660, 252252, 327600],
      [90090, 196560, 200200, 205920, 304920, 324324],
      [32760, 77220, 240240, 249480, 315315],
      [60060, 138600, 154440, 229320, 288288],
      [51480, 108108, 110880, 150150, 262080, 280280],
      [30030, 102960, 163800, 194040, 216216, 320320],
      [72072, 160160, 270270, 277200, 283140],
      [40040, 55440, 131040, 135135, 300300, 308880],
      [27720, 98280, 144144, 210210, 257400],
      [36036, 65520, 83160, 128700, 330330],
      [25740, 80080, 332640],
      [45045, 334620]].getD i [] :=
    ⟨_, rfl⟩
  obtain ⟨col, hcol⟩ : ∃ col : ℕ → ℕ, col = fun c => [[180180, 221760, 294840],
      [120120, 166320, 225225, 231660, 252252, 327600],
      [90090, 196560, 200200, 205920, 304920, 324324],
      [32760, 77220, 240240, 249480, 315315],
      [60060, 138600, 154440, 229320, 288288],
      [51480, 108108, 110880, 150150, 262080, 280280],
      [30030, 102960, 163800, 194040, 216216, 320320],
      [72072, 160160, 270270, 277200, 283140],
      [40040, 55440, 131040, 135135, 300300, 308880],
      [27720, 98280, 144144, 210210, 257400],
      [36036, 65520, 83160, 128700, 330330],
      [25740, 80080, 332640],
      [45045, 334620]].findIdx
      (fun D => D.contains c) := ⟨_, rfl⟩
  have hcover : ∀ c ∈ ([25740, 27720, 30030, 32760, 36036, 40040, 45045, 51480, 55440, 60060, 65520, 72072,
      77220, 80080, 83160, 90090, 98280, 102960, 108108, 110880, 120120, 128700, 131040,
      135135, 138600, 144144, 150150, 154440, 160160, 163800, 166320, 180180, 194040, 196560,
      200200, 205920, 210210, 216216, 221760, 225225, 229320, 231660, 240240, 249480, 252252,
      257400, 262080, 270270, 277200, 280280, 283140, 288288, 294840, 300300, 304920, 308880,
      315315, 320320, 324324, 327600, 330330, 332640, 334620] : List ℕ),
      col c < 13 ∧ c ∈ cls (col c) := by
    subst hcol hcls
    decide
  have hgood : ∀ i < 13, ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ 15 * c.gcd d ≤ c ∨ 15 * c.gcd d ≤ d := by
    subst hcls
    decide
  -- pigeonhole: 14 other elements, 13 classes
  have hmaps : ∀ x ∈ A.erase (A.max' hne), col (360360 * x / A.max' hne) ∈ Finset.range 13 := by
    intro x hx
    obtain ⟨c, hc, hxc⟩ := hval x hx
    rw [Finset.mem_range, hxc, Nat.mul_div_cancel _ hMpos]
    exact (hcover c hc).1
  have hlt : (Finset.range 13).card < (A.erase (A.max' hne)).card := by
    rw [Finset.card_erase_of_mem hMA, hcard, Finset.card_range]
    norm_num
  obtain ⟨x, hx, y, hy, hxy, hxycol⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hlt hmaps
  obtain ⟨c, hc, hxc⟩ := hval x hx
  obtain ⟨d, hd, hyd⟩ := hval y hy
  rw [hxc, hyd, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hxycol
  have hcd : c ≠ d := by
    rintro rfl
    exact hxy (by omega)
  have hcmem := (hcover c hc).2
  have hdmem := (hcover d hd).2
  rw [← hxycol] at hdmem
  -- carry the good pair of values back to x and y
  have hg : c.gcd d * A.max' hne = 360360 * x.gcd y := by
    rw [← Nat.gcd_mul_right, ← hxc, ← hyd, Nat.gcd_mul_left]
  have hxA : x ∈ A := (Finset.mem_erase.mp hx).2
  have hyA : y ∈ A := (Finset.mem_erase.mp hy).2
  rcases hgood (col c) (hcover c hc).1 c hcmem d hdmem with h | h | h
  · exact absurd h hcd
  · refine ⟨x, hxA, y, hyA, toQ x y ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hxc] at h2
    omega
  · refine ⟨y, hyA, x, hxA, toQ y x ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hyd] at h2
    rw [Nat.gcd_comm]
    omega

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
import Nodes.«variant-4ad214d0».Context

/-! Graham's gcd conjecture (Erdős problem 402) restricted to sets of exactly fifteen elements.
Route: let M be the largest element. Either some x has 15 · gcd(M, x) ≤ M, and the pair (M, x)
works, or every other x has M < 15 · gcd(M, x), so M = k·g and x = j·g with g = gcd(M, x) and
1 ≤ j < k ≤ 14; then 360360 · x / M (360360 = lcm(1..14)) takes one of 63 values. A computer
search finds a split of those 63 values into 13 classes in each of which two distinct values
c, d satisfy 15 · gcd(c, d) ≤ max(c, d); fourteen elements in thirteen classes force two into one
class, and gcd(x, y) · 360360 = gcd(c, d) · M carries the bound back to x and y. -/

theorem Opn.erdos_402_card_fifteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 15 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  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 →

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

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

Every set A of exactly fifteen positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

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

Rendered from targets/erdos-402/nodes/variant-4ad214d0/Statement.lean. Origin: variant (partial).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000307.json, merge commit 6a97a4214037.

Verdict pass, from attestations/000307.json.

Submitter
t0929-5
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000307.json, merge commit 6a97a4214037.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/variant-4ad214d0/Witness.lean, sha256 864d8ecce7ce.
import Mathlib

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 15 := ⟨Finset.Icc 1 15, by decide, by decide⟩

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 →

Relation to the problem’s statement

Checked by the kernel — checked at admission (D-30); no proof of the node is implied.

Relation.lean — the implication between this variant and the problem’s statement, checked by the gate when the variant was admitted and immutable after (D-30). Rendered from targets/erdos-402/nodes/variant-4ad214d0/Relation.lean, sha256 960d743f79be.
-- relation: partial
import Mathlib

theorem relation :
    (∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ᵉ (a ∈ A) (b ∈ A), a.gcd b ≤ (a / A.card : ℚ)) →
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 15 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro hroot A h0 hcard
  apply hroot A h0
  rw [← Finset.card_pos, hcard]
  norm_num

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

Acknowledged findings (1)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at ↑a / ↑A.card

A.card = 15 is a hypothesis, so the divisor is 15 wherever the conclusion is read; the root statement divides by A.card in the same way.

How to read this page

How to read a statement’s page →