Konyagin's theorem: points where f is near a rational

Checked by the kernel — an outline of the attested proof below: attestations/000568.json, merge commit 3e4a866f1f30.

Outline of Proof.lean, extracted by the gate at f878b4d44120 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. hfl have (0 : ℤ) ≤ ⌊N⌋

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hfl : (0 : ℤ) ≤ ⌊N⌋.

   Uses library Int.floor_nonneg.

   Lean, line 43

     have hfl : (0 : ℤ) ≤ ⌊N⌋ := Int.floor_nonneg.mpr hN.le

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 43 at 3e4a866f1f30 ↗

2. hsub have S ⊆ Finset.Icc (0 : ℤ) ⌊N⌋

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hsub : S ⊆ Finset.Icc (0 : ℤ) ⌊N⌋.

   Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.mem_Icc, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

   Lean, lines 44–46

     have hsub : S ⊆ Finset.Icc (0 : ℤ) ⌊N⌋ := fun u hu => by
       obtain ⟨a, b⟩ := hS u hu
       exact Finset.mem_Icc.mpr ⟨a, b⟩

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 44–46 at 3e4a866f1f30 ↗

   1. hsub.s1 obtain (0 : ℤ) ≤ u ∧ u ≤ ⌊N⌋

      Leaves u ∈ Finset.Icc (0 : ℤ) ⌊N⌋, with a : (0 : ℤ) ≤ u, b : u ≤ ⌊N⌋.

      Lean, line 45

          obtain ⟨a, b⟩ := hS u hu

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 45 at 3e4a866f1f30 ↗

3. hcardZ have (↑S.card : ℤ) ≤ ⌊N⌋ + (1 : ℤ)

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hcardZ : (↑S.card : ℤ) ≤ ⌊N⌋ + (1 : ℤ).

   Uses library Int.card_Icc.

   Lean, lines 47–50

     have hcardZ : (S.card : ℤ) ≤ ⌊N⌋ + 1 := by
       have := Finset.card_le_card hsub
       rw [Int.card_Icc] at this
       omega

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 47–50 at 3e4a866f1f30 ↗

   1. hcardZ.this have S.card ≤ (Finset.Icc (0 : ℤ) ⌊N⌋).card

      Leaves (↑S.card : ℤ) ≤ ⌊N⌋ + (1 : ℤ), with this : S.card ≤ (Finset.Icc (0 : ℤ) ⌊N⌋).card.

      Uses library Finset.card_le_card.

      Lean, line 48

          have := Finset.card_le_card hsub

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 48 at 3e4a866f1f30 ↗

4. hcard have (↑S.card : ℝ) ≤ N + (1 : ℝ)

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hcard : (↑S.card : ℝ) ≤ N + (1 : ℝ).

   Uses library Int.floor_le.

   Lean, lines 51–54

     have hcard : (S.card : ℝ) ≤ N + 1 := by
       have h' : ((S.card : ℤ) : ℝ) ≤ ((⌊N⌋ + 1 : ℤ) : ℝ) := by exact_mod_cast hcardZ
       push_cast at h'
       linarith [Int.floor_le N]

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 51–54 at 3e4a866f1f30 ↗

   1. hcard.h' have (↑(↑S.card : ℤ) : ℝ) ≤ (↑(⌊N⌋ + (1 : ℤ)) : ℝ)

      Leaves (↑S.card : ℝ) ≤ N + (1 : ℝ), with h' : (↑(↑S.card : ℤ) : ℝ) ≤ (↑(⌊N⌋ + (1 : ℤ)) : ℝ).

      Lean, line 52

          have h' : ((S.card : ℤ) : ℝ) ≤ ((⌊N⌋ + 1 : ℤ) : ℝ) := by exact_mod_cast hcardZ

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 52 at 3e4a866f1f30 ↗

5. hr2 have (4 : ℝ) ≤ (2 : ℝ) * (↑r : ℝ) * lam

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hr2 : (4 : ℝ) ≤ (2 : ℝ) * (↑r : ℝ) * lam.

   Lean, lines 55–57

     have hr2 : (4 : ℝ) ≤ 2 * (r : ℝ) * lam := by
       have : (2 : ℝ) ≤ r := by exact_mod_cast hr
       nlinarith

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 55–57 at 3e4a866f1f30 ↗

   1. hr2.this have (2 : ℝ) ≤ (↑r : ℝ)

      Leaves (4 : ℝ) ≤ (2 : ℝ) * (↑r : ℝ) * lam, with this : (2 : ℝ) ≤ (↑r : ℝ).

      Lean, line 56

          have : (2 : ℝ) ≤ r := by exact_mod_cast hr

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 56 at 3e4a866f1f30 ↗

6. s6 case

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hX : (1 : ℝ) ≤ (65536 : ℝ) * X.

   Lean, lines 59–60

     · have : N ≤ 65536 * N * X := by nlinarith
       linarith

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 59–60 at 3e4a866f1f30 ↗

   1. s6.this have N ≤ (65536 : ℝ) * N * X routine: nlinarith

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with this : N ≤ (65536 : ℝ) * N * X.

      Lean, line 59

        · have : N ≤ 65536 * N * X := by nlinarith

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 59 at 3e4a866f1f30 ↗

