Graham's bound for |A| ≤ 24

Checked by the kernel — an outline of the attested proof below: attestations/000309.json, merge commit d2b3cf021906.

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. general have ∀ (n L : ℕ) (cls : List (List ℕ)), (2 : ℕ) ≤ n → (0 : ℕ) < L → (∀ k < n, (0 : ℕ) < k → L / k * k = L) → (∀ k < n, ∀ j < k, (0 : ℕ) < j → List.findIdx (fun (l : List ℕ) => decide (L / k * j ∈ l)) cls < n - (2 : ℕ) ∧ L / k * j ∈ cls.getD (List.findIdx (fun (l : List ℕ) => decide (L / k * j ∈ l)) cls) []) → (∀ i < n - (2 : ℕ), ∀ v ∈ cls.getD i [], ∀ w ∈ cls.getD i [], v ≠ w → n * v.gcd w ≤ v ∨ n * v.gcd w ≤ w) → ∀ (A : Finset ℕ), (0 : ℕ) ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)

   Leaves ∀ (A : Finset ℕ), (0 : ℕ) ∉ A → A.Nonempty → A.card ≤ (24 : ℕ) → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with general : ∀ (n L : ℕ) (cls : List (List ℕ)), (2 : ℕ) ≤ n → (0 : ℕ) < L → (∀ k < n, (0 : ℕ) < k → L / k * k = L) → (∀ k < n, ∀ j < k, (0 : ℕ) < j → List.findIdx (fun (l : List ℕ) => decide (L / k * j ∈ l)) cls < n - (2 : ℕ) ∧ L / k * j ∈ cls.getD (List.findIdx (fun (l : List ℕ) => decide (L / k * j ∈ l)) cls) []) → (∀ i < n - (2 : ℕ), ∀ v ∈ cls.getD i [], ∀ w ∈ cls.getD i [], v ≠ w → n * v.gcd w ≤ v ∨ n * v.gcd w ≤ w) → ∀ (A : Finset ℕ), (0 : ℕ) ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

   Uses library List Linked lists: ordered lists, in which each element has a reference to the next element. , Decidable.decide Converts a decidable proposition into a Bool. , Finset Finset α is the type of finite sets of elements of α. .

   Lean, lines 15–118

     have general : ∀ (n L : ℕ) (cls : List (List ℕ)), 2 ≤ n → 0 < L →
         (∀ k < n, 0 < k → L / k * k = L) →
         (∀ k < n, ∀ j < k, 0 < j →
           cls.findIdx (fun l => decide (L / k * j ∈ l)) < n - 2 ∧
           L / k * j ∈ cls.getD (cls.findIdx (fun l => decide (L / k * j ∈ l))) []) →
         (∀ i < n - 2, ∀ v ∈ cls.getD i [], ∀ w ∈ cls.getD i [], v ≠ w →
           n * v.gcd w ≤ v ∨ n * v.gcd w ≤ w) →
         ∀ A : Finset ℕ, 0 ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
       intro n L cls hn2 hLpos hL H1 H2 A hA hn
       have hpos : 0 < A.card := by omega
       have hne : A.Nonempty := Finset.card_pos.mp hpos
       have key : ∀ a b : ℕ, a.gcd b * A.card ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
         intro a b h
         rw [le_div_iff₀ (by exact_mod_cast hpos)]
         exact_mod_cast h
       have hM : A.max' hne ∈ A := Finset.max'_mem A hne
       have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
       by_cases hw : ∃ x ∈ A, (A.max' hne).gcd x * n ≤ A.max' hne
       · obtain ⟨x, hx, h⟩ := hw
         exact ⟨_, hM, x, hx, key _ x (by rw [hn]; exact h)⟩
       push_neg at hw
       have forms : ∀ x ∈ A.erase (A.max' hne), ∃ k j, k < n ∧ j < k ∧ 0 < j ∧
           L * x = L / k * j * A.max' hne := by
         intro x hx
         rw [Finset.mem_erase] at hx
         have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))
         have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
         have hg := hw x hx.2
         obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
         obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
         obtain ⟨g, hgd⟩ : ∃ g, (A.max' hne).gcd x = g := ⟨_, rfl⟩
         rw [hgd] at hk hj hg
         have hkN : k < n := by
           by_contra hh
           push_neg at hh
           have := Nat.mul_le_mul_left g hh
           omega
         have hjk : j < k := by
           by_contra hh
           push_neg at hh
           have := Nat.mul_le_mul_left g hh
           omega
         have hj1 : 0 < j := by
           rcases Nat.eq_zero_or_pos j with h | h
           · subst h
             omega
           · exact h
         refine ⟨k, j, hkN, hjk, hj1, ?_⟩
         have hLk := hL k hkN (by omega)
         rw [hj, hk]
         calc L * (g * j) = (L / k * k) * (g * j) := by rw [hLk]
           _ = L / k * j * (g * k) := by ring
       have hcard : (A.erase (A.max' hne)).card = n - 1 := by
         rw [Finset.card_erase_of_mem hM, hn]
       have hmaps : ∀ x ∈ A.erase (A.max' hne),
           cls.findIdx (fun l => decide (L * x / A.max' hne ∈ l)) ∈ Finset.range (n - 2) := by
         intro x hx
         obtain ⟨k, j, hk, hj, hj0, he⟩ := forms x hx
         rw [Finset.mem_range, he, Nat.mul_div_cancel _ hMpos]
         exact (H1 k hk j hj hj0).1
       obtain ⟨x, hx, y, hy, hxy, hc⟩ :=
         Finset.exists_ne_map_eq_of_card_lt_of_maps_to (by rw [hcard, Finset.card_range]; omega) hmaps
       obtain ⟨k, j, hk, hj, hj0, hex⟩ := forms x hx
       obtain ⟨k', j', hk', hj', hj0', hey⟩ := forms y hy
       have ex' : L * x / A.max' hne = L / k * j := by
         rw [hex, Nat.mul_div_cancel _ hMpos]
       have ey' : L * y / A.max' hne = L / k' * j' := by
         rw [hey, Nat.mul_div_cancel _ hMpos]
       simp only [ex', ey'] at hc
       have h1 := (H1 k hk j hj hj0).2
       have h2 := (H1 k' hk' j' hj' hj0').2
       rw [hc] at h1
       have hvw : L / k * j ≠ L / k' * j' := by
         intro h
         apply hxy
         apply Nat.eq_of_mul_eq_mul_left hLpos
         rw [hex, hey, h]
       have hgcd : (L / k * j).gcd (L / k' * j') * A.max' hne = L * x.gcd y := by
         have h := Nat.gcd_mul_left L x y
         rw [hex, hey, Nat.gcd_mul_right] at h
         exact h
       have hxA := (Finset.mem_erase.mp hx).2
       have hyA := (Finset.mem_erase.mp hy).2
       rcases H2 _ (H1 k' hk' j' hj' hj0').1 _ h1 _ h2 hvw with h | h
       · refine ⟨x, hxA, y, hyA, key x y ?_⟩
         rw [hn]
         have h3 := Nat.mul_le_mul_right (A.max' hne) h
         have h5 : L * (x.gcd y * n) ≤ L * x := by
           calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring
             _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]
             _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring
             _ ≤ L / k * j * A.max' hne := h3
             _ = L * x := hex.symm
         exact Nat.le_of_mul_le_mul_left h5 hLpos
       · refine ⟨y, hyA, x, hxA, key y x ?_⟩
         rw [hn, Nat.gcd_comm]
         have h3 := Nat.mul_le_mul_right (A.max' hne) h
         have h5 : L * (x.gcd y * n) ≤ L * y := by
           calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring
             _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]
             _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring
             _ ≤ L / k' * j' * A.max' hne := h3
             _ = L * y := hey.symm
         exact Nat.le_of_mul_le_mul_left h5 hLpos

   targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 15–118 at d2b3cf021906 ↗

   1. general.hpos have (0 : ℕ) < A.card routine: omega

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

      Lean, line 24

          have hpos : 0 < A.card := by omega

      targets/erdos-402/nodes/variant-77918742/Proof.lean, line 24 at d2b3cf021906 ↗

   2. general.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 25

          have hne : A.Nonempty := Finset.card_pos.mp hpos

      targets/erdos-402/nodes/variant-77918742/Proof.lean, line 25 at d2b3cf021906 ↗

   3. general.key have ∀ (a b : ℕ), a.gcd b * A.card ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with key : ∀ (a b : ℕ), a.gcd b * A.card ≤ 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 26–29

          have key : ∀ a b : ℕ, a.gcd b * A.card ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
            intro a b h
            rw [le_div_iff₀ (by exact_mod_cast hpos)]
            exact_mod_cast h

      targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 26–29 at d2b3cf021906 ↗

   4. general.hM have A.max' hne ∈ A

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

      Uses library Finset.max'_mem.

      Lean, line 30

          have hM : A.max' hne ∈ A := Finset.max'_mem A hne

      targets/erdos-402/nodes/variant-77918742/Proof.lean, line 30 at d2b3cf021906 ↗

   5. general.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 31

          have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))

      targets/erdos-402/nodes/variant-77918742/Proof.lean, line 31 at d2b3cf021906 ↗

   6. general.s6 case

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

      Uses library Exists.intro Existential introduction. .

      Lean, lines 33–34

          · obtain ⟨x, hx, h⟩ := hw
            exact ⟨_, hM, x, hx, key _ x (by rw [hn]; exact h)⟩

      targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 33–34 at d2b3cf021906 ↗

      1. general.s6.s1 obtain ∃ x ∈ A, (A.max' hne).gcd x * n ≤ A.max' hne

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

         Lean, line 33

             · obtain ⟨x, hx, h⟩ := hw

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 33 at d2b3cf021906 ↗

   7. general.forms have ∀ x ∈ A.erase (A.max' hne), ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with forms : ∀ x ∈ A.erase (A.max' hne), ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne.

      Uses library Finset.mem_erase, Exists.intro Existential introduction. .

      Lean, lines 36–66

          have forms : ∀ x ∈ A.erase (A.max' hne), ∃ k j, k < n ∧ j < k ∧ 0 < j ∧
              L * x = L / k * j * A.max' hne := by
            intro x hx
            rw [Finset.mem_erase] at hx
            have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))
            have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
            have hg := hw x hx.2
            obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
            obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
            obtain ⟨g, hgd⟩ : ∃ g, (A.max' hne).gcd x = g := ⟨_, rfl⟩
            rw [hgd] at hk hj hg
            have hkN : k < n := by
              by_contra hh
              push_neg at hh
              have := Nat.mul_le_mul_left g hh
              omega
            have hjk : j < k := by
              by_contra hh
              push_neg at hh
              have := Nat.mul_le_mul_left g hh
              omega
            have hj1 : 0 < j := by
              rcases Nat.eq_zero_or_pos j with h | h
              · subst h
                omega
              · exact h
            refine ⟨k, j, hkN, hjk, hj1, ?_⟩
            have hLk := hL k hkN (by omega)
            rw [hj, hk]
            calc L * (g * j) = (L / k * k) * (g * j) := by rw [hLk]
              _ = L / k * j * (g * k) := by ring

      targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 36–66 at d2b3cf021906 ↗

      1. general.forms.hxpos have (0 : ℕ) < x

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with hxpos : (0 : ℕ) < x.

         Uses library Nat.pos_of_ne_zero.

         Lean, line 40

               have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 40 at d2b3cf021906 ↗

      2. general.forms.hlt have x < A.max' hne

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with hlt : x < A.max' hne.

         Uses library lt_of_le_of_ne, Finset.le_max'.

         Lean, line 41

               have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 41 at d2b3cf021906 ↗

      3. general.forms.hg have A.max' hne < (A.max' hne).gcd x * n

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with hg : A.max' hne < (A.max' hne).gcd x * n.

         Lean, line 42

               have hg := hw x hx.2

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 42 at d2b3cf021906 ↗

      4. general.forms.s4 obtain (A.max' hne).gcd x ∣ A.max' hne

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.

         Uses library Nat.gcd_dvd_left.

         Lean, line 43

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

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 43 at d2b3cf021906 ↗

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

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.

         Uses library Nat.gcd_dvd_right.

         Lean, line 44

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

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 44 at d2b3cf021906 ↗

      6. general.forms.s6 obtain ∃ (g : ℕ), (A.max' hne).gcd x = g

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with g : ℕ, hgd : (A.max' hne).gcd x = g.

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

         Lean, line 45

               obtain ⟨g, hgd⟩ : ∃ g, (A.max' hne).gcd x = g := ⟨_, rfl⟩

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 45 at d2b3cf021906 ↗

      7. general.forms.hkN have k < n

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with hkN : k < n.

         Lean, lines 47–51

               have hkN : k < n := by
                 by_contra hh
                 push_neg at hh
                 have := Nat.mul_le_mul_left g hh
                 omega

         targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 47–51 at d2b3cf021906 ↗

         1. general.forms.hkN.this have g * n ≤ g * k

            Leaves False, with this : g * n ≤ g * k.

            Uses library Nat.mul_le_mul_left.

            Lean, line 50

                    have := Nat.mul_le_mul_left g hh

            targets/erdos-402/nodes/variant-77918742/Proof.lean, line 50 at d2b3cf021906 ↗

      8. general.forms.hjk have j < k

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with hjk : j < k.

         Lean, lines 52–56

               have hjk : j < k := by
                 by_contra hh
                 push_neg at hh
                 have := Nat.mul_le_mul_left g hh
                 omega

         targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 52–56 at d2b3cf021906 ↗

         1. general.forms.hjk.this have g * k ≤ g * j

            Leaves False, with this : g * k ≤ g * j.

            Uses library Nat.mul_le_mul_left.

            Lean, line 55

                    have := Nat.mul_le_mul_left g hh

            targets/erdos-402/nodes/variant-77918742/Proof.lean, line 55 at d2b3cf021906 ↗

      9. general.forms.hj1 have (0 : ℕ) < j

         Leaves ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne, with hj1 : (0 : ℕ) < j.

         Uses library Nat.eq_zero_or_pos.

         Lean, lines 57–61

               have hj1 : 0 < j := by
                 rcases Nat.eq_zero_or_pos j with h | h
                 · subst h
                   omega
                 · exact h

         targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 57–61 at d2b3cf021906 ↗

         1. general.forms.hj1.s1 case

            Leaves (0 : ℕ) < j.

            Lean, lines 59–60

                    · subst h
                      omega

            targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 59–60 at d2b3cf021906 ↗

         2. general.forms.hj1.s2 case

            Leaves (0 : ℕ) < j.

            Lean, line 61

                    · exact h

            targets/erdos-402/nodes/variant-77918742/Proof.lean, line 61 at d2b3cf021906 ↗

      10. general.forms.hLk have L / k * k = L

          Leaves L * x = L / k * j * A.max' hne, with hLk : L / k * k = L.

          Lean, line 63

                have hLk := hL k hkN (by omega)

          targets/erdos-402/nodes/variant-77918742/Proof.lean, line 63 at d2b3cf021906 ↗

      11. general.forms.s11 calc L * (g * j) = L / k * k * (g * j)

          Closes the goal.

          Lean, line 65

                calc L * (g * j) = (L / k * k) * (g * j) := by rw [hLk]

          targets/erdos-402/nodes/variant-77918742/Proof.lean, line 65 at d2b3cf021906 ↗

      12. general.forms.s12 calc routine: ring

          Closes the goal.

          Lean, line 66

                  _ = L / k * j * (g * k) := by ring

          targets/erdos-402/nodes/variant-77918742/Proof.lean, line 66 at d2b3cf021906 ↗

   8. general.hcard have (A.erase (A.max' hne)).card = n - (1 : ℕ)

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcard : (A.erase (A.max' hne)).card = n - (1 : ℕ).

      Uses library Finset.card_erase_of_mem $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. .

      Lean, lines 67–68

          have hcard : (A.erase (A.max' hne)).card = n - 1 := by
            rw [Finset.card_erase_of_mem hM, hn]

      targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 67–68 at d2b3cf021906 ↗

   9. general.hmaps have ∀ x ∈ A.erase (A.max' hne), List.findIdx (fun (l : List ℕ) => decide (L * x / A.max' hne ∈ l)) cls ∈ Finset.range (n - (2 : ℕ))

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase (A.max' hne), List.findIdx (fun (l : List ℕ) => decide (L * x / A.max' hne ∈ l)) cls ∈ Finset.range (n - (2 : ℕ)).

      Uses library Decidable.decide Converts a decidable proposition into a Bool. , Finset.range range n is the set of natural numbers less than n. , Finset.mem_range, Nat.mul_div_cancel.

      Lean, lines 69–74

          have hmaps : ∀ x ∈ A.erase (A.max' hne),
              cls.findIdx (fun l => decide (L * x / A.max' hne ∈ l)) ∈ Finset.range (n - 2) := by
            intro x hx
            obtain ⟨k, j, hk, hj, hj0, he⟩ := forms x hx
            rw [Finset.mem_range, he, Nat.mul_div_cancel _ hMpos]
            exact (H1 k hk j hj hj0).1

      targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 69–74 at d2b3cf021906 ↗

      1. general.hmaps.s1 obtain ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne

         Leaves List.findIdx (fun (l : List ℕ) => decide (L * x / A.max' hne ∈ l)) cls ∈ Finset.range (n - (2 : ℕ)), with k : ℕ, j : ℕ, hk : k < n, hj : j < k, hj0 : (0 : ℕ) < j, he : L * x = L / k * j * A.max' hne.

         Lean, line 72

               obtain ⟨k, j, hk, hj, hj0, he⟩ := forms x hx

         targets/erdos-402/nodes/variant-77918742/Proof.lean, line 72 at d2b3cf021906 ↗

   10. general.s10 obtain ∃ x ∈ A.erase (A.max' hne), ∃ y ∈ A.erase (A.max' hne), x ≠ y ∧ List.findIdx (fun (l : List ℕ) => decide (L * x / A.max' hne ∈ l)) cls = List.findIdx (fun (l : List ℕ) => decide (L * y / A.max' hne ∈ l)) cls

       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, hc : List.findIdx (fun (l : List ℕ) => decide (L * x / A.max' hne ∈ l)) cls = List.findIdx (fun (l : List ℕ) => decide (L * y / A.max' hne ∈ l)) cls.

       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. , Finset.card_range.

       Lean, lines 75–76

           obtain ⟨x, hx, y, hy, hxy, hc⟩ :=
             Finset.exists_ne_map_eq_of_card_lt_of_maps_to (by rw [hcard, Finset.card_range]; omega) hmaps

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 75–76 at d2b3cf021906 ↗

   11. general.s11 obtain ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * x = L / k * j * A.max' hne

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with k : ℕ, j : ℕ, hk : k < n, hj : j < k, hj0 : (0 : ℕ) < j, hex : L * x = L / k * j * A.max' hne.

       Lean, line 77

           obtain ⟨k, j, hk, hj, hj0, hex⟩ := forms x hx

       targets/erdos-402/nodes/variant-77918742/Proof.lean, line 77 at d2b3cf021906 ↗

   12. general.s12 obtain ∃ (k : ℕ) (j : ℕ), k < n ∧ j < k ∧ (0 : ℕ) < j ∧ L * y = L / k * j * A.max' hne

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with k' : ℕ, j' : ℕ, hk' : k' < n, hj' : j' < k', hj0' : (0 : ℕ) < j', hey : L * y = L / k' * j' * A.max' hne.

       Lean, line 78

           obtain ⟨k', j', hk', hj', hj0', hey⟩ := forms y hy

       targets/erdos-402/nodes/variant-77918742/Proof.lean, line 78 at d2b3cf021906 ↗

   13. general.ex' have L * x / A.max' hne = L / k * j

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with ex' : L * x / A.max' hne = L / k * j.

       Uses library Nat.mul_div_cancel.

       Lean, lines 79–80

           have ex' : L * x / A.max' hne = L / k * j := by
             rw [hex, Nat.mul_div_cancel _ hMpos]

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 79–80 at d2b3cf021906 ↗

   14. general.ey' have L * y / A.max' hne = L / k' * j'

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with ey' : L * y / A.max' hne = L / k' * j'.

       Uses library Nat.mul_div_cancel.

       Lean, lines 81–82

           have ey' : L * y / A.max' hne = L / k' * j' := by
             rw [hey, Nat.mul_div_cancel _ hMpos]

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 81–82 at d2b3cf021906 ↗

   15. general.h1 have L / k * j ∈ cls.getD (List.findIdx (fun (l : List ℕ) => decide (L / k * j ∈ l)) cls) []

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h1 : L / k * j ∈ cls.getD (List.findIdx (fun (l : List ℕ) => decide (L / k * j ∈ l)) cls) [].

       Lean, line 84

           have h1 := (H1 k hk j hj hj0).2

       targets/erdos-402/nodes/variant-77918742/Proof.lean, line 84 at d2b3cf021906 ↗

   16. general.h2 have L / k' * j' ∈ cls.getD (List.findIdx (fun (l : List ℕ) => decide (L / k' * j' ∈ l)) cls) []

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h2 : L / k' * j' ∈ cls.getD (List.findIdx (fun (l : List ℕ) => decide (L / k' * j' ∈ l)) cls) [].

       Lean, line 85

           have h2 := (H1 k' hk' j' hj' hj0').2

       targets/erdos-402/nodes/variant-77918742/Proof.lean, line 85 at d2b3cf021906 ↗

   17. general.hvw have L / k * j ≠ L / k' * j'

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hvw : L / k * j ≠ L / k' * j'.

       Uses library Nat.eq_of_mul_eq_mul_left.

       Lean, lines 87–91

           have hvw : L / k * j ≠ L / k' * j' := by
             intro h
             apply hxy
             apply Nat.eq_of_mul_eq_mul_left hLpos
             rw [hex, hey, h]

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 87–91 at d2b3cf021906 ↗

   18. general.hgcd have (L / k * j).gcd (L / k' * j') * A.max' hne = L * x.gcd y

       Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgcd : (L / k * j).gcd (L / k' * j') * A.max' hne = L * x.gcd y.

       Uses library Nat.gcd_mul_right.

       Lean, lines 92–95

           have hgcd : (L / k * j).gcd (L / k' * j') * A.max' hne = L * x.gcd y := by
             have h := Nat.gcd_mul_left L x y
             rw [hex, hey, Nat.gcd_mul_right] at h
             exact h

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 92–95 at d2b3cf021906 ↗

       1. general.hgcd.h have (L * x).gcd (L * y) = L * x.gcd y

          Leaves (L / k * j).gcd (L / k' * j') * A.max' hne = L * x.gcd y, with h : (L * x).gcd (L * y) = L * x.gcd y.

          Uses library Nat.gcd_mul_left.

          Lean, line 93

                have h := Nat.gcd_mul_left L x y

          targets/erdos-402/nodes/variant-77918742/Proof.lean, line 93 at d2b3cf021906 ↗

   19. general.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 96

           have hxA := (Finset.mem_erase.mp hx).2

       targets/erdos-402/nodes/variant-77918742/Proof.lean, line 96 at d2b3cf021906 ↗

   20. general.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 97

           have hyA := (Finset.mem_erase.mp hy).2

       targets/erdos-402/nodes/variant-77918742/Proof.lean, line 97 at d2b3cf021906 ↗

   21. general.s21 case

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

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

       Lean, lines 99–108

           · refine ⟨x, hxA, y, hyA, key x y ?_⟩
             rw [hn]
             have h3 := Nat.mul_le_mul_right (A.max' hne) h
             have h5 : L * (x.gcd y * n) ≤ L * x := by
               calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring
                 _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]
                 _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring
                 _ ≤ L / k * j * A.max' hne := h3
                 _ = L * x := hex.symm
             exact Nat.le_of_mul_le_mul_left h5 hLpos

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 99–108 at d2b3cf021906 ↗

       1. general.s21.h3 have n * (L / k * j).gcd (L / k' * j') * A.max' hne ≤ L / k * j * A.max' hne

          Leaves x.gcd y * n ≤ x, with h3 : n * (L / k * j).gcd (L / k' * j') * A.max' hne ≤ L / k * j * A.max' hne.

          Uses library Nat.mul_le_mul_right.

          Lean, line 101

                have h3 := Nat.mul_le_mul_right (A.max' hne) h

          targets/erdos-402/nodes/variant-77918742/Proof.lean, line 101 at d2b3cf021906 ↗

       2. general.s21.h5 have L * (x.gcd y * n) ≤ L * x

          Leaves x.gcd y * n ≤ x, with h5 : L * (x.gcd y * n) ≤ L * x.

          Lean, lines 102–107

                have h5 : L * (x.gcd y * n) ≤ L * x := by
                  calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring
                    _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]
                    _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring
                    _ ≤ L / k * j * A.max' hne := h3
                    _ = L * x := hex.symm

          targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 102–107 at d2b3cf021906 ↗

          1. general.s21.h5.s1 calc L * (x.gcd y * n) = n * (L * x.gcd y) routine: ring

             Closes the goal.

             Lean, line 103

                     calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 103 at d2b3cf021906 ↗

          2. general.s21.h5.s2 calc

             Closes the goal.

             Lean, line 104

                       _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 104 at d2b3cf021906 ↗

          3. general.s21.h5.s3 calc routine: ring

             Closes the goal.

             Lean, line 105

                       _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 105 at d2b3cf021906 ↗

          4. general.s21.h5.s4 calc n * (L / k * j).gcd (L / k' * j') * A.max' hne ≤ L / k * j * A.max' hne

             Closes the goal.

             Lean, line 106

                       _ ≤ L / k * j * A.max' hne := h3

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 106 at d2b3cf021906 ↗

          5. general.s21.h5.s5 calc L / k * j * A.max' hne = L * x

             Closes the goal.

             Lean, line 107

                       _ = L * x := hex.symm

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 107 at d2b3cf021906 ↗

   22. general.s22 case

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

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

       Lean, lines 109–118

           · refine ⟨y, hyA, x, hxA, key y x ?_⟩
             rw [hn, Nat.gcd_comm]
             have h3 := Nat.mul_le_mul_right (A.max' hne) h
             have h5 : L * (x.gcd y * n) ≤ L * y := by
               calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring
                 _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]
                 _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring
                 _ ≤ L / k' * j' * A.max' hne := h3
                 _ = L * y := hey.symm
             exact Nat.le_of_mul_le_mul_left h5 hLpos

       targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 109–118 at d2b3cf021906 ↗

       1. general.s22.h3 have n * (L / k * j).gcd (L / k' * j') * A.max' hne ≤ L / k' * j' * A.max' hne

          Leaves x.gcd y * n ≤ y, with h3 : n * (L / k * j).gcd (L / k' * j') * A.max' hne ≤ L / k' * j' * A.max' hne.

          Uses library Nat.mul_le_mul_right.

          Lean, line 111

                have h3 := Nat.mul_le_mul_right (A.max' hne) h

          targets/erdos-402/nodes/variant-77918742/Proof.lean, line 111 at d2b3cf021906 ↗

       2. general.s22.h5 have L * (x.gcd y * n) ≤ L * y

          Leaves x.gcd y * n ≤ y, with h5 : L * (x.gcd y * n) ≤ L * y.

          Lean, lines 112–117

                have h5 : L * (x.gcd y * n) ≤ L * y := by
                  calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring
                    _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]
                    _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring
                    _ ≤ L / k' * j' * A.max' hne := h3
                    _ = L * y := hey.symm

          targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 112–117 at d2b3cf021906 ↗

          1. general.s22.h5.s1 calc L * (x.gcd y * n) = n * (L * x.gcd y) routine: ring

             Closes the goal.

             Lean, line 113

                     calc L * (x.gcd y * n) = n * (L * x.gcd y) := by ring

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 113 at d2b3cf021906 ↗

          2. general.s22.h5.s2 calc

             Closes the goal.

             Lean, line 114

                       _ = n * ((L / k * j).gcd (L / k' * j') * A.max' hne) := by rw [hgcd]

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 114 at d2b3cf021906 ↗

          3. general.s22.h5.s3 calc routine: ring

             Closes the goal.

             Lean, line 115

                       _ = n * (L / k * j).gcd (L / k' * j') * A.max' hne := by ring

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 115 at d2b3cf021906 ↗

          4. general.s22.h5.s4 calc n * (L / k * j).gcd (L / k' * j') * A.max' hne ≤ L / k' * j' * A.max' hne

             Closes the goal.

             Lean, line 116

                       _ ≤ L / k' * j' * A.max' hne := h3

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 116 at d2b3cf021906 ↗

          5. general.s22.h5.s5 calc L / k' * j' * A.max' hne = L * y

             Closes the goal.

             Lean, line 117

                       _ = L * y := hey.symm

             targets/erdos-402/nodes/variant-77918742/Proof.lean, line 117 at d2b3cf021906 ↗

2. s2 obtain ∃ (n : ℕ), A.card = n

   Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with n : ℕ, hn : A.card = n.

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

   Lean, line 120

     obtain ⟨n, hn⟩ : ∃ n, A.card = n := ⟨_, rfl⟩

   targets/erdos-402/nodes/variant-77918742/Proof.lean, line 120 at d2b3cf021906 ↗

3. h1 have (1 : ℕ) ≤ n

   Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h1 : (1 : ℕ) ≤ n.

   Uses library Finset.card_pos.

   Lean, line 121

     have h1 : 1 ≤ n := by rw [← hn]; exact Finset.card_pos.mpr hne

   targets/erdos-402/nodes/variant-77918742/Proof.lean, line 121 at d2b3cf021906 ↗

4. hN have n ≤ (24 : ℕ) routine: omega

   Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hN : n ≤ (24 : ℕ).

   Lean, line 122

     have hN : n ≤ 24 := by omega

   targets/erdos-402/nodes/variant-77918742/Proof.lean, line 122 at d2b3cf021906 ↗

5. s5 case

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

   Uses library Exists.intro Existential introduction. .

   Lean, lines 124–125

     · obtain ⟨a, rfl⟩ := Finset.card_eq_one.mp hn
       exact ⟨a, by simp, a, by simp, by simp⟩

   targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 124–125 at d2b3cf021906 ↗

   1. s5.s1 obtain printed form did not read back: shown as its Lean lines only

        · obtain ⟨a, rfl⟩ := Finset.card_eq_one.mp hn

      targets/erdos-402/nodes/variant-77918742/Proof.lean, line 124 at d2b3cf021906 ↗

6. s6 case

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

   Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

   Lean, lines 126–127

     · exact general 2 1 [] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
         (by decide +kernel) A hA hn

   targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 126–127 at d2b3cf021906 ↗

7. s7 case

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

   Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

   Lean, lines 128–129

     · exact general 3 2 [[1]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
         (by decide +kernel) A hA hn

   targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 128–129 at d2b3cf021906 ↗

8. s8 case

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

   Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

   Lean, lines 130–131

     · exact general 4 6 [[3, 4], [2]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
         (by decide +kernel) A hA hn

   targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 130–131 at d2b3cf021906 ↗

9. s9 case

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

   Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

   Lean, lines 132–133

     · exact general 5 12 [[6], [3, 8], [4, 9]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
         (by decide +kernel) A hA hn

   targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 132–133 at d2b3cf021906 ↗

10. s10 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 134–135

      · exact general 6 60 [[20, 24, 45], [12], [15, 40, 48], [30, 36]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 134–135 at d2b3cf021906 ↗

11. s11 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 136–137

      · exact general 7 60 [[15, 36, 40], [30], [20, 48], [12, 45, 50], [10, 24]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 136–137 at d2b3cf021906 ↗

12. s12 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 138–139

      · exact general 8 420 [[84, 280, 360], [60, 168, 315, 350], [105, 180, 336], [210, 240], [70, 120, 252], [140, 300]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 138–139 at d2b3cf021906 ↗

13. s13 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 140–141

      · exact general 9 840 [[210, 480, 504, 700], [280, 525, 672, 720], [105, 240], [120, 315, 336], [168, 560, 600, 630], [420], [140, 360, 735]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 140–141 at d2b3cf021906 ↗

14. s14 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 142–143

      · exact general 10 2520 [[630, 2240], [1260, 1800, 1960], [360, 945, 1008, 1120], [504, 1080, 1680, 2205], [420, 1400, 1440, 1512], [840, 1575, 2016, 2160], [315, 560, 2100], [280, 720, 1890]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 142–143 at d2b3cf021906 ↗

15. s15 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 144–145

      · exact general 11 2520 [[360, 756, 1575, 1680], [1260], [315, 720, 1120, 1512], [840, 1800, 2016], [630, 1080, 1400, 1764], [280, 1008, 2100, 2205], [252, 560, 945, 2160], [504, 1890, 2240], [420, 1440, 1960, 2268]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 144–145 at d2b3cf021906 ↗

16. s16 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 146–147

      · exact general 12 27720 [[3080, 7560, 11088, 17325], [6930, 15400, 15840, 16632, 20160], [9240, 15120, 19404], [4620, 7920, 12600, 22176], [5544, 10080, 10395, 24640], [2520, 12320, 19800, 20790], [2772, 5040, 11880], [3465, 6160, 17640, 23100, 23760, 24948], [3960, 8316, 18480, 24255, 25200], [13860, 21560, 22680]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 146–147 at d2b3cf021906 ↗

17. s17 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 148–149

      · exact general 13 27720 [[13860, 24640, 25200], [5544, 10395, 15120, 15400, 16170], [2310, 7920, 8316, 10080], [3465, 7560, 11088, 21560, 25410], [3080, 5040, 11550, 11880, 22176, 24255], [2520, 18480, 19800], [9240, 12600, 19404], [3960, 6160, 16632, 22680, 23100], [4620, 17325, 17640, 23760, 24948], [6930, 12320, 20160], [2772, 15840, 20790]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 148–149 at d2b3cf021906 ↗

18. s18 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 150–151

      · exact general 14 360360 [[32760, 102960, 110880, 270270, 320320], [90090, 163800, 194040, 288288], [30030, 138600, 144144, 154440, 196560, 280280], [180180, 229320, 332640], [36036, 55440, 150150, 262080], [27720, 65520, 200200, 205920, 216216, 330330], [51480, 80080, 108108, 131040, 166320, 300300], [60060, 225225, 249480, 252252, 327600], [45045, 83160, 240240, 257400], [40040, 98280, 210210, 221760, 324324], [120120, 277200, 308880, 315315], [72072, 135135, 160160, 294840, 304920]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 150–151 at d2b3cf021906 ↗

19. s19 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 152–153

      · exact general 15 360360 [[32760, 80080, 150150, 154440, 277200, 288288], [180180, 294840, 304920], [51480, 138600, 280280, 324324, 327600], [25740, 83160, 163800, 240240], [36036, 55440, 205920, 270270], [60060, 110880, 216216, 225225, 334620], [27720, 98280, 102960, 200200, 210210], [45045, 65520, 160160, 252252, 257400, 332640], [40040, 135135, 144144, 249480, 262080, 283140, 300300], [72072, 77220, 166320, 229320, 330330], [90090, 131040, 194040, 231660, 320320], [120120, 221760, 308880], [30030, 108108, 128700, 196560, 315315]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 152–153 at d2b3cf021906 ↗

20. s20 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 154–155

      · exact general 16 360360 [[32760, 48048, 110880, 225225, 280280, 308880, 324324], [30030, 65520, 108108, 166320, 200200, 205920, 315315, 336336], [60060, 131040, 216216, 277200], [120120, 231660], [45045, 55440, 96096, 154440, 262080, 300300], [72072, 138600, 229320, 283140], [90090, 192192, 194040, 257400], [36036, 98280, 128700, 240240, 249480], [25740, 80080, 83160, 168168, 196560, 330330], [40040, 77220, 144144, 210210, 221760, 327600], [180180, 264264, 320320], [51480, 135135, 163800, 288288, 304920], [27720, 102960, 270270, 312312], [24024, 150150, 160160, 252252, 294840, 332640, 334620]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 154–155 at d2b3cf021906 ↗

21. s21 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 156–157

      · exact general 17 720720 [[72072, 160160, 262080, 308880, 450450, 665280], [360360, 554400, 589680, 624624], [144144, 257400, 320320, 420420, 495495], [90090, 277200, 336336, 640640, 669240], [102960, 192192, 327600, 540540], [45045, 205920, 432432], [60060, 196560, 288288, 315315, 400400, 443520], [120120, 166320, 393120, 405405, 514800, 672672], [80080, 131040, 270270, 411840, 498960, 504504, 528528], [180180, 332640, 384384, 458640], [48048, 110880, 225225, 463320, 655200, 660660], [65520, 154440, 576576, 600600, 609840, 630630], [51480, 96096, 135135, 221760, 300300, 560560, 648648], [240240, 388080, 524160, 617760, 675675], [55440, 216216, 480480, 566280, 585585]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 156–157 at d2b3cf021906 ↗

22. s22 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 158–159

      · exact general 18 12252240 [[2450448, 2882880, 4375800, 5360355, 6683040, 8482320, 10890880, 11231220], [816816, 2227680, 3769920, 7207200, 9189180, 9626760], [3063060, 5654880, 6534528, 7796880, 9369360], [4084080, 6486480, 10720710, 11377080], [1531530, 2162160, 5445440, 5717712, 8751600, 8910720, 11027016], [6126120, 11531520], [875160, 1884960, 3341520, 5105100, 6891885, 9801792, 10810800], [720720, 2722720, 4712400, 5250960, 10618608, 11138400, 11486475], [1021020, 3603600, 3675672, 8423415, 9529520, 10024560, 11309760], [1113840, 1633632, 4324320, 6597360, 7001280, 7657650], [1750320, 3267264, 4594590, 6806800, 7539840, 7927920], [2042040, 5045040, 10367280, 10501920, 11435424], [1361360, 3500640, 3828825, 5765760, 7351344, 9424800], [1225224, 2827440, 7876440, 8168160, 8648640, 9954945], [765765, 2625480, 4900896, 5569200, 7147140, 10090080], [942480, 1441440, 2297295, 4455360, 8576568, 8984976, 10210200]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 158–159 at d2b3cf021906 ↗

23. s23 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 160–161

      · exact general 19 12252240 [[4084080, 5360355, 10090080], [680680, 2227680, 2827440, 3828825, 4324320, 7876440, 8984976], [1225224, 5445440, 5654880, 6891885, 7796880, 8648640, 8751600, 10618608], [3063060, 7539840, 8848840, 10810800], [1361360, 3603600, 5717712, 8910720, 9189180, 9626760], [875160, 3675672, 4712400, 5045040, 8168160, 11486475], [2450448, 5105100, 6597360, 7001280, 7927920, 9954945, 11138400, 11571560], [1113840, 1441440, 4764760, 5250960, 7657650, 9801792, 11231220], [1021020, 2162160, 4900896, 6806800, 8423415, 8482320, 11377080], [1750320, 2297295, 2882880, 3403400, 6534528, 6683040, 7147140, 11309760], [942480, 2722720, 3341520, 5765760, 10720710, 11027016], [2042040, 10501920, 11435424, 11531520], [1531530, 4375800, 4455360, 7351344, 7487480, 9369360], [720720, 1884960, 2625480, 3267264, 10024560, 10210200], [765765, 1633632, 3769920, 5569200, 7207200, 9529520], [816816, 3500640, 4594590, 6486480, 8576568, 10367280, 10890880], [6126120, 9424800]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 160–161 at d2b3cf021906 ↗

24. s24 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 162–163

      · exact general 20 232792560 [[116396280, 196035840, 196978320], [21162960, 27387360, 69837768, 96996900, 101846745, 107442720, 110270160, 216164520, 219859640], [46558512, 103463360, 135795660, 159279120, 160044885, 166280400, 190466640, 205405200], [33256080, 84651840, 87297210, 123243120, 147026880, 193993800, 217273056], [16628040, 36756720, 72747675, 155195040, 161164080, 178017840], [58198140, 89535600, 98017920, 150630480, 181060880, 201753552, 211629600], [29099070, 62078016, 90530440, 109549440, 179071200, 183783600, 199536480, 209513304], [77597520, 162954792, 208288080, 218243025, 219098880], [19399380, 35814240, 41081040, 129329200, 171531360, 182908440, 186234048], [12252240, 43648605, 93117024, 143256960, 148140720, 164324160], [25865840, 105814800, 122522400, 125349840, 133024320, 139675536, 191711520, 213393180], [23279256, 42325920, 53721360, 61261200, 95855760, 189143955, 206926720], [38798760, 49008960, 136936800, 149652360, 169303680, 203693490], [15519504, 54774720, 73513440, 142262120, 145495350, 214885440], [17907120, 31039008, 64664600, 99768240, 134774640], [14549535, 51731680, 63488880, 82162080, 83140200, 108636528, 220540320], [12932920, 66512160, 68468400, 85765680, 170714544, 174594420], [13693680, 24504480, 49884120, 71628480, 124156032, 126977760, 130945815, 168127960]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 162–163 at d2b3cf021906 ↗

25. s25 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 164–165

      · exact general 21 232792560 [[12932920, 62078016, 105814800, 109549440, 159279120, 174594420], [13693680, 24504480, 145495350, 148140720, 161164080, 186234048, 216164520, 219859640], [11639628, 72747675, 125349840, 155195040, 190466640], [58198140, 122522400, 181060880, 199536480, 219098880], [16628040, 31039008, 36756720, 64664600, 71628480, 95855760, 218243025, 221152932], [38798760, 54774720, 101846745, 128035908, 143256960, 147026880, 149652360, 201753552, 211629600], [25865840, 87297210, 171531360, 197873676], [17907120, 27387360, 83140200, 139675536, 160044885, 206926720, 208288080], [46558512, 61261200, 90530440, 107442720, 169303680, 182908440, 205405200], [29099070, 41081040, 84651840, 108636528, 110270160, 142262120, 151315164, 179071200], [33256080, 43648605, 73513440, 81477396, 89535600, 103463360, 191711520, 213393180], [21162960, 49884120, 51731680, 98017920, 135795660, 136936800, 189143955, 209513304], [19399380, 53721360, 93117024, 134774640, 166280400, 203693490], [14549535, 42325920, 69837768, 85765680, 123243120, 133024320, 193993800, 214885440, 217273056], [15519504, 63488880, 66512160, 82162080, 129329200, 130945815, 162954792, 183783600], [116396280, 150630480, 196035840], [23279256, 49008960, 68468400, 99768240, 168127960, 170714544], [12252240, 34918884, 35814240, 96996900, 124156032, 126977760, 164324160], [77597520, 104756652, 178017840, 196978320, 220540320]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 164–165 at d2b3cf021906 ↗

26. s26 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 166–167

      · exact general 22 232792560 [[46558512, 68468400, 85765680, 169303680, 199536480, 218243025], [12252240, 34918884, 66512160, 95855760, 143256960, 160044885, 168127960, 211629600, 217273056], [11085360, 69837768, 148140720, 161164080, 189143955, 191711520, 193993800, 220540320], [29099070, 41081040, 49008960, 55426800, 107442720, 124156032, 149652360, 151315164, 213393180, 219859640], [38798760, 122522400, 144109680, 150630480, 186234048], [77597520, 164324160, 190466640, 208288080, 221152932], [12932920, 42325920, 54774720, 88682880, 108636528, 171531360, 174594420, 196978320], [14549535, 24504480, 44341440, 89535600, 90530440, 126977760, 170714544, 197873676, 205405200, 216164520], [21162960, 22170720, 64664600, 87297210, 98017920, 123243120, 179071200, 201753552], [25865840, 71628480, 105814800, 109549440, 110853600, 134774640, 139675536, 203693490], [13693680, 31039008, 53721360, 83140200, 84651840, 101846745, 142262120, 188451120, 196035840, 209513304], [19399380, 27387360, 99768240, 162954792, 183783600, 206926720, 214885440], [15519504, 35814240, 36756720, 72747675, 82162080, 104756652, 133024320, 135795660], [11639628, 49884120, 51731680, 110270160, 145495350, 210621840], [33256080, 62078016, 73513440, 96996900, 128035908, 130945815, 136936800, 181060880], [17907120, 43648605, 61261200, 81477396, 155195040, 182908440], [23279256, 63488880, 103463360, 159279120, 166280400], [58198140, 121938960, 219098880], [16628040, 93117024, 125349840, 129329200, 177365760, 178017840], [116396280, 147026880, 221707200]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 166–167 at d2b3cf021906 ↗

27. s27 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 168–169

      · exact general 23 232792560 [[17907120, 41081040, 66512160, 81477396, 98017920, 170714544, 189143955, 190466640, 193993800], [23279256, 63488880, 103463360, 125349840, 145495350, 147026880, 205405200, 210621840, 216164520], [12252240, 34918884, 42325920, 83140200, 95855760, 142262120, 179071200, 188451120, 217273056], [21162960, 88682880, 101846745, 107442720, 129329200, 182908440, 201753552, 208288080, 209513304, 219098880], [10581480, 53721360, 150630480, 155195040], [116396280, 183783600], [25865840, 72747675, 84651840, 99768240, 151315164, 164324160, 220540320], [15519504, 24504480, 87297210, 90530440, 133024320, 191711520, 196978320, 197873676, 211629600], [46558512, 68468400, 95233320, 110853600, 135795660, 143256960, 160044885, 196035840], [12932920, 35814240, 43648605, 44341440, 105814800, 123243120, 134774640, 162954792], [11639628, 49884120, 51731680, 89535600, 110270160, 136936800, 144109680, 179885160, 218243025], [33256080, 96996900, 128035908, 148140720, 178017840, 206926720], [77597520, 222211080], [11085360, 27387360, 49008960, 69837768, 168127960, 169303680, 203693490], [38798760, 61261200, 82162080, 149652360, 186234048, 201048120, 221707200], [13693680, 31039008, 55426800, 74070360, 171531360, 174594420], [58198140, 124156032, 158722200, 159279120, 161164080, 199536480], [14549535, 22170720, 31744440, 54774720, 64664600, 73513440, 104756652, 108636528, 214885440], [19399380, 85765680, 93117024, 130945815, 137559240, 166280400], [29099070, 36756720, 62078016, 109549440, 121938960, 126977760, 181060880, 221152932], [16628040, 52907400, 71628480, 122522400, 139675536, 177365760, 213393180, 219859640]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 168–169 at d2b3cf021906 ↗

28. s28 case

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

    Uses library Lean.Parser.Tactic.DecideConfig.kernel If true (default: false), then use only kernel reduction when reducing the Decidable instance. .

    Lean, lines 170–171

      · exact general 24 5354228880 [[1784742960, 2834591760, 3099816720, 4655851200, 5019589575, 5110854840], [486748080, 1862340480, 2804596080, 2883046320, 3212537328, 3945221280, 4971783960], [297457160, 629909280, 1163962800, 1972610640, 2007835830, 3059559360, 4118637600, 4380732720, 4640331696], [382444920, 713897184, 944863920, 1127206080, 2095133040, 2230928700, 2944825884, 4164400240, 4350310965, 4844302320, 4867480800, 4942365120], [1070845776, 1396755360, 2536213680, 3123300180, 3650610600, 3681032355, 4409364960, 5056771720], [764889840, 4227022800, 4818805992, 4888643760], [892371480, 931170240, 1690809120, 2433740400, 3442004280, 4551094548, 4997280288, 5039274240, 5099265600], [669278610, 1647455040, 2294669520, 2855588736, 2974571600, 3407236560, 4094410320, 4190266080], [594914320, 1147334760, 1259818560, 2471182560, 2793510720, 3480248772, 4079412480, 4137358680, 4684950270, 5072427360], [334639305, 730122120, 1409007600, 2141691552, 2204682480, 3026303280, 4334375760], [254963280, 845404560, 1673196525, 1889727840, 2082200120, 2560718160, 3163862520, 4283383104], [356948592, 698377680, 973496160, 1274816400, 2409402996, 2818015200, 3779455680, 4759314560, 4908043140], [314954640, 563603040, 1216870200, 1427794368, 1629547920, 2549632800, 3272028760, 3294910080, 4015671660], [2677114440, 3491888400], [1338557220, 2039706240, 2327925600, 2498640144, 2920488480, 3663419760], [232792560, 1189828640, 1460244240, 2519637120, 3011753745, 3824449200, 3926434512, 5086517436], [243374040, 465585120, 1606268664, 2059318800, 2342475135, 2379657280, 3149546400, 3314522640, 3381618240, 4206894120], [535422888, 1019853120, 1235591280, 2190366360, 2254412160, 3259095840, 4461857400], [411863760, 803134332, 1703618280, 1912224600, 3569485920, 4423058640, 4508824320], [446185740, 823727520, 1574773200, 1946992320, 3724680960, 3747960216, 3866943080, 4589339040, 4790625840], [267711444, 509926560, 3346393050, 3893984640, 3957473520, 4530501360, 4724319600], [281801520, 1003917915, 1487285800, 1529779680, 1873980108, 3464501040, 3706773840, 4624106760, 5121436320]] (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel)
          (by decide +kernel) A hA hn

    targets/erdos-402/nodes/variant-77918742/Proof.lean, lines 170–171 at d2b3cf021906 ↗