7. s7 case

   Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hX : ¬(1 : ℝ) ≤ (65536 : ℝ) * X.

   Uses library Finset.sum_const, Finset.card_range, nsmul_eq_mul.

   Lean, lines 61–261

     · push_neg at hX
       -- the remaining (hard) case, for a scale parameter in `[1, 2)`
       have core : ∀ (N' : ℝ), 0 < N' → ∀ (lam' : ℝ), 1 ≤ lam' → lam' < 2 →
           ∀ (D' : ℝ), 0 < D' → ∀ (D1' : ℝ), 0 < D1' → ∀ (g : ℝ → ℝ),
           ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g →
           (∀ x ∈ Set.Icc (0 : ℝ) N', D' / (2 : ℝ) ≤ |iteratedDeriv r g x|) →
           (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv r g x| ≤ D') →
           (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv (r + (1 : ℕ)) g x| ≤ D1') →
           ∀ (S' : Finset ℤ), (∀ u ∈ S', (0 : ℤ) ≤ u ∧ u ≤ ⌊N'⌋) →
           (∀ u ∈ S', ∃ (v : ℤ) (w : ℕ),
               (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |g (↑u : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ) →
           65536 * ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
               (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ +
               (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) < 1 →
           (↑S'.card : ℝ) < 65536 * N' *
               ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
                 (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ +
               (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) +
             (2 : ℝ) * (↑r : ℝ) * lam' := by
         intro N' hN' lam' hl1' hl2' D' hD' D1' hD1' g hg g1 g2 g3 S' hS' hS2' hlt
         exact erdos_1094__h2__h2__h2__h3__h1__h1__h1 r hr N hN W hW δ hδ lam hlam D_r hDr D_r1 hDr1
           f hf h1 h2 h3 S hS hS2 (not_le.mpr hX) N' hN' lam' hl1' hl2' D' hD' D1' hD1' g hg g1 g2 g3
           S' hS' hS2' hlt
       -- reduction of a general scale `lam` to a scale in `[1, 2)` via residue classes
       set q : ℕ := ⌊lam⌋₊ with hqdef
       have hq1 : 1 ≤ q := Nat.le_floor (by exact_mod_cast hlam)
       have hqpos : (0 : ℝ) < q := by exact_mod_cast hq1
       have hqle : (q : ℝ) ≤ lam := Nat.floor_le (by linarith)
       have hqlt : lam < q + 1 := Nat.lt_floor_add_one lam
       set lam' : ℝ := lam / q with hlam'
       have hl1 : 1 ≤ lam' := by rw [hlam', le_div_iff₀ hqpos]; linarith
       have hl2 : lam' < 2 := by
         rw [hlam', div_lt_iff₀ hqpos]
         have : (1 : ℝ) ≤ q := by exact_mod_cast hq1
         linarith
       have hX0 : 0 ≤ X := by
         rw [hXdef]
         have := hDr.le; have := hDr1.le; have := hδ.le
         have hl0 : 0 ≤ lam := by linarith
         positivity
       have hXinv : (D_r * q ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
           (δ * W ^ (2 : ℕ) / (D_r * q ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ +
           (D_r1 * q ^ (r + 1) * lam' * W ^ (2 : ℕ) / (D_r * q ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹
           = X := by
         have e1 : (q : ℝ) ^ r * lam' ^ r = lam ^ r := by
           rw [← mul_pow, hlam', mul_div_cancel₀ _ hqpos.ne']
         have e2 : D_r1 * q ^ (r + 1) * lam' * W ^ (2 : ℕ) / (D_r * q ^ r)
             = D_r1 * lam * W ^ (2 : ℕ) / D_r := by
           rw [hlam']; field_simp; ring
         rw [hXdef, e2, mul_assoc D_r, e1]
       have hclass : ∀ c ∈ Finset.range q,
           ((S.filter (fun u => (u % (q : ℤ)).toNat = c)).card : ℝ)
             < 65536 * (N / q) * X + 2 * (r : ℝ) * lam' := by
         intro c hc
         have hcq : c < q := Finset.mem_range.mp hc
         set T := S.filter (fun u => (u % (q : ℤ)).toNat = c) with hT
         have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1
         have hmem : ∀ u ∈ T, u ∈ S ∧ u % (q : ℤ) = c := by
           intro u hu
           rw [hT, Finset.mem_filter] at hu
           refine ⟨hu.1, ?_⟩
           have h0 : 0 ≤ u % (q : ℤ) := Int.emod_nonneg _ hqZ.ne'
           omega
         have hdecomp : ∀ u ∈ T, u = c + q * (u / q) := by
           intro u hu
           have := Int.emod_add_mul_ediv u q
           rw [(hmem u hu).2] at this
           omega
         set T' := T.image (fun u => u / (q : ℤ)) with hT'
         have hcardT : T'.card = T.card := by
           apply Finset.card_image_of_injOn
           intro u hu u' hu' huu
           simp only at huu
           rw [hdecomp u hu, hdecomp u' hu', huu]
         have hlam'pos : (4 : ℝ) ≤ 2 * (r : ℝ) * lam' := by
           have : (2 : ℝ) ≤ r := by exact_mod_cast hr
           nlinarith
         have hNq : 0 ≤ 65536 * (N / q) * X := by positivity
         by_cases hNc : (c : ℝ) < N
         · set N' : ℝ := (N - c) / q with hN'
           have hN'pos : 0 < N' := div_pos (by linarith) hqpos
           set g : ℝ → ℝ := fun t => f (c + q * t) with hg
           have hgfun : ∀ k : ℕ, k ≤ r + 1 → ∀ t, iteratedDeriv k g t
               = (q : ℝ) ^ k * iteratedDeriv k f (c + q * t) := by
             intro k hk t
             have hf1 : ContDiff ℝ k (fun z => f (c + z)) := by
               have : ContDiff ℝ k f := hf.of_le (by exact_mod_cast hk)
               exact this.comp (contDiff_const.add contDiff_id)
             have := iteratedDeriv_comp_const_mul hf1 (q : ℝ)
             have h2 := congrFun this t
             try simp only at h2
             rw [show g = fun x => (fun z => f (c + z)) (q * x) from rfl, h2,
               iteratedDeriv_comp_const_add]
           have hgC : ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g :=
             hf.comp (contDiff_const.add (contDiff_const.mul contDiff_id))
           have hIcc : ∀ x ∈ Set.Icc (0 : ℝ) N', (c : ℝ) + q * x ∈ Set.Icc (0 : ℝ) N := by
             intro x hx
             obtain ⟨hx0, hx1⟩ := hx
             constructor
             · positivity
             · have : (q : ℝ) * x ≤ q * N' := mul_le_mul_of_nonneg_left hx1 hqpos.le
               rw [hN', mul_div_cancel₀ _ hqpos.ne'] at this
               linarith
           have hqr : (0 : ℝ) < (q : ℝ) ^ r := pow_pos hqpos r
           have key := core N' hN'pos lam' hl1 hl2 (D_r * q ^ r) (by positivity)
             (D_r1 * q ^ (r + 1)) (by positivity) g hgC
             (by
               intro x hx
               rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
               have := h1 _ (hIcc x hx)
               nlinarith)
             (by
               intro x hx
               rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
               have := h2 _ (hIcc x hx)
               nlinarith)
             (by
               intro x hx
               rw [hgfun (r + 1) le_rfl, abs_mul, abs_of_pos (pow_pos hqpos _)]
               have := h3 _ (hIcc x hx)
               have : (0 : ℝ) < (q : ℝ) ^ (r + 1) := pow_pos hqpos _
               nlinarith)
             T'
             (by
               intro t ht
               rw [hT', Finset.mem_image] at ht
               obtain ⟨u, hu, rfl⟩ := ht
               have huS := (hmem u hu).1
               obtain ⟨hu0, hu1⟩ := hS u huS
               refine ⟨Int.ediv_nonneg hu0 hqZ.le, ?_⟩
               apply Int.le_floor.mpr
               rw [hN', le_div_iff₀ hqpos]
               have hdu := hdecomp u hu
               have hreal : (u : ℝ) = c + q * ((u / q : ℤ) : ℝ) := by
                 have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                 push_cast at this
                 exact this
               have : (u : ℝ) ≤ N := le_trans (by exact_mod_cast hu1) (Int.floor_le N)
               linarith)
             (by
               intro t ht
               rw [hT', Finset.mem_image] at ht
               obtain ⟨u, hu, rfl⟩ := ht
               obtain ⟨v, w, hw0, hwW, hvw⟩ := hS2 u (hmem u hu).1
               refine ⟨v, w, hw0, hwW, ?_⟩
               have hdu := hdecomp u hu
               have hreal : (c : ℝ) + q * ((u / q : ℤ) : ℝ) = u := by
                 have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                 push_cast at this
                 exact this.symm
               simp only [hg, hreal]
               exact hvw)
             (by rw [hXinv]; exact hX)
           rw [hXinv, hcardT] at key
           have : 65536 * N' * X ≤ 65536 * (N / q) * X := by
             apply mul_le_mul_of_nonneg_right _ hX0
             apply mul_le_mul_of_nonneg_left _ (by norm_num)
             rw [hN']
             apply div_le_div_of_nonneg_right _ hqpos.le
             have : (0 : ℝ) ≤ c := by positivity
             linarith
           linarith
         · push_neg at hNc
           -- the class contains at most the single point `c`
           have hle : T.card ≤ 1 := by
             rw [Finset.card_le_one]
             intro u hu u' hu'
             have key : ∀ x ∈ T, x = c := by
               intro x hx
               have hxS := (hmem x hx).1
               obtain ⟨hx0, hx1⟩ := hS x hxS
               have hdx := hdecomp x hx
               have hxN : (x : ℝ) ≤ N := le_trans (by exact_mod_cast hx1) (Int.floor_le N)
               have hxc : x ≤ c := by
                 have : (x : ℝ) ≤ c := le_trans hxN hNc
                 exact_mod_cast this
               have hcq' : (c : ℤ) < q := by exact_mod_cast hcq
               have hdvd : (q : ℤ) ∣ x - c := ⟨x / q, by omega⟩
               have habs : |x - (c : ℤ)| < q := by rw [abs_lt]; constructor <;> omega
               have := Int.eq_zero_of_abs_lt_dvd hdvd habs
               omega
             rw [key u hu, key u' hu']
           have : (T.card : ℝ) ≤ 1 := by exact_mod_cast hle
           linarith
       have hsum : (S.card : ℝ) = ∑ c ∈ Finset.range q,
           ((S.filter (fun u => (u % (q : ℤ)).toNat = c)).card : ℝ) := by
         rw [Finset.card_eq_sum_card_fiberwise (f := fun u => (u % (q : ℤ)).toNat)
           (t := Finset.range q)]
         · push_cast; rfl
         · intro u _
           simp only [Finset.coe_range, Set.mem_Iio]
           have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1
           have h1 := Int.emod_nonneg u hqZ.ne'
           have h2 := Int.emod_lt_of_pos u hqZ
           omega
       have hlt := Finset.sum_lt_sum_of_nonempty (Finset.nonempty_range_iff.mpr (by omega)) hclass
       rw [← hsum, Finset.sum_const, Finset.card_range, nsmul_eq_mul] at hlt
       have : (q : ℝ) * (65536 * (N / q) * X + 2 * (r : ℝ) * lam')
           = 65536 * N * X + 2 * (r : ℝ) * lam := by
         rw [hlam']; field_simp
       linarith

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 61–261 at 3e4a866f1f30 ↗

   1. s7.core have ∀ (N' : ℝ), (0 : ℝ) < N' → ∀ (lam' : ℝ), (1 : ℝ) ≤ lam' → lam' < (2 : ℝ) → ∀ (D' : ℝ), (0 : ℝ) < D' → ∀ (D1' : ℝ), (0 : ℝ) < D1' → ∀ (g : ℝ → ℝ), ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g → (∀ x ∈ Set.Icc (0 : ℝ) N', D' / (2 : ℝ) ≤ |iteratedDeriv r g x|) → (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv r g x| ≤ D') → (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv (r + (1 : ℕ)) g x| ≤ D1') → ∀ (S' : Finset ℤ), (∀ u ∈ S', (0 : ℤ) ≤ u ∧ u ≤ ⌊N'⌋) → (∀ u ∈ S', ∃ (v : ℤ) (w : ℕ), (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |g (↑u : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ) → (65536 : ℝ) * ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) < (1 : ℝ) → (↑S'.card : ℝ) < (65536 : ℝ) * N' * ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) + (2 : ℝ) * (↑r : ℝ) * lam'

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with core : ∀ (N' : ℝ), (0 : ℝ) < N' → ∀ (lam' : ℝ), (1 : ℝ) ≤ lam' → lam' < (2 : ℝ) → ∀ (D' : ℝ), (0 : ℝ) < D' → ∀ (D1' : ℝ), (0 : ℝ) < D1' → ∀ (g : ℝ → ℝ), ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g → (∀ x ∈ Set.Icc (0 : ℝ) N', D' / (2 : ℝ) ≤ |iteratedDeriv r g x|) → (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv r g x| ≤ D') → (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv (r + (1 : ℕ)) g x| ≤ D1') → ∀ (S' : Finset ℤ), (∀ u ∈ S', (0 : ℤ) ≤ u ∧ u ≤ ⌊N'⌋) → (∀ u ∈ S', ∃ (v : ℤ) (w : ℕ), (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |g (↑u : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ) → (65536 : ℝ) * ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) < (1 : ℝ) → (↑S'.card : ℝ) < (65536 : ℝ) * N' * ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) + (2 : ℝ) * (↑r : ℝ) * lam'.

      Uses statements erdos-1094--h2--h2--h2--h3--h1--h1--h1; library ContDiff A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. , WithTop Attach ⊤ to a type. , Set.Icc Icc a b is the left-closed right-closed interval $[a, b]$. , iteratedDeriv The n-th iterated derivative of a function from 𝕜 to F, as a function from 𝕜 to F. , Finset Finset α is the type of finite sets of elements of α. , not_le.

      Lean, lines 63–83

          have core : ∀ (N' : ℝ), 0 < N' → ∀ (lam' : ℝ), 1 ≤ lam' → lam' < 2 →
              ∀ (D' : ℝ), 0 < D' → ∀ (D1' : ℝ), 0 < D1' → ∀ (g : ℝ → ℝ),
              ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g →
              (∀ x ∈ Set.Icc (0 : ℝ) N', D' / (2 : ℝ) ≤ |iteratedDeriv r g x|) →
              (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv r g x| ≤ D') →
              (∀ x ∈ Set.Icc (0 : ℝ) N', |iteratedDeriv (r + (1 : ℕ)) g x| ≤ D1') →
              ∀ (S' : Finset ℤ), (∀ u ∈ S', (0 : ℤ) ≤ u ∧ u ≤ ⌊N'⌋) →
              (∀ u ∈ S', ∃ (v : ℤ) (w : ℕ),
                  (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |g (↑u : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ) →
              65536 * ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
                  (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ +
                  (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) < 1 →
              (↑S'.card : ℝ) < 65536 * N' *
                  ((D' * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
                    (δ * W ^ (2 : ℕ) / (D' * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ +
                  (D1' * lam' * W ^ (2 : ℕ) / D') ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) +
                (2 : ℝ) * (↑r : ℝ) * lam' := by
            intro N' hN' lam' hl1' hl2' D' hD' D1' hD1' g hg g1 g2 g3 S' hS' hS2' hlt
            exact erdos_1094__h2__h2__h2__h3__h1__h1__h1 r hr N hN W hW δ hδ lam hlam D_r hDr D_r1 hDr1
              f hf h1 h2 h3 S hS hS2 (not_le.mpr hX) N' hN' lam' hl1' hl2' D' hD' D1' hD1' g hg g1 g2 g3
              S' hS' hS2' hlt

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 63–83 at 3e4a866f1f30 ↗

   2. s7.hq1 have (1 : ℕ) ≤ q

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hq1 : (1 : ℕ) ≤ q.

      Uses library Nat.le_floor.

      Lean, line 86

          have hq1 : 1 ≤ q := Nat.le_floor (by exact_mod_cast hlam)

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 86 at 3e4a866f1f30 ↗

   3. s7.hqpos have (0 : ℝ) < (↑q : ℝ)

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hqpos : (0 : ℝ) < (↑q : ℝ).

      Lean, line 87

          have hqpos : (0 : ℝ) < q := by exact_mod_cast hq1

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 87 at 3e4a866f1f30 ↗

   4. s7.hqle have (↑q : ℝ) ≤ lam

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hqle : (↑q : ℝ) ≤ lam.

      Uses library Nat.floor_le.

      Lean, line 88

          have hqle : (q : ℝ) ≤ lam := Nat.floor_le (by linarith)

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 88 at 3e4a866f1f30 ↗

   5. s7.hqlt have lam < (↑q : ℝ) + (1 : ℝ)

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hqlt : lam < (↑q : ℝ) + (1 : ℝ).

      Uses library Nat.lt_floor_add_one.

      Lean, line 89

          have hqlt : lam < q + 1 := Nat.lt_floor_add_one lam

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 89 at 3e4a866f1f30 ↗

   6. s7.hl1 have (1 : ℝ) ≤ lam'

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hl1 : (1 : ℝ) ≤ lam'.

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

      Lean, line 91

          have hl1 : 1 ≤ lam' := by rw [hlam', le_div_iff₀ hqpos]; linarith

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 91 at 3e4a866f1f30 ↗

   7. s7.hl2 have lam' < (2 : ℝ)

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hl2 : lam' < (2 : ℝ).

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

      Lean, lines 92–95

          have hl2 : lam' < 2 := by
            rw [hlam', div_lt_iff₀ hqpos]
            have : (1 : ℝ) ≤ q := by exact_mod_cast hq1
            linarith

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 92–95 at 3e4a866f1f30 ↗

      1. s7.hl2.this have (1 : ℝ) ≤ (↑q : ℝ)

         Leaves lam < (2 : ℝ) * (↑q : ℝ), with this : (1 : ℝ) ≤ (↑q : ℝ).

         Lean, line 94

               have : (1 : ℝ) ≤ q := by exact_mod_cast hq1

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 94 at 3e4a866f1f30 ↗

   8. s7.hX0 have (0 : ℝ) ≤ X

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hX0 : (0 : ℝ) ≤ X.

      Lean, lines 96–100

          have hX0 : 0 ≤ X := by
            rw [hXdef]
            have := hDr.le; have := hDr1.le; have := hδ.le
            have hl0 : 0 ≤ lam := by linarith
            positivity

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 96–100 at 3e4a866f1f30 ↗

      1. s7.hX0.s1 have (0 : ℝ) ≤ D_r

         Leaves (0 : ℝ) ≤ (D_r * lam ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * lam ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * lam * W ^ (2 : ℕ) / D_r) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹, with this : (0 : ℝ) ≤ D_r.

         Lean, line 98

               have := hDr.le; have := hDr1.le; have := hδ.le

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 98 at 3e4a866f1f30 ↗

      2. s7.hX0.s2 have (0 : ℝ) ≤ D_r1

         Leaves (0 : ℝ) ≤ (D_r * lam ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * lam ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * lam * W ^ (2 : ℕ) / D_r) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹, with this : (0 : ℝ) ≤ D_r1.

         Lean, line 98

               have := hDr.le; have := hDr1.le; have := hδ.le

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 98 at 3e4a866f1f30 ↗

      3. s7.hX0.s3 have (0 : ℝ) ≤ δ

         Leaves (0 : ℝ) ≤ (D_r * lam ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * lam ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * lam * W ^ (2 : ℕ) / D_r) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹, with this : (0 : ℝ) ≤ δ.

         Lean, line 98

               have := hDr.le; have := hDr1.le; have := hδ.le

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 98 at 3e4a866f1f30 ↗

      4. s7.hX0.hl0 have (0 : ℝ) ≤ lam routine: linarith

         Leaves (0 : ℝ) ≤ (D_r * lam ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * lam ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * lam * W ^ (2 : ℕ) / D_r) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹, with hl0 : (0 : ℝ) ≤ lam.

         Lean, line 99

               have hl0 : 0 ≤ lam := by linarith

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 99 at 3e4a866f1f30 ↗

   9. s7.hXinv have (D_r * (↑q : ℝ) ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹ = X

      Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hXinv : (D_r * (↑q : ℝ) ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹ = X.

      Uses library mul_assoc.

      Lean, lines 101–110

          have hXinv : (D_r * q ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
              (δ * W ^ (2 : ℕ) / (D_r * q ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ +
              (D_r1 * q ^ (r + 1) * lam' * W ^ (2 : ℕ) / (D_r * q ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹
              = X := by
            have e1 : (q : ℝ) ^ r * lam' ^ r = lam ^ r := by
              rw [← mul_pow, hlam', mul_div_cancel₀ _ hqpos.ne']
            have e2 : D_r1 * q ^ (r + 1) * lam' * W ^ (2 : ℕ) / (D_r * q ^ r)
                = D_r1 * lam * W ^ (2 : ℕ) / D_r := by
              rw [hlam']; field_simp; ring
            rw [hXdef, e2, mul_assoc D_r, e1]

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 101–110 at 3e4a866f1f30 ↗

      1. s7.hXinv.e1 have (↑q : ℝ) ^ r * lam' ^ r = lam ^ r

         Leaves (D_r * (↑q : ℝ) ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹ = X, with e1 : (↑q : ℝ) ^ r * lam' ^ r = lam ^ r.

         Uses library mul_pow, mul_div_cancel₀.

         Lean, lines 105–106

               have e1 : (q : ℝ) ^ r * lam' ^ r = lam ^ r := by
                 rw [← mul_pow, hlam', mul_div_cancel₀ _ hqpos.ne']

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 105–106 at 3e4a866f1f30 ↗

      2. s7.hXinv.e2 have D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r) = D_r1 * lam * W ^ (2 : ℕ) / D_r

         Leaves (D_r * (↑q : ℝ) ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹ = X, with e2 : D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r) = D_r1 * lam * W ^ (2 : ℕ) / D_r.

         Lean, lines 107–109

               have e2 : D_r1 * q ^ (r + 1) * lam' * W ^ (2 : ℕ) / (D_r * q ^ r)
                   = D_r1 * lam * W ^ (2 : ℕ) / D_r := by
                 rw [hlam']; field_simp; ring

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 107–109 at 3e4a866f1f30 ↗

   10. s7.hclass have ∀ c ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = c}.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam'

       Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hclass : ∀ c ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = c}.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam'.

       Uses library Finset.range range n is the set of natural numbers less than n. .

       Lean, lines 111–244

           have hclass : ∀ c ∈ Finset.range q,
               ((S.filter (fun u => (u % (q : ℤ)).toNat = c)).card : ℝ)
                 < 65536 * (N / q) * X + 2 * (r : ℝ) * lam' := by
             intro c hc
             have hcq : c < q := Finset.mem_range.mp hc
             set T := S.filter (fun u => (u % (q : ℤ)).toNat = c) with hT
             have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1
             have hmem : ∀ u ∈ T, u ∈ S ∧ u % (q : ℤ) = c := by
               intro u hu
               rw [hT, Finset.mem_filter] at hu
               refine ⟨hu.1, ?_⟩
               have h0 : 0 ≤ u % (q : ℤ) := Int.emod_nonneg _ hqZ.ne'
               omega
             have hdecomp : ∀ u ∈ T, u = c + q * (u / q) := by
               intro u hu
               have := Int.emod_add_mul_ediv u q
               rw [(hmem u hu).2] at this
               omega
             set T' := T.image (fun u => u / (q : ℤ)) with hT'
             have hcardT : T'.card = T.card := by
               apply Finset.card_image_of_injOn
               intro u hu u' hu' huu
               simp only at huu
               rw [hdecomp u hu, hdecomp u' hu', huu]
             have hlam'pos : (4 : ℝ) ≤ 2 * (r : ℝ) * lam' := by
               have : (2 : ℝ) ≤ r := by exact_mod_cast hr
               nlinarith
             have hNq : 0 ≤ 65536 * (N / q) * X := by positivity
             by_cases hNc : (c : ℝ) < N
             · set N' : ℝ := (N - c) / q with hN'
               have hN'pos : 0 < N' := div_pos (by linarith) hqpos
               set g : ℝ → ℝ := fun t => f (c + q * t) with hg
               have hgfun : ∀ k : ℕ, k ≤ r + 1 → ∀ t, iteratedDeriv k g t
                   = (q : ℝ) ^ k * iteratedDeriv k f (c + q * t) := by
                 intro k hk t
                 have hf1 : ContDiff ℝ k (fun z => f (c + z)) := by
                   have : ContDiff ℝ k f := hf.of_le (by exact_mod_cast hk)
                   exact this.comp (contDiff_const.add contDiff_id)
                 have := iteratedDeriv_comp_const_mul hf1 (q : ℝ)
                 have h2 := congrFun this t
                 try simp only at h2
                 rw [show g = fun x => (fun z => f (c + z)) (q * x) from rfl, h2,
                   iteratedDeriv_comp_const_add]
               have hgC : ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g :=
                 hf.comp (contDiff_const.add (contDiff_const.mul contDiff_id))
               have hIcc : ∀ x ∈ Set.Icc (0 : ℝ) N', (c : ℝ) + q * x ∈ Set.Icc (0 : ℝ) N := by
                 intro x hx
                 obtain ⟨hx0, hx1⟩ := hx
                 constructor
                 · positivity
                 · have : (q : ℝ) * x ≤ q * N' := mul_le_mul_of_nonneg_left hx1 hqpos.le
                   rw [hN', mul_div_cancel₀ _ hqpos.ne'] at this
                   linarith
               have hqr : (0 : ℝ) < (q : ℝ) ^ r := pow_pos hqpos r
               have key := core N' hN'pos lam' hl1 hl2 (D_r * q ^ r) (by positivity)
                 (D_r1 * q ^ (r + 1)) (by positivity) g hgC
                 (by
                   intro x hx
                   rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
                   have := h1 _ (hIcc x hx)
                   nlinarith)
                 (by
                   intro x hx
                   rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
                   have := h2 _ (hIcc x hx)
                   nlinarith)
                 (by
                   intro x hx
                   rw [hgfun (r + 1) le_rfl, abs_mul, abs_of_pos (pow_pos hqpos _)]
                   have := h3 _ (hIcc x hx)
                   have : (0 : ℝ) < (q : ℝ) ^ (r + 1) := pow_pos hqpos _
                   nlinarith)
                 T'
                 (by
                   intro t ht
                   rw [hT', Finset.mem_image] at ht
                   obtain ⟨u, hu, rfl⟩ := ht
                   have huS := (hmem u hu).1
                   obtain ⟨hu0, hu1⟩ := hS u huS
                   refine ⟨Int.ediv_nonneg hu0 hqZ.le, ?_⟩
                   apply Int.le_floor.mpr
                   rw [hN', le_div_iff₀ hqpos]
                   have hdu := hdecomp u hu
                   have hreal : (u : ℝ) = c + q * ((u / q : ℤ) : ℝ) := by
                     have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                     push_cast at this
                     exact this
                   have : (u : ℝ) ≤ N := le_trans (by exact_mod_cast hu1) (Int.floor_le N)
                   linarith)
                 (by
                   intro t ht
                   rw [hT', Finset.mem_image] at ht
                   obtain ⟨u, hu, rfl⟩ := ht
                   obtain ⟨v, w, hw0, hwW, hvw⟩ := hS2 u (hmem u hu).1
                   refine ⟨v, w, hw0, hwW, ?_⟩
                   have hdu := hdecomp u hu
                   have hreal : (c : ℝ) + q * ((u / q : ℤ) : ℝ) = u := by
                     have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                     push_cast at this
                     exact this.symm
                   simp only [hg, hreal]
                   exact hvw)
                 (by rw [hXinv]; exact hX)
               rw [hXinv, hcardT] at key
               have : 65536 * N' * X ≤ 65536 * (N / q) * X := by
                 apply mul_le_mul_of_nonneg_right _ hX0
                 apply mul_le_mul_of_nonneg_left _ (by norm_num)
                 rw [hN']
                 apply div_le_div_of_nonneg_right _ hqpos.le
                 have : (0 : ℝ) ≤ c := by positivity
                 linarith
               linarith
             · push_neg at hNc
               -- the class contains at most the single point `c`
               have hle : T.card ≤ 1 := by
                 rw [Finset.card_le_one]
                 intro u hu u' hu'
                 have key : ∀ x ∈ T, x = c := by
                   intro x hx
                   have hxS := (hmem x hx).1
                   obtain ⟨hx0, hx1⟩ := hS x hxS
                   have hdx := hdecomp x hx
                   have hxN : (x : ℝ) ≤ N := le_trans (by exact_mod_cast hx1) (Int.floor_le N)
                   have hxc : x ≤ c := by
                     have : (x : ℝ) ≤ c := le_trans hxN hNc
                     exact_mod_cast this
                   have hcq' : (c : ℤ) < q := by exact_mod_cast hcq
                   have hdvd : (q : ℤ) ∣ x - c := ⟨x / q, by omega⟩
                   have habs : |x - (c : ℤ)| < q := by rw [abs_lt]; constructor <;> omega
                   have := Int.eq_zero_of_abs_lt_dvd hdvd habs
                   omega
                 rw [key u hu, key u' hu']
               have : (T.card : ℝ) ≤ 1 := by exact_mod_cast hle
               linarith

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 111–244 at 3e4a866f1f30 ↗

       1. s7.hclass.hcq have c < q

          Leaves (↑{u ∈ S | (u % (↑q : ℤ)).toNat = c}.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hcq : c < q.

          Uses library Finset.mem_range.

          Lean, line 115

                have hcq : c < q := Finset.mem_range.mp hc

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 115 at 3e4a866f1f30 ↗

       2. s7.hclass.hqZ have (0 : ℤ) < (↑q : ℤ)

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hqZ : (0 : ℤ) < (↑q : ℤ).

          Lean, line 117

                have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 117 at 3e4a866f1f30 ↗

       3. s7.hclass.hmem have ∀ u ∈ T, u ∈ S ∧ u % (↑q : ℤ) = (↑c : ℤ)

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hmem : ∀ u ∈ T, u ∈ S ∧ u % (↑q : ℤ) = (↑c : ℤ).

          Uses library Finset.mem_filter, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

          Lean, lines 118–123

                have hmem : ∀ u ∈ T, u ∈ S ∧ u % (q : ℤ) = c := by
                  intro u hu
                  rw [hT, Finset.mem_filter] at hu
                  refine ⟨hu.1, ?_⟩
                  have h0 : 0 ≤ u % (q : ℤ) := Int.emod_nonneg _ hqZ.ne'
                  omega

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 118–123 at 3e4a866f1f30 ↗

          1. s7.hclass.hmem.h0 have (0 : ℤ) ≤ u % (↑q : ℤ)

             Leaves u % (↑q : ℤ) = (↑c : ℤ), with h0 : (0 : ℤ) ≤ u % (↑q : ℤ).

             Uses library Int.emod_nonneg.

             Lean, line 122

                     have h0 : 0 ≤ u % (q : ℤ) := Int.emod_nonneg _ hqZ.ne'

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 122 at 3e4a866f1f30 ↗

       4. s7.hclass.hdecomp have ∀ u ∈ T, u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hdecomp : ∀ u ∈ T, u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ)).

          Lean, lines 124–128

                have hdecomp : ∀ u ∈ T, u = c + q * (u / q) := by
                  intro u hu
                  have := Int.emod_add_mul_ediv u q
                  rw [(hmem u hu).2] at this
                  omega

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 124–128 at 3e4a866f1f30 ↗

          1. s7.hclass.hdecomp.this have u % (↑q : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ)) = u

             Leaves u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ)), with this : u % (↑q : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ)) = u.

             Uses library Int.emod_add_mul_ediv.

             Lean, line 126

                     have := Int.emod_add_mul_ediv u q

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 126 at 3e4a866f1f30 ↗

       5. s7.hclass.hcardT have T'.card = T.card

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hcardT : T'.card = T.card.

          Uses library Finset.card_image_of_injOn.

          Lean, lines 130–134

                have hcardT : T'.card = T.card := by
                  apply Finset.card_image_of_injOn
                  intro u hu u' hu' huu
                  simp only at huu
                  rw [hdecomp u hu, hdecomp u' hu', huu]

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 130–134 at 3e4a866f1f30 ↗

       6. s7.hclass.hlam'pos have (4 : ℝ) ≤ (2 : ℝ) * (↑r : ℝ) * lam'

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hlam'pos : (4 : ℝ) ≤ (2 : ℝ) * (↑r : ℝ) * lam'.

          Lean, lines 135–137

                have hlam'pos : (4 : ℝ) ≤ 2 * (r : ℝ) * lam' := by
                  have : (2 : ℝ) ≤ r := by exact_mod_cast hr
                  nlinarith

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 135–137 at 3e4a866f1f30 ↗

          1. s7.hclass.hlam'pos.this have (2 : ℝ) ≤ (↑r : ℝ)

             Leaves (4 : ℝ) ≤ (2 : ℝ) * (↑r : ℝ) * lam', with this : (2 : ℝ) ≤ (↑r : ℝ).

             Lean, line 136

                     have : (2 : ℝ) ≤ r := by exact_mod_cast hr

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 136 at 3e4a866f1f30 ↗

       7. s7.hclass.hNq have (0 : ℝ) ≤ (65536 : ℝ) * (N / (↑q : ℝ)) * X routine: positivity

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hNq : (0 : ℝ) ≤ (65536 : ℝ) * (N / (↑q : ℝ)) * X.

          Lean, line 138

                have hNq : 0 ≤ 65536 * (N / q) * X := by positivity

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 138 at 3e4a866f1f30 ↗

       8. s7.hclass.s8 case

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hNc : (↑c : ℝ) < N.

          Lean, lines 140–222

                · set N' : ℝ := (N - c) / q with hN'
                  have hN'pos : 0 < N' := div_pos (by linarith) hqpos
                  set g : ℝ → ℝ := fun t => f (c + q * t) with hg
                  have hgfun : ∀ k : ℕ, k ≤ r + 1 → ∀ t, iteratedDeriv k g t
                      = (q : ℝ) ^ k * iteratedDeriv k f (c + q * t) := by
                    intro k hk t
                    have hf1 : ContDiff ℝ k (fun z => f (c + z)) := by
                      have : ContDiff ℝ k f := hf.of_le (by exact_mod_cast hk)
                      exact this.comp (contDiff_const.add contDiff_id)
                    have := iteratedDeriv_comp_const_mul hf1 (q : ℝ)
                    have h2 := congrFun this t
                    try simp only at h2
                    rw [show g = fun x => (fun z => f (c + z)) (q * x) from rfl, h2,
                      iteratedDeriv_comp_const_add]
                  have hgC : ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g :=
                    hf.comp (contDiff_const.add (contDiff_const.mul contDiff_id))
                  have hIcc : ∀ x ∈ Set.Icc (0 : ℝ) N', (c : ℝ) + q * x ∈ Set.Icc (0 : ℝ) N := by
                    intro x hx
                    obtain ⟨hx0, hx1⟩ := hx
                    constructor
                    · positivity
                    · have : (q : ℝ) * x ≤ q * N' := mul_le_mul_of_nonneg_left hx1 hqpos.le
                      rw [hN', mul_div_cancel₀ _ hqpos.ne'] at this
                      linarith
                  have hqr : (0 : ℝ) < (q : ℝ) ^ r := pow_pos hqpos r
                  have key := core N' hN'pos lam' hl1 hl2 (D_r * q ^ r) (by positivity)
                    (D_r1 * q ^ (r + 1)) (by positivity) g hgC
                    (by
                      intro x hx
                      rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
                      have := h1 _ (hIcc x hx)
                      nlinarith)
                    (by
                      intro x hx
                      rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
                      have := h2 _ (hIcc x hx)
                      nlinarith)
                    (by
                      intro x hx
                      rw [hgfun (r + 1) le_rfl, abs_mul, abs_of_pos (pow_pos hqpos _)]
                      have := h3 _ (hIcc x hx)
                      have : (0 : ℝ) < (q : ℝ) ^ (r + 1) := pow_pos hqpos _
                      nlinarith)
                    T'
                    (by
                      intro t ht
                      rw [hT', Finset.mem_image] at ht
                      obtain ⟨u, hu, rfl⟩ := ht
                      have huS := (hmem u hu).1
                      obtain ⟨hu0, hu1⟩ := hS u huS
                      refine ⟨Int.ediv_nonneg hu0 hqZ.le, ?_⟩
                      apply Int.le_floor.mpr
                      rw [hN', le_div_iff₀ hqpos]
                      have hdu := hdecomp u hu
                      have hreal : (u : ℝ) = c + q * ((u / q : ℤ) : ℝ) := by
                        have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                        push_cast at this
                        exact this
                      have : (u : ℝ) ≤ N := le_trans (by exact_mod_cast hu1) (Int.floor_le N)
                      linarith)
                    (by
                      intro t ht
                      rw [hT', Finset.mem_image] at ht
                      obtain ⟨u, hu, rfl⟩ := ht
                      obtain ⟨v, w, hw0, hwW, hvw⟩ := hS2 u (hmem u hu).1
                      refine ⟨v, w, hw0, hwW, ?_⟩
                      have hdu := hdecomp u hu
                      have hreal : (c : ℝ) + q * ((u / q : ℤ) : ℝ) = u := by
                        have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                        push_cast at this
                        exact this.symm
                      simp only [hg, hreal]
                      exact hvw)
                    (by rw [hXinv]; exact hX)
                  rw [hXinv, hcardT] at key
                  have : 65536 * N' * X ≤ 65536 * (N / q) * X := by
                    apply mul_le_mul_of_nonneg_right _ hX0
                    apply mul_le_mul_of_nonneg_left _ (by norm_num)
                    rw [hN']
                    apply div_le_div_of_nonneg_right _ hqpos.le
                    have : (0 : ℝ) ≤ c := by positivity
                    linarith
                  linarith

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 140–222 at 3e4a866f1f30 ↗

          1. s7.hclass.s8.hN'pos have (0 : ℝ) < N'

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hN'pos : (0 : ℝ) < N'.

             Uses library div_pos.

             Lean, line 141

                     have hN'pos : 0 < N' := div_pos (by linarith) hqpos

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 141 at 3e4a866f1f30 ↗

          2. s7.hclass.s8.hgfun have ∀ k ≤ r + (1 : ℕ), ∀ (t : ℝ), iteratedDeriv k g t = (↑q : ℝ) ^ k * iteratedDeriv k f ((↑c : ℝ) + (↑q : ℝ) * t)

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hgfun : ∀ k ≤ r + (1 : ℕ), ∀ (t : ℝ), iteratedDeriv k g t = (↑q : ℝ) ^ k * iteratedDeriv k f ((↑c : ℝ) + (↑q : ℝ) * t).

             Uses library iteratedDeriv The n-th iterated derivative of a function from 𝕜 to F, as a function from 𝕜 to F. , rfl rfl : a = a is the unique constructor of the equality type. , iteratedDeriv_comp_const_add The iterated derivative commutes with shifting the function by a constant on the left. .

             Lean, lines 143–153

                     have hgfun : ∀ k : ℕ, k ≤ r + 1 → ∀ t, iteratedDeriv k g t
                         = (q : ℝ) ^ k * iteratedDeriv k f (c + q * t) := by
                       intro k hk t
                       have hf1 : ContDiff ℝ k (fun z => f (c + z)) := by
                         have : ContDiff ℝ k f := hf.of_le (by exact_mod_cast hk)
                         exact this.comp (contDiff_const.add contDiff_id)
                       have := iteratedDeriv_comp_const_mul hf1 (q : ℝ)
                       have h2 := congrFun this t
                       try simp only at h2
                       rw [show g = fun x => (fun z => f (c + z)) (q * x) from rfl, h2,
                         iteratedDeriv_comp_const_add]

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 143–153 at 3e4a866f1f30 ↗

             1. s7.hclass.s8.hgfun.hf1 have ContDiff ℝ (↑k : WithTop ℕ∞) fun (z : ℝ) => f ((↑c : ℝ) + z)

                Leaves iteratedDeriv k g t = (↑q : ℝ) ^ k * iteratedDeriv k f ((↑c : ℝ) + (↑q : ℝ) * t), with hf1 : ContDiff ℝ (↑k : WithTop ℕ∞) fun (z : ℝ) => f ((↑c : ℝ) + z).

                Uses library ContDiff A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. , contDiff_const Constants are C^∞. , contDiff_id The identity is C^n. .

                Lean, lines 146–148

                          have hf1 : ContDiff ℝ k (fun z => f (c + z)) := by
                            have : ContDiff ℝ k f := hf.of_le (by exact_mod_cast hk)
                            exact this.comp (contDiff_const.add contDiff_id)

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 146–148 at 3e4a866f1f30 ↗

                1. s7.hclass.s8.hgfun.hf1.this have ContDiff ℝ (↑k : WithTop ℕ∞) f

                   Leaves ContDiff ℝ (↑k : WithTop ℕ∞) fun (z : ℝ) => f ((↑c : ℝ) + z), with this : ContDiff ℝ (↑k : WithTop ℕ∞) f.

                   Uses library ContDiff A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. .

                   Lean, line 147

                               have : ContDiff ℝ k f := hf.of_le (by exact_mod_cast hk)

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 147 at 3e4a866f1f30 ↗

             2. s7.hclass.s8.hgfun.this have (iteratedDeriv k fun (x : ℝ) => f ((↑c : ℝ) + (↑q : ℝ) * x)) = fun (x : ℝ) => (↑q : ℝ) ^ k * iteratedDeriv k (fun (z : ℝ) => f ((↑c : ℝ) + z)) ((↑q : ℝ) * x)

                Leaves iteratedDeriv k g t = (↑q : ℝ) ^ k * iteratedDeriv k f ((↑c : ℝ) + (↑q : ℝ) * t), with this : (iteratedDeriv k fun (x : ℝ) => f ((↑c : ℝ) + (↑q : ℝ) * x)) = fun (x : ℝ) => (↑q : ℝ) ^ k * iteratedDeriv k (fun (z : ℝ) => f ((↑c : ℝ) + z)) ((↑q : ℝ) * x).

                Uses library iteratedDeriv_comp_const_mul.

                Lean, line 149

                          have := iteratedDeriv_comp_const_mul hf1 (q : ℝ)

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 149 at 3e4a866f1f30 ↗

             3. s7.hclass.s8.hgfun.h2 have iteratedDeriv k (fun (x : ℝ) => f ((↑c : ℝ) + (↑q : ℝ) * x)) t = (↑q : ℝ) ^ k * iteratedDeriv k (fun (z : ℝ) => f ((↑c : ℝ) + z)) ((↑q : ℝ) * t)

                Leaves iteratedDeriv k g t = (↑q : ℝ) ^ k * iteratedDeriv k f ((↑c : ℝ) + (↑q : ℝ) * t), with h2 : iteratedDeriv k (fun (x : ℝ) => f ((↑c : ℝ) + (↑q : ℝ) * x)) t = (↑q : ℝ) ^ k * iteratedDeriv k (fun (z : ℝ) => f ((↑c : ℝ) + z)) ((↑q : ℝ) * t).

                Uses library congrFun Congruence in the function part of an application: If f = g then f a = g a. .

                Lean, line 150

                          have h2 := congrFun this t

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 150 at 3e4a866f1f30 ↗

          3. s7.hclass.s8.hgC have ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hgC : ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g.

             Uses library ContDiff A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. , WithTop Attach ⊤ to a type. , contDiff_const Constants are C^∞. , contDiff_id The identity is C^n. .

             Lean, lines 154–155

                     have hgC : ContDiff ℝ (↑(↑(r + (1 : ℕ)) : ℕ∞) : WithTop ℕ∞) g :=
                       hf.comp (contDiff_const.add (contDiff_const.mul contDiff_id))

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 154–155 at 3e4a866f1f30 ↗

          4. s7.hclass.s8.hIcc have ∀ x ∈ Set.Icc (0 : ℝ) N', (↑c : ℝ) + (↑q : ℝ) * x ∈ Set.Icc (0 : ℝ) N

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hIcc : ∀ x ∈ Set.Icc (0 : ℝ) N', (↑c : ℝ) + (↑q : ℝ) * x ∈ Set.Icc (0 : ℝ) N.

             Uses library Set.Icc Icc a b is the left-closed right-closed interval $[a, b]$. .

             Lean, lines 156–163

                     have hIcc : ∀ x ∈ Set.Icc (0 : ℝ) N', (c : ℝ) + q * x ∈ Set.Icc (0 : ℝ) N := by
                       intro x hx
                       obtain ⟨hx0, hx1⟩ := hx
                       constructor
                       · positivity
                       · have : (q : ℝ) * x ≤ q * N' := mul_le_mul_of_nonneg_left hx1 hqpos.le
                         rw [hN', mul_div_cancel₀ _ hqpos.ne'] at this
                         linarith

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 156–163 at 3e4a866f1f30 ↗

             1. s7.hclass.s8.hIcc.s1 obtain x ∈ Set.Icc (0 : ℝ) N'

                Leaves (↑c : ℝ) + (↑q : ℝ) * x ∈ Set.Icc (0 : ℝ) N, with hx0 : (0 : ℝ) ≤ x, hx1 : x ≤ N'.

                Lean, line 158

                          obtain ⟨hx0, hx1⟩ := hx

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 158 at 3e4a866f1f30 ↗

             2. s7.hclass.s8.hIcc.s2 case routine: positivity

                Leaves (0 : ℝ) ≤ (↑c : ℝ) + (↑q : ℝ) * x.

                Lean, line 160

                          · positivity

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 160 at 3e4a866f1f30 ↗

             3. s7.hclass.s8.hIcc.s3 case

                Leaves (↑c : ℝ) + (↑q : ℝ) * x ≤ N.

                Uses library mul_div_cancel₀.

                Lean, lines 161–163

                          · have : (q : ℝ) * x ≤ q * N' := mul_le_mul_of_nonneg_left hx1 hqpos.le
                            rw [hN', mul_div_cancel₀ _ hqpos.ne'] at this
                            linarith

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 161–163 at 3e4a866f1f30 ↗

                1. s7.hclass.s8.hIcc.s3.this have (↑q : ℝ) * x ≤ (↑q : ℝ) * N'

                   Leaves (↑c : ℝ) + (↑q : ℝ) * x ≤ N, with this : (↑q : ℝ) * x ≤ (↑q : ℝ) * N'.

                   Uses library mul_le_mul_of_nonneg_left.

                   Lean, line 161

                             · have : (q : ℝ) * x ≤ q * N' := mul_le_mul_of_nonneg_left hx1 hqpos.le

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 161 at 3e4a866f1f30 ↗

          5. s7.hclass.s8.hqr have (0 : ℝ) < (↑q : ℝ) ^ r

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hqr : (0 : ℝ) < (↑q : ℝ) ^ r.

             Uses library pow_pos.

             Lean, line 164

                     have hqr : (0 : ℝ) < (q : ℝ) ^ r := pow_pos hqpos r

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 164 at 3e4a866f1f30 ↗

          6. s7.hclass.s8.key have (↑T'.card : ℝ) < (65536 : ℝ) * N' * ((D_r * (↑q : ℝ) ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) + (2 : ℝ) * (↑r : ℝ) * lam'

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with key : (↑T'.card : ℝ) < (65536 : ℝ) * N' * ((D_r * (↑q : ℝ) ^ r * lam' ^ r * W ^ (2 : ℕ)) ^ ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ + (δ * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r * lam' ^ r)) ^ ((↑r : ℝ) - (1 : ℝ))⁻¹ + (D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)) * lam' * W ^ (2 : ℕ) / (D_r * (↑q : ℝ) ^ r)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) + (2 : ℝ) * (↑r : ℝ) * lam'.

             Uses library abs_mul, abs_of_pos, le_rfl A version of le_refl where the argument is implicit , pow_pos, Finset.mem_image, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , Int.ediv_nonneg, Int.le_floor, le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. , Exists.intro Existential introduction. .

             Lean, lines 165–213

                     have key := core N' hN'pos lam' hl1 hl2 (D_r * q ^ r) (by positivity)
                       (D_r1 * q ^ (r + 1)) (by positivity) g hgC
                       (by
                         intro x hx
                         rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
                         have := h1 _ (hIcc x hx)
                         nlinarith)
                       (by
                         intro x hx
                         rw [hgfun r (by omega), abs_mul, abs_of_pos hqr]
                         have := h2 _ (hIcc x hx)
                         nlinarith)
                       (by
                         intro x hx
                         rw [hgfun (r + 1) le_rfl, abs_mul, abs_of_pos (pow_pos hqpos _)]
                         have := h3 _ (hIcc x hx)
                         have : (0 : ℝ) < (q : ℝ) ^ (r + 1) := pow_pos hqpos _
                         nlinarith)
                       T'
                       (by
                         intro t ht
                         rw [hT', Finset.mem_image] at ht
                         obtain ⟨u, hu, rfl⟩ := ht
                         have huS := (hmem u hu).1
                         obtain ⟨hu0, hu1⟩ := hS u huS
                         refine ⟨Int.ediv_nonneg hu0 hqZ.le, ?_⟩
                         apply Int.le_floor.mpr
                         rw [hN', le_div_iff₀ hqpos]
                         have hdu := hdecomp u hu
                         have hreal : (u : ℝ) = c + q * ((u / q : ℤ) : ℝ) := by
                           have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                           push_cast at this
                           exact this
                         have : (u : ℝ) ≤ N := le_trans (by exact_mod_cast hu1) (Int.floor_le N)
                         linarith)
                       (by
                         intro t ht
                         rw [hT', Finset.mem_image] at ht
                         obtain ⟨u, hu, rfl⟩ := ht
                         obtain ⟨v, w, hw0, hwW, hvw⟩ := hS2 u (hmem u hu).1
                         refine ⟨v, w, hw0, hwW, ?_⟩
                         have hdu := hdecomp u hu
                         have hreal : (c : ℝ) + q * ((u / q : ℤ) : ℝ) = u := by
                           have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                           push_cast at this
                           exact this.symm
                         simp only [hg, hreal]
                         exact hvw)
                       (by rw [hXinv]; exact hX)

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 165–213 at 3e4a866f1f30 ↗

             1. s7.hclass.s8.key.s1 have D_r / (2 : ℝ) ≤ |iteratedDeriv r f ((↑c : ℝ) + (↑q : ℝ) * x)|

                Leaves D_r * (↑q : ℝ) ^ r / (2 : ℝ) ≤ (↑q : ℝ) ^ r * |iteratedDeriv r f ((↑c : ℝ) + (↑q : ℝ) * x)|, with this : D_r / (2 : ℝ) ≤ |iteratedDeriv r f ((↑c : ℝ) + (↑q : ℝ) * x)|.

                Lean, line 170

                            have := h1 _ (hIcc x hx)

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 170 at 3e4a866f1f30 ↗

             2. s7.hclass.s8.key.s2 have |iteratedDeriv r f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r

                Leaves (↑q : ℝ) ^ r * |iteratedDeriv r f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r * (↑q : ℝ) ^ r, with this : |iteratedDeriv r f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r.

                Lean, line 175

                            have := h2 _ (hIcc x hx)

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 175 at 3e4a866f1f30 ↗

             3. s7.hclass.s8.key.s3 have |iteratedDeriv (r + (1 : ℕ)) f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r1

                Leaves (↑q : ℝ) ^ (r + (1 : ℕ)) * |iteratedDeriv (r + (1 : ℕ)) f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)), with this : |iteratedDeriv (r + (1 : ℕ)) f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r1.

                Lean, line 180

                            have := h3 _ (hIcc x hx)

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 180 at 3e4a866f1f30 ↗

             4. s7.hclass.s8.key.s4 have (0 : ℝ) < (↑q : ℝ) ^ (r + (1 : ℕ))

                Leaves (↑q : ℝ) ^ (r + (1 : ℕ)) * |iteratedDeriv (r + (1 : ℕ)) f ((↑c : ℝ) + (↑q : ℝ) * x)| ≤ D_r1 * (↑q : ℝ) ^ (r + (1 : ℕ)), with this : (0 : ℝ) < (↑q : ℝ) ^ (r + (1 : ℕ)).

                Uses library pow_pos.

                Lean, line 181

                            have : (0 : ℝ) < (q : ℝ) ^ (r + 1) := pow_pos hqpos _

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 181 at 3e4a866f1f30 ↗

             5. s7.hclass.s8.key.s5 obtain ∃ a ∈ T, a / (↑q : ℤ) = t

                Leaves (0 : ℤ) ≤ u / (↑q : ℤ) ∧ u / (↑q : ℤ) ≤ ⌊N'⌋, with u : ℤ, hu : u ∈ T.

                Lean, line 187

                            obtain ⟨u, hu, rfl⟩ := ht

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 187 at 3e4a866f1f30 ↗

             6. s7.hclass.s8.key.huS have u ∈ S

                Leaves (0 : ℤ) ≤ u / (↑q : ℤ) ∧ u / (↑q : ℤ) ≤ ⌊N'⌋, with huS : u ∈ S.

                Lean, line 188

                            have huS := (hmem u hu).1

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 188 at 3e4a866f1f30 ↗

             7. s7.hclass.s8.key.s7 obtain (0 : ℤ) ≤ u ∧ u ≤ ⌊N⌋

                Leaves (0 : ℤ) ≤ u / (↑q : ℤ) ∧ u / (↑q : ℤ) ≤ ⌊N'⌋, with hu0 : (0 : ℤ) ≤ u, hu1 : u ≤ ⌊N⌋.

                Lean, line 189

                            obtain ⟨hu0, hu1⟩ := hS u huS

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 189 at 3e4a866f1f30 ↗

             8. s7.hclass.s8.key.s8 have u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))

                Leaves (↑(u / (↑q : ℤ)) : ℝ) * (↑q : ℝ) ≤ N - (↑c : ℝ), with hdu : u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ)).

                Lean, line 193

                            have hdu := hdecomp u hu

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 193 at 3e4a866f1f30 ↗

             9. s7.hclass.s8.key.s9 have (↑u : ℝ) = (↑c : ℝ) + (↑q : ℝ) * (↑(u / (↑q : ℤ)) : ℝ)

                Leaves (↑(u / (↑q : ℤ)) : ℝ) * (↑q : ℝ) ≤ N - (↑c : ℝ), with hreal : (↑u : ℝ) = (↑c : ℝ) + (↑q : ℝ) * (↑(u / (↑q : ℤ)) : ℝ).

                Lean, lines 194–197

                            have hreal : (u : ℝ) = c + q * ((u / q : ℤ) : ℝ) := by
                              have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                              push_cast at this
                              exact this

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 194–197 at 3e4a866f1f30 ↗

                1. s7.hclass.s8.key.s9.this have (↑u : ℝ) = (↑((↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))) : ℝ)

                   Leaves (↑u : ℝ) = (↑c : ℝ) + (↑q : ℝ) * (↑(u / (↑q : ℤ)) : ℝ), with this : (↑u : ℝ) = (↑((↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))) : ℝ).

                   Uses library congrArg Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. .

                   Lean, line 195

                                 have := congrArg (fun z : ℤ => (z : ℝ)) hdu

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 195 at 3e4a866f1f30 ↗

             10. s7.hclass.s8.key.s10 have (↑u : ℝ) ≤ N

                 Leaves (↑(u / (↑q : ℤ)) : ℝ) * (↑q : ℝ) ≤ N - (↑c : ℝ), with this : (↑u : ℝ) ≤ N.

                 Uses library le_trans The relation ≤ on a preorder is transitive. , Int.floor_le.

                 Lean, line 198

                             have : (u : ℝ) ≤ N := le_trans (by exact_mod_cast hu1) (Int.floor_le N)

                 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 198 at 3e4a866f1f30 ↗

             11. s7.hclass.s8.key.s11 obtain ∃ a ∈ T, a / (↑q : ℤ) = t

                 Leaves ∃ (v : ℤ) (w : ℕ), (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |g (↑(u / (↑q : ℤ)) : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ, with u : ℤ, hu : u ∈ T.

                 Lean, line 203

                             obtain ⟨u, hu, rfl⟩ := ht

                 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 203 at 3e4a866f1f30 ↗

             12. s7.hclass.s8.key.s12 obtain ∃ (v : ℤ) (w : ℕ), (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |f (↑u : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ

                 Leaves ∃ (v : ℤ) (w : ℕ), (0 : ℕ) < w ∧ (↑w : ℝ) ≤ W ∧ |g (↑(u / (↑q : ℤ)) : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ, with v : ℤ, w : ℕ, hw0 : (0 : ℕ) < w, hwW : (↑w : ℝ) ≤ W, hvw : |f (↑u : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ.

                 Lean, line 204

                             obtain ⟨v, w, hw0, hwW, hvw⟩ := hS2 u (hmem u hu).1

                 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 204 at 3e4a866f1f30 ↗

             13. s7.hclass.s8.key.s13 have u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))

                 Leaves |g (↑(u / (↑q : ℤ)) : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ, with hdu : u = (↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ)).

                 Lean, line 206

                             have hdu := hdecomp u hu

                 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 206 at 3e4a866f1f30 ↗

             14. s7.hclass.s8.key.s14 have (↑c : ℝ) + (↑q : ℝ) * (↑(u / (↑q : ℤ)) : ℝ) = (↑u : ℝ)

                 Leaves |g (↑(u / (↑q : ℤ)) : ℝ) - (↑v : ℝ) / (↑w : ℝ)| < δ, with hreal : (↑c : ℝ) + (↑q : ℝ) * (↑(u / (↑q : ℤ)) : ℝ) = (↑u : ℝ).

                 Lean, lines 207–210

                             have hreal : (c : ℝ) + q * ((u / q : ℤ) : ℝ) = u := by
                               have := congrArg (fun z : ℤ => (z : ℝ)) hdu
                               push_cast at this
                               exact this.symm

                 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 207–210 at 3e4a866f1f30 ↗

                 1. s7.hclass.s8.key.s14.this have (↑u : ℝ) = (↑((↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))) : ℝ)

                    Leaves (↑c : ℝ) + (↑q : ℝ) * (↑(u / (↑q : ℤ)) : ℝ) = (↑u : ℝ), with this : (↑u : ℝ) = (↑((↑c : ℤ) + (↑q : ℤ) * (u / (↑q : ℤ))) : ℝ).

                    Uses library congrArg Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. .

                    Lean, line 208

                                  have := congrArg (fun z : ℤ => (z : ℝ)) hdu

                    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 208 at 3e4a866f1f30 ↗

          7. s7.hclass.s8.this have (65536 : ℝ) * N' * X ≤ (65536 : ℝ) * (N / (↑q : ℝ)) * X

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with this : (65536 : ℝ) * N' * X ≤ (65536 : ℝ) * (N / (↑q : ℝ)) * X.

             Uses library mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, div_le_div_of_nonneg_right.

             Lean, lines 215–221

                     have : 65536 * N' * X ≤ 65536 * (N / q) * X := by
                       apply mul_le_mul_of_nonneg_right _ hX0
                       apply mul_le_mul_of_nonneg_left _ (by norm_num)
                       rw [hN']
                       apply div_le_div_of_nonneg_right _ hqpos.le
                       have : (0 : ℝ) ≤ c := by positivity
                       linarith

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 215–221 at 3e4a866f1f30 ↗

             1. s7.hclass.s8.this.this have (0 : ℝ) ≤ (↑c : ℝ) routine: positivity

                Leaves N - (↑c : ℝ) ≤ N, with this : (0 : ℝ) ≤ (↑c : ℝ).

                Lean, line 220

                          have : (0 : ℝ) ≤ c := by positivity

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 220 at 3e4a866f1f30 ↗

       9. s7.hclass.s9 case

          Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hNc : ¬(↑c : ℝ) < N.

          Lean, lines 223–244

                · push_neg at hNc
                  -- the class contains at most the single point `c`
                  have hle : T.card ≤ 1 := by
                    rw [Finset.card_le_one]
                    intro u hu u' hu'
                    have key : ∀ x ∈ T, x = c := by
                      intro x hx
                      have hxS := (hmem x hx).1
                      obtain ⟨hx0, hx1⟩ := hS x hxS
                      have hdx := hdecomp x hx
                      have hxN : (x : ℝ) ≤ N := le_trans (by exact_mod_cast hx1) (Int.floor_le N)
                      have hxc : x ≤ c := by
                        have : (x : ℝ) ≤ c := le_trans hxN hNc
                        exact_mod_cast this
                      have hcq' : (c : ℤ) < q := by exact_mod_cast hcq
                      have hdvd : (q : ℤ) ∣ x - c := ⟨x / q, by omega⟩
                      have habs : |x - (c : ℤ)| < q := by rw [abs_lt]; constructor <;> omega
                      have := Int.eq_zero_of_abs_lt_dvd hdvd habs
                      omega
                    rw [key u hu, key u' hu']
                  have : (T.card : ℝ) ≤ 1 := by exact_mod_cast hle
                  linarith

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 223–244 at 3e4a866f1f30 ↗

          1. s7.hclass.s9.hle have T.card ≤ (1 : ℕ)

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with hle : T.card ≤ (1 : ℕ).

             Uses library Finset.card_le_one.

             Lean, lines 225–242

                     have hle : T.card ≤ 1 := by
                       rw [Finset.card_le_one]
                       intro u hu u' hu'
                       have key : ∀ x ∈ T, x = c := by
                         intro x hx
                         have hxS := (hmem x hx).1
                         obtain ⟨hx0, hx1⟩ := hS x hxS
                         have hdx := hdecomp x hx
                         have hxN : (x : ℝ) ≤ N := le_trans (by exact_mod_cast hx1) (Int.floor_le N)
                         have hxc : x ≤ c := by
                           have : (x : ℝ) ≤ c := le_trans hxN hNc
                           exact_mod_cast this
                         have hcq' : (c : ℤ) < q := by exact_mod_cast hcq
                         have hdvd : (q : ℤ) ∣ x - c := ⟨x / q, by omega⟩
                         have habs : |x - (c : ℤ)| < q := by rw [abs_lt]; constructor <;> omega
                         have := Int.eq_zero_of_abs_lt_dvd hdvd habs
                         omega
                       rw [key u hu, key u' hu']

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 225–242 at 3e4a866f1f30 ↗

             1. s7.hclass.s9.hle.key have ∀ x ∈ T, x = (↑c : ℤ)

                Leaves u = u', with key : ∀ x ∈ T, x = (↑c : ℤ).

                Lean, lines 228–241

                          have key : ∀ x ∈ T, x = c := by
                            intro x hx
                            have hxS := (hmem x hx).1
                            obtain ⟨hx0, hx1⟩ := hS x hxS
                            have hdx := hdecomp x hx
                            have hxN : (x : ℝ) ≤ N := le_trans (by exact_mod_cast hx1) (Int.floor_le N)
                            have hxc : x ≤ c := by
                              have : (x : ℝ) ≤ c := le_trans hxN hNc
                              exact_mod_cast this
                            have hcq' : (c : ℤ) < q := by exact_mod_cast hcq
                            have hdvd : (q : ℤ) ∣ x - c := ⟨x / q, by omega⟩
                            have habs : |x - (c : ℤ)| < q := by rw [abs_lt]; constructor <;> omega
                            have := Int.eq_zero_of_abs_lt_dvd hdvd habs
                            omega

                targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 228–241 at 3e4a866f1f30 ↗

                1. s7.hclass.s9.hle.key.hxS have x ∈ S

                   Leaves x = (↑c : ℤ), with hxS : x ∈ S.

                   Lean, line 230

                               have hxS := (hmem x hx).1

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 230 at 3e4a866f1f30 ↗

                2. s7.hclass.s9.hle.key.s2 obtain (0 : ℤ) ≤ x ∧ x ≤ ⌊N⌋

                   Leaves x = (↑c : ℤ), with hx0 : (0 : ℤ) ≤ x, hx1 : x ≤ ⌊N⌋.

                   Lean, line 231

                               obtain ⟨hx0, hx1⟩ := hS x hxS

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 231 at 3e4a866f1f30 ↗

                3. s7.hclass.s9.hle.key.hdx have x = (↑c : ℤ) + (↑q : ℤ) * (x / (↑q : ℤ))

                   Leaves x = (↑c : ℤ), with hdx : x = (↑c : ℤ) + (↑q : ℤ) * (x / (↑q : ℤ)).

                   Lean, line 232

                               have hdx := hdecomp x hx

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 232 at 3e4a866f1f30 ↗

                4. s7.hclass.s9.hle.key.hxN have (↑x : ℝ) ≤ N

                   Leaves x = (↑c : ℤ), with hxN : (↑x : ℝ) ≤ N.

                   Uses library le_trans The relation ≤ on a preorder is transitive. , Int.floor_le.

                   Lean, line 233

                               have hxN : (x : ℝ) ≤ N := le_trans (by exact_mod_cast hx1) (Int.floor_le N)

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 233 at 3e4a866f1f30 ↗

                5. s7.hclass.s9.hle.key.hxc have x ≤ (↑c : ℤ)

                   Leaves x = (↑c : ℤ), with hxc : x ≤ (↑c : ℤ).

                   Lean, lines 234–236

                               have hxc : x ≤ c := by
                                 have : (x : ℝ) ≤ c := le_trans hxN hNc
                                 exact_mod_cast this

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 234–236 at 3e4a866f1f30 ↗

                   1. s7.hclass.s9.hle.key.hxc.this have (↑x : ℝ) ≤ (↑c : ℝ)

                      Leaves x ≤ (↑c : ℤ), with this : (↑x : ℝ) ≤ (↑c : ℝ).

                      Uses library le_trans The relation ≤ on a preorder is transitive. .

                      Lean, line 235

                                    have : (x : ℝ) ≤ c := le_trans hxN hNc

                      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 235 at 3e4a866f1f30 ↗

                6. s7.hclass.s9.hle.key.hcq' have (↑c : ℤ) < (↑q : ℤ)

                   Leaves x = (↑c : ℤ), with hcq' : (↑c : ℤ) < (↑q : ℤ).

                   Lean, line 237

                               have hcq' : (c : ℤ) < q := by exact_mod_cast hcq

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 237 at 3e4a866f1f30 ↗

                7. s7.hclass.s9.hle.key.hdvd have (↑q : ℤ) ∣ x - (↑c : ℤ)

                   Leaves x = (↑c : ℤ), with hdvd : (↑q : ℤ) ∣ x - (↑c : ℤ).

                   Uses library Exists.intro Existential introduction. .

                   Lean, line 238

                               have hdvd : (q : ℤ) ∣ x - c := ⟨x / q, by omega⟩

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 238 at 3e4a866f1f30 ↗

                8. s7.hclass.s9.hle.key.habs have |x - (↑c : ℤ)| < (↑q : ℤ)

                   Leaves x = (↑c : ℤ), with habs : |x - (↑c : ℤ)| < (↑q : ℤ).

                   Uses library abs_lt.

                   Lean, line 239

                               have habs : |x - (c : ℤ)| < q := by rw [abs_lt]; constructor <;> omega

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 239 at 3e4a866f1f30 ↗

                9. s7.hclass.s9.hle.key.this have x - (↑c : ℤ) = (0 : ℤ)

                   Leaves x = (↑c : ℤ), with this : x - (↑c : ℤ) = (0 : ℤ).

                   Uses library Int.eq_zero_of_abs_lt_dvd.

                   Lean, line 240

                               have := Int.eq_zero_of_abs_lt_dvd hdvd habs

                   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 240 at 3e4a866f1f30 ↗

          2. s7.hclass.s9.this have (↑T.card : ℝ) ≤ (1 : ℝ)

             Leaves (↑T.card : ℝ) < (65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam', with this : (↑T.card : ℝ) ≤ (1 : ℝ).

             Lean, line 243

                     have : (T.card : ℝ) ≤ 1 := by exact_mod_cast hle

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 243 at 3e4a866f1f30 ↗

   11. s7.hsum have (↑S.card : ℝ) = ∑ c ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = c}.card : ℝ)

       Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hsum : (↑S.card : ℝ) = ∑ c ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = c}.card : ℝ).

       Uses library Finset.range range n is the set of natural numbers less than n. , Finset.card_eq_sum_card_fiberwise.

       Lean, lines 245–255

           have hsum : (S.card : ℝ) = ∑ c ∈ Finset.range q,
               ((S.filter (fun u => (u % (q : ℤ)).toNat = c)).card : ℝ) := by
             rw [Finset.card_eq_sum_card_fiberwise (f := fun u => (u % (q : ℤ)).toNat)
               (t := Finset.range q)]
             · push_cast; rfl
             · intro u _
               simp only [Finset.coe_range, Set.mem_Iio]
               have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1
               have h1 := Int.emod_nonneg u hqZ.ne'
               have h2 := Int.emod_lt_of_pos u hqZ
               omega

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 245–255 at 3e4a866f1f30 ↗

       1. s7.hsum.s1 case

          Leaves (↑(∑ b ∈ Finset.range q, {a ∈ S | (a % (↑q : ℤ)).toNat = b}.card) : ℝ) = ∑ c ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = c}.card : ℝ).

          Lean, line 249

                · push_cast; rfl

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 249 at 3e4a866f1f30 ↗

       2. s7.hsum.s2 case

          Leaves Set.MapsTo (fun (u : ℤ) => (u % (↑q : ℤ)).toNat) (↑S : Set ℤ) (↑(Finset.range q) : Set ℕ).

          Uses library Finset.coe_range, Set.mem_Iio.

          Lean, lines 250–255

                · intro u _
                  simp only [Finset.coe_range, Set.mem_Iio]
                  have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1
                  have h1 := Int.emod_nonneg u hqZ.ne'
                  have h2 := Int.emod_lt_of_pos u hqZ
                  omega

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 250–255 at 3e4a866f1f30 ↗

          1. s7.hsum.s2.hqZ have (0 : ℤ) < (↑q : ℤ)

             Leaves (u % (↑q : ℤ)).toNat < q, with hqZ : (0 : ℤ) < (↑q : ℤ).

             Lean, line 252

                     have hqZ : (0 : ℤ) < q := by exact_mod_cast hq1

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 252 at 3e4a866f1f30 ↗

          2. s7.hsum.s2.h1 have (0 : ℤ) ≤ u % (↑q : ℤ)

             Leaves (u % (↑q : ℤ)).toNat < q, with h1 : (0 : ℤ) ≤ u % (↑q : ℤ).

             Uses library Int.emod_nonneg.

             Lean, line 253

                     have h1 := Int.emod_nonneg u hqZ.ne'

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 253 at 3e4a866f1f30 ↗

          3. s7.hsum.s2.h2 have u % (↑q : ℤ) < (↑q : ℤ)

             Leaves (u % (↑q : ℤ)).toNat < q, with h2 : u % (↑q : ℤ) < (↑q : ℤ).

             Uses library Int.emod_lt_of_pos.

             Lean, line 254

                     have h2 := Int.emod_lt_of_pos u hqZ

             targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 254 at 3e4a866f1f30 ↗

   12. s7.hlt have ∑ i ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = i}.card : ℝ) < ∑ i ∈ Finset.range q, ((65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam')

       Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with hlt : ∑ i ∈ Finset.range q, (↑{u ∈ S | (u % (↑q : ℤ)).toNat = i}.card : ℝ) < ∑ i ∈ Finset.range q, ((65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam').

       Uses library Finset.sum_lt_sum_of_nonempty In an ordered additive commutative monoid, if each summand f i of one nontrivial finite sum is strictly less than the corresponding summand g i of another nontrivial finite sum, then s.sum f < s.sum g. , Finset.nonempty_range_iff.

       Lean, line 256

           have hlt := Finset.sum_lt_sum_of_nonempty (Finset.nonempty_range_iff.mpr (by omega)) hclass

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, line 256 at 3e4a866f1f30 ↗

   13. s7.this have (↑q : ℝ) * ((65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam') = (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam

       Leaves (↑S.card : ℝ) < (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam, with this : (↑q : ℝ) * ((65536 : ℝ) * (N / (↑q : ℝ)) * X + (2 : ℝ) * (↑r : ℝ) * lam') = (65536 : ℝ) * N * X + (2 : ℝ) * (↑r : ℝ) * lam.

       Lean, lines 258–260

           have : (q : ℝ) * (65536 * (N / q) * X + 2 * (r : ℝ) * lam')
               = 65536 * N * X + 2 * (r : ℝ) * lam := by
             rw [hlam']; field_simp

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean, lines 258–260 at 3e4a866f1f30 ↗