Mertens' second theorem, bounded-error form

spec-7d098d5c Opn.erdos_69_mertens_reciprocal_primes

proved

Proposed by a contributor.

$\displaystyle \exists C\ge 0\ \ \forall x\in\mathbb{N},\ x\ge 2:\quad \Bigl\lvert \sum_{p\le x,\ p\ \text{prime}}\frac{1}{p} - \log\log x \Bigr\rvert \le C$

There is a nonnegative real C such that for every natural x ≥ 2 the sum of 1/p over the primes p ≤ x differs from log log x by at most C, with log the natural logarithm (Mathlib's Real.log) and the primes p ≤ x the finset Nat.primesLE x.

unverified · history

Lean

theorem Opn.erdos_69_mertens_reciprocal_primes :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : ℕ, 2 ≤ x →
      |∑ p ∈ Nat.primesLE x, (1 : ℝ) / p - Real.log (Real.log (x : ℝ))| ≤ C := by
  sorry

Why does it end in sorry?

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

How it was proved

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000343.json, merge commit 061cea5f5749.

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.

hM have ∃ (C : ℝ), ∀ (n : ℕ), |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ C
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with hM : ∃ (C : ℝ), ∀ (n : ℕ), |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ C.
Uses library Nat.primesLE, Real.log, Exists.intro, Nat.eq_zero_or_pos, abs_le.
Lean, lines 15–204
```
  have hM : ∃ C : ℝ, ∀ n : ℕ,
      |∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) - Real.log n| ≤ C := by
    -- (a) Stirling lower bound, by induction
    have hstir : ∀ n : ℕ, (n : ℝ) * Real.log n - n ≤ Real.log (n.factorial : ℝ) := by
      intro n
      induction n with
      | zero => simp
      | succ n ih =>
        have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast n.factorial_pos
        have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
        rw [Nat.factorial_succ, Nat.cast_mul, Real.log_mul hn1.ne' hf.ne']
        rcases Nat.eq_zero_or_pos n with h0 | hpos
        · subst h0
          simp
        · have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos
          have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)
              = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm
          have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity)
          have h3 : (n : ℝ) * (((n + 1 : ℕ) : ℝ) / n - 1) = 1 := by
            push_cast
            field_simp
            ring
          have h4 : (n : ℝ) * (Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)) ≤ 1 := by
            rw [h1, ← h3]
            exact mul_le_mul_of_nonneg_left h2 hn0.le
          push_cast at h4 ih ⊢
          nlinarith
    -- (b) the prime-power tail: ∑_{2 ≤ m ≤ k+1} log m / (m (m-1)) ≤ 2
    have htail : ∀ k : ℕ, ∑ m ∈ Finset.Icc 2 (k + 1), Real.log (m : ℝ) / ((m : ℝ) * ((m : ℝ) - 1))
        ≤ 2 - (Real.log ((k + 1 : ℕ) : ℝ) + 2) / ((k + 1 : ℕ) : ℝ) := by
      intro k
      induction k with
      | zero => simp
      | succ k ih =>
        rw [Finset.sum_Icc_succ_top (by omega)]
        have ha : (0 : ℝ) < ((k + 1 : ℕ) : ℝ) := by positivity
        have ha1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ k + 1)
        have hb : (0 : ℝ) < ((k + 1 + 1 : ℕ) : ℝ) := by positivity
        have hbe : ((k + 1 + 1 : ℕ) : ℝ) = ((k + 1 : ℕ) : ℝ) + 1 := by push_cast; ring
        have h1 : Real.log ((k + 1 + 1 : ℕ) : ℝ) - Real.log ((k + 1 : ℕ) : ℝ)
            = Real.log (((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ)) :=
          (Real.log_div hb.ne' ha.ne').symm
        have h2 := Real.log_le_sub_one_of_pos
          (show 0 < ((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ) by positivity)
        rw [← h1, hbe] at h2
        rw [hbe] at hb ⊢
        generalize ((k + 1 : ℕ) : ℝ) = a at *
        generalize Real.log a = L1 at *
        generalize Real.log (a + 1) = L2 at *
        have h3 : (a + 1) / a - 1 = 1 / a := by field_simp; ring
        have h4 : a * (L2 - L1) ≤ 1 := by
          have := mul_le_mul_of_nonneg_left h2 ha.le
          rw [h3] at this
          have e : a * (1 / a) = 1 := by field_simp
          linarith
        have h5 : L2 - L1 ≤ 1 := by
          have : 1 / a ≤ 1 := by rw [div_le_one ha]; exact ha1
          linarith [h3 ▸ h2]
        have e : (L1 + 2) / a - (L2 + 2) / (a + 1) - L2 / ((a + 1) * (a + 1 - 1))
            = (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := by
          rw [show a + 1 - 1 = a by ring]
          field_simp
          ring
        have : 0 ≤ (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) :=
          div_nonneg (by linarith) (by positivity)
        linarith
    refine ⟨3, ?_⟩
    intro n
    rcases Nat.eq_zero_or_pos n with h0 | hpos
    · subst h0
      simp
    have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos
    have hfne : n.factorial ≠ 0 := n.factorial_ne_zero
    -- (c) log n! as a sum over primes ≤ n
    have hfac : Real.log (n.factorial : ℝ)
        = ∑ p ∈ Nat.primesLE n, (n.factorial.factorization p : ℝ) * Real.log (p : ℝ) := by
      rw [Real.log_nat_eq_sum_factorization]
      refine Finsupp.sum_of_support_subset _ ?_ _ (fun i _ => by simp)
      intro p hp
      rw [Nat.support_factorization, Nat.mem_primeFactors] at hp
      exact Nat.mem_primesLE.mpr ⟨(Nat.Prime.dvd_factorial hp.1).mp hp.2.1, hp.1⟩
    -- (d) Legendre bounds on the exponent
    have hleg : ∀ p ∈ Nat.primesLE n,
        (n : ℝ) / p - 1 ≤ (n.factorial.factorization p : ℝ) ∧
          (n.factorial.factorization p : ℝ) ≤ (n : ℝ) / ((p : ℝ) - 1) := by
      intro p hp
      have hpp := (Nat.mem_primesLE.mp hp).2
      have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast hpp.two_le
      have hp0 : (0 : ℝ) < p := by linarith
      constructor
      · have hd : p ^ (n / p) ∣ n.factorial := by
          have h1 : n.factorial.factorization p ≥ n / p := by
            have h2 := Nat.factorization_factorial_mul (n := n / p) hpp
            have h3 : (p * (n / p)).factorial ∣ n.factorial :=
              Nat.factorial_dvd_factorial (Nat.mul_div_le n p)
            have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p
            omega
          exact (hpp.pow_dvd_iff_le_factorization hfne).mpr h1
        have h1 : n / p ≤ n.factorial.factorization p :=
          (hpp.pow_dvd_iff_le_factorization hfne).mp hd
        have h2 : (n : ℝ) < ((n / p : ℕ) : ℝ) * p + p := by
          have : n < n / p * p + p := by
            have := Nat.div_add_mod n p
            have := Nat.mod_lt n hpp.pos
            nlinarith [Nat.mul_comm p (n / p)]
          exact_mod_cast this
        have h3 : ((n / p : ℕ) : ℝ) ≤ (n.factorial.factorization p : ℝ) := by exact_mod_cast h1
        rw [sub_le_iff_le_add, div_le_iff₀ hp0]
        nlinarith
      · have h1 : (p - 1) * n.factorial.factorization p ≤ n := by
          rw [← Nat.multiplicity_eq_factorization hpp hfne, hpp.sub_one_mul_multiplicity_factorial]
          exact Nat.sub_le _ _
        have h2 : ((p : ℝ) - 1) * (n.factorial.factorization p : ℝ) ≤ n := by
          have : (((p - 1 : ℕ) : ℝ)) * (n.factorial.factorization p : ℝ) ≤ n := by exact_mod_cast h1
          rwa [Nat.cast_sub hpp.one_le, Nat.cast_one] at this
        rw [le_div_iff₀ (by linarith)]
        linarith
    have hlogp : ∀ p ∈ Nat.primesLE n, 0 ≤ Real.log (p : ℝ) := fun p _ =>
      Real.log_natCast_nonneg p
    -- (e) Chebyshev
    have hθ : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) ≤ Real.log 4 * n := by
      have h := Chebyshev.theta_le_log4_mul_x (x := (n : ℝ)) hn0.le
      rw [Chebyshev.theta_eq_sum_Icc, Nat.floor_natCast] at h
      refine le_trans (le_of_eq ?_) h
      refine Finset.sum_congr ?_ (fun _ _ => rfl)
      ext p
      simp [Nat.mem_primesLE]
    have hl4 : Real.log 4 ≤ 3 := by
      have := Real.log_le_sub_one_of_pos (show (0 : ℝ) < 4 by norm_num)
      linarith
    -- (f) upper bound
    have hup : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ)
        ≤ (n : ℝ) * Real.log n + Real.log 4 * n := by
      have h1 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ)
          ≤ Real.log (n.factorial : ℝ) := by
        rw [hfac]
        exact Finset.sum_le_sum fun p hp =>
          mul_le_mul_of_nonneg_right (hleg p hp).1 (hlogp p hp)
      have h2 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ)
          = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ)
            - ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) := by
        rw [Finset.mul_sum, ← Finset.sum_sub_distrib]
        exact Finset.sum_congr rfl fun p _ => by ring
      have h3 : Real.log (n.factorial : ℝ) ≤ (n : ℝ) * Real.log n := by
        rw [← Real.log_pow]
        exact Real.log_le_log (by exact_mod_cast n.factorial_pos)
          (by exact_mod_cast Nat.factorial_le_pow n)
      linarith
    -- (g) lower bound
    have hlo : (n : ℝ) * Real.log n - n
        ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) + (n : ℝ) * 2 := by
      have h1 : Real.log (n.factorial : ℝ)
          ≤ ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ) := by
        rw [hfac]
        exact Finset.sum_le_sum fun p hp =>
          mul_le_mul_of_nonneg_right (hleg p hp).2 (hlogp p hp)
      have h2 : ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ)
          = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ)
            + (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) := by
        rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
        refine Finset.sum_congr rfl fun p hp => ?_
        have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast (Nat.mem_primesLE.mp hp).2.two_le
        have : (p : ℝ) - 1 ≠ 0 := by linarith
        have : (p : ℝ) ≠ 0 := by linarith
        field_simp
        ring
      have h3 : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) ≤ 2 := by
        have hsub : Nat.primesLE n ⊆ Finset.Icc 2 (n - 1 + 1) := by
          intro p hp
          have := Nat.mem_primesLE.mp hp
          have := this.2.two_le
          rw [Finset.mem_Icc]
          omega
        refine (Finset.sum_le_sum_of_subset_of_nonneg hsub fun m hm _ => ?_).trans ?_
        · have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast (Finset.mem_Icc.mp hm).1
          exact div_nonneg (Real.log_natCast_nonneg m) (by nlinarith)
        · refine (htail (n - 1)).trans ?_
          have : 0 ≤ (Real.log ((n - 1 + 1 : ℕ) : ℝ) + 2) / ((n - 1 + 1 : ℕ) : ℝ) :=
            div_nonneg (by linarith [Real.log_natCast_nonneg (n - 1 + 1)]) (by positivity)
          linarith
      have h4 := mul_le_mul_of_nonneg_left h3 hn0.le
      linarith [hstir n]
    rw [abs_le]
    constructor
    · have : (n : ℝ) * (Real.log n - 3) ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) := by
        linarith
      linarith [le_of_mul_le_mul_left this hn0]
    · have : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) ≤ (n : ℝ) * (Real.log n + 3) := by
        nlinarith
      linarith [le_of_mul_le_mul_left this hn0]
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 15–204 at 061cea5f5749 ↗
1. hM.hstir have ∀ (n : ℕ), (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ Real.log (↑n.factorial : ℝ)
  Leaves ∃ (C : ℝ), ∀ (n : ℕ), |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ C, with hstir : ∀ (n : ℕ), (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ Real.log (↑n.factorial : ℝ).
  Uses library Real.log.
  Lean, lines 18–41
  have hstir : ∀ n : ℕ, (n : ℝ) * Real.log n - n ≤ Real.log (n.factorial : ℝ) := by intro n induction n with | zero => simp | succ n ih => have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast n.factorial_pos have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity rw [Nat.factorial_succ, Nat.cast_mul, Real.log_mul hn1.ne' hf.ne'] rcases Nat.eq_zero_or_pos n with h0 | hpos · subst h0 simp · have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity) have h3 : (n : ℝ) * (((n + 1 : ℕ) : ℝ) / n - 1) = 1 := by push_cast field_simp ring have h4 : (n : ℝ) * (Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)) ≤ 1 := by rw [h1, ← h3] exact mul_le_mul_of_nonneg_left h2 hn0.le push_cast at h4 ih ⊢ nlinarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 18–41 at 061cea5f5749 ↗
  hM.hstir.s1 case routine: simp
  Leaves (↑(0 : ℕ) : ℝ) * Real.log (↑(0 : ℕ) : ℝ) - (↑(0 : ℕ) : ℝ) ≤ Real.log (↑(Nat.factorial (0 : ℕ)) : ℝ).
  Uses library Nat.zero.
  Lean, line 21
  | zero => simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 21 at 061cea5f5749 ↗
  hM.hstir.s2 case
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)).factorial : ℝ), with n : ℕ, ih : (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ Real.log (↑n.factorial : ℝ).
  Uses library Nat.succ, Nat.factorial_succ, Nat.cast_mul, Real.log_mul, Nat.eq_zero_or_pos.
  Lean, lines 22–41
  | succ n ih => have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast n.factorial_pos have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity rw [Nat.factorial_succ, Nat.cast_mul, Real.log_mul hn1.ne' hf.ne'] rcases Nat.eq_zero_or_pos n with h0 | hpos · subst h0 simp · have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity) have h3 : (n : ℝ) * (((n + 1 : ℕ) : ℝ) / n - 1) = 1 := by push_cast field_simp ring have h4 : (n : ℝ) * (Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)) ≤ 1 := by rw [h1, ← h3] exact mul_le_mul_of_nonneg_left h2 hn0.le push_cast at h4 ih ⊢ nlinarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 22–41 at 061cea5f5749 ↗
  hM.hstir.s2.hf have (0 : ℝ) < (↑n.factorial : ℝ)
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)).factorial : ℝ), with hf : (0 : ℝ) < (↑n.factorial : ℝ).
  Lean, line 23
  have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast n.factorial_pos
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 23 at 061cea5f5749 ↗
  hM.hstir.s2.hn1 have (0 : ℝ) < (↑(n + (1 : ℕ)) : ℝ) routine: positivity
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)).factorial : ℝ), with hn1 : (0 : ℝ) < (↑(n + (1 : ℕ)) : ℝ).
  Lean, line 24
  have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 24 at 061cea5f5749 ↗
  hM.hstir.s2.s3 case
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ).
  Lean, lines 27–28
  · subst h0 simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 27–28 at 061cea5f5749 ↗
  hM.hstir.s2.s4 case
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ).
  Lean, lines 29–41
  · have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity) have h3 : (n : ℝ) * (((n + 1 : ℕ) : ℝ) / n - 1) = 1 := by push_cast field_simp ring have h4 : (n : ℝ) * (Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)) ≤ 1 := by rw [h1, ← h3] exact mul_le_mul_of_nonneg_left h2 hn0.le push_cast at h4 ih ⊢ nlinarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 29–41 at 061cea5f5749 ↗
  hM.hstir.s2.s4.hn0 have (0 : ℝ) < (↑n : ℝ)
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ), with hn0 : (0 : ℝ) < (↑n : ℝ).
  Lean, line 29
  · have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 29 at 061cea5f5749 ↗
  hM.hstir.s2.s4.h1 have Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) = Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ))
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ), with h1 : Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) = Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ)).
  Uses library Real.log, Real.log_div.
  Lean, lines 30–31
  have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 30–31 at 061cea5f5749 ↗
  hM.hstir.s2.s4.h2 have Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ)) ≤ (↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ)
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ), with h2 : Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ)) ≤ (↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ).
  Uses library Real.log_le_sub_one_of_pos.
  Lean, line 32
  have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 32 at 061cea5f5749 ↗
  hM.hstir.s2.s4.h3 have (↑n : ℝ) * ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ)) = (1 : ℝ)
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ), with h3 : (↑n : ℝ) * ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ)) = (1 : ℝ).
  Lean, lines 33–36
  have h3 : (n : ℝ) * (((n + 1 : ℕ) : ℝ) / n - 1) = 1 := by push_cast field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 33–36 at 061cea5f5749 ↗
  hM.hstir.s2.s4.h4 have (↑n : ℝ) * (Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ)) ≤ (1 : ℝ)
  Leaves (↑(n + (1 : ℕ)) : ℝ) * Real.log (↑(n + (1 : ℕ)) : ℝ) - (↑(n + (1 : ℕ)) : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ) + Real.log (↑n.factorial : ℝ), with h4 : (↑n : ℝ) * (Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ)) ≤ (1 : ℝ).
  Uses library Real.log, mul_le_mul_of_nonneg_left.
  Lean, lines 37–39
  have h4 : (n : ℝ) * (Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)) ≤ 1 := by rw [h1, ← h3] exact mul_le_mul_of_nonneg_left h2 hn0.le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 37–39 at 061cea5f5749 ↗
2. hM.htail have ∀ (k : ℕ), ∑ m ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ)) : ℝ)
  Leaves ∃ (C : ℝ), ∀ (n : ℕ), |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ C, with htail : ∀ (k : ℕ), ∑ m ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ)) : ℝ).
  Uses library Finset.Icc, Real.log.
  Lean, lines 43–80
  have htail : ∀ k : ℕ, ∑ m ∈ Finset.Icc 2 (k + 1), Real.log (m : ℝ) / ((m : ℝ) * ((m : ℝ) - 1)) ≤ 2 - (Real.log ((k + 1 : ℕ) : ℝ) + 2) / ((k + 1 : ℕ) : ℝ) := by intro k induction k with | zero => simp | succ k ih => rw [Finset.sum_Icc_succ_top (by omega)] have ha : (0 : ℝ) < ((k + 1 : ℕ) : ℝ) := by positivity have ha1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ k + 1) have hb : (0 : ℝ) < ((k + 1 + 1 : ℕ) : ℝ) := by positivity have hbe : ((k + 1 + 1 : ℕ) : ℝ) = ((k + 1 : ℕ) : ℝ) + 1 := by push_cast; ring have h1 : Real.log ((k + 1 + 1 : ℕ) : ℝ) - Real.log ((k + 1 : ℕ) : ℝ) = Real.log (((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ)) := (Real.log_div hb.ne' ha.ne').symm have h2 := Real.log_le_sub_one_of_pos (show 0 < ((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ) by positivity) rw [← h1, hbe] at h2 rw [hbe] at hb ⊢ generalize ((k + 1 : ℕ) : ℝ) = a at * generalize Real.log a = L1 at * generalize Real.log (a + 1) = L2 at * have h3 : (a + 1) / a - 1 = 1 / a := by field_simp; ring have h4 : a * (L2 - L1) ≤ 1 := by have := mul_le_mul_of_nonneg_left h2 ha.le rw [h3] at this have e : a * (1 / a) = 1 := by field_simp linarith have h5 : L2 - L1 ≤ 1 := by have : 1 / a ≤ 1 := by rw [div_le_one ha]; exact ha1 linarith [h3 ▸ h2] have e : (L1 + 2) / a - (L2 + 2) / (a + 1) - L2 / ((a + 1) * (a + 1 - 1)) = (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := by rw [show a + 1 - 1 = a by ring] field_simp ring have : 0 ≤ (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := div_nonneg (by linarith) (by positivity) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 43–80 at 061cea5f5749 ↗
  hM.htail.s1 case routine: simp
  Leaves ∑ m ∈ Finset.Icc (2 : ℕ) ((0 : ℕ) + (1 : ℕ)), Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑((0 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑((0 : ℕ) + (1 : ℕ)) : ℝ).
  Uses library Nat.zero.
  Lean, line 47
  | zero => simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 47 at 061cea5f5749 ↗
  hM.htail.s2 case
  Leaves ∑ m ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ) + (1 : ℕ)), Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with k : ℕ, ih : ∑ m ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ)) : ℝ).
  Uses library Nat.succ, Finset.sum_Icc_succ_top, Real.log.
  Lean, lines 48–80
  | succ k ih => rw [Finset.sum_Icc_succ_top (by omega)] have ha : (0 : ℝ) < ((k + 1 : ℕ) : ℝ) := by positivity have ha1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ k + 1) have hb : (0 : ℝ) < ((k + 1 + 1 : ℕ) : ℝ) := by positivity have hbe : ((k + 1 + 1 : ℕ) : ℝ) = ((k + 1 : ℕ) : ℝ) + 1 := by push_cast; ring have h1 : Real.log ((k + 1 + 1 : ℕ) : ℝ) - Real.log ((k + 1 : ℕ) : ℝ) = Real.log (((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ)) := (Real.log_div hb.ne' ha.ne').symm have h2 := Real.log_le_sub_one_of_pos (show 0 < ((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ) by positivity) rw [← h1, hbe] at h2 rw [hbe] at hb ⊢ generalize ((k + 1 : ℕ) : ℝ) = a at * generalize Real.log a = L1 at * generalize Real.log (a + 1) = L2 at * have h3 : (a + 1) / a - 1 = 1 / a := by field_simp; ring have h4 : a * (L2 - L1) ≤ 1 := by have := mul_le_mul_of_nonneg_left h2 ha.le rw [h3] at this have e : a * (1 / a) = 1 := by field_simp linarith have h5 : L2 - L1 ≤ 1 := by have : 1 / a ≤ 1 := by rw [div_le_one ha]; exact ha1 linarith [h3 ▸ h2] have e : (L1 + 2) / a - (L2 + 2) / (a + 1) - L2 / ((a + 1) * (a + 1 - 1)) = (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := by rw [show a + 1 - 1 = a by ring] field_simp ring have : 0 ≤ (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := div_nonneg (by linarith) (by positivity) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 48–80 at 061cea5f5749 ↗
  hM.htail.s2.ha have (0 : ℝ) < (↑(k + (1 : ℕ)) : ℝ) routine: positivity
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) * ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with ha : (0 : ℝ) < (↑(k + (1 : ℕ)) : ℝ).
  Lean, line 50
  have ha : (0 : ℝ) < ((k + 1 : ℕ) : ℝ) := by positivity
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 50 at 061cea5f5749 ↗
  hM.htail.s2.ha1 have (1 : ℝ) ≤ (↑(k + (1 : ℕ)) : ℝ)
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) * ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with ha1 : (1 : ℝ) ≤ (↑(k + (1 : ℕ)) : ℝ).
  Lean, line 51
  have ha1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ k + 1)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 51 at 061cea5f5749 ↗
  hM.htail.s2.hb have (0 : ℝ) < (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) routine: positivity
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) * ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with hb : (0 : ℝ) < (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ).
  Lean, line 52
  have hb : (0 : ℝ) < ((k + 1 + 1 : ℕ) : ℝ) := by positivity
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 52 at 061cea5f5749 ↗
  hM.htail.s2.hbe have (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) = (↑(k + (1 : ℕ)) : ℝ) + (1 : ℝ)
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) * ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with hbe : (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) = (↑(k + (1 : ℕ)) : ℝ) + (1 : ℝ).
  Lean, line 53
  have hbe : ((k + 1 + 1 : ℕ) : ℝ) = ((k + 1 : ℕ) : ℝ) + 1 := by push_cast; ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 53 at 061cea5f5749 ↗
  hM.htail.s2.h1 have Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - Real.log (↑(k + (1 : ℕ)) : ℝ) = Real.log ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / (↑(k + (1 : ℕ)) : ℝ))
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) * ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with h1 : Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - Real.log (↑(k + (1 : ℕ)) : ℝ) = Real.log ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / (↑(k + (1 : ℕ)) : ℝ)).
  Uses library Real.log, Real.log_div.
  Lean, lines 54–56
  have h1 : Real.log ((k + 1 + 1 : ℕ) : ℝ) - Real.log ((k + 1 : ℕ) : ℝ) = Real.log (((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ)) := (Real.log_div hb.ne' ha.ne').symm
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 54–56 at 061cea5f5749 ↗
  hM.htail.s2.h2 have Real.log ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / (↑(k + (1 : ℕ)) : ℝ)) ≤ (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / (↑(k + (1 : ℕ)) : ℝ) - (1 : ℝ)
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) * ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (Real.log (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ), with h2 : Real.log ((↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / (↑(k + (1 : ℕ)) : ℝ)) ≤ (↑(k + (1 : ℕ) + (1 : ℕ)) : ℝ) / (↑(k + (1 : ℕ)) : ℝ) - (1 : ℝ).
  Uses library Real.log_le_sub_one_of_pos.
  Lean, lines 57–58
  have h2 := Real.log_le_sub_one_of_pos (show 0 < ((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ) by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 57–58 at 061cea5f5749 ↗
  hM.htail.s2.h3 have (a + (1 : ℝ)) / a - (1 : ℝ) = (1 : ℝ) / a routine: field_simp, ring
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (L2 + (2 : ℝ)) / (a + (1 : ℝ)), with h3 : (a + (1 : ℝ)) / a - (1 : ℝ) = (1 : ℝ) / a.
  Lean, line 64
  have h3 : (a + 1) / a - 1 = 1 / a := by field_simp; ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 64 at 061cea5f5749 ↗
  hM.htail.s2.h4 have a * (L2 - L1) ≤ (1 : ℝ)
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (L2 + (2 : ℝ)) / (a + (1 : ℝ)), with h4 : a * (L2 - L1) ≤ (1 : ℝ).
  Lean, lines 65–69
  have h4 : a * (L2 - L1) ≤ 1 := by have := mul_le_mul_of_nonneg_left h2 ha.le rw [h3] at this have e : a * (1 / a) = 1 := by field_simp linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 65–69 at 061cea5f5749 ↗
  hM.htail.s2.h4.this have a * (L2 - L1) ≤ a * ((a + (1 : ℝ)) / a - (1 : ℝ))
  Leaves a * (L2 - L1) ≤ (1 : ℝ), with this : a * (L2 - L1) ≤ a * ((a + (1 : ℝ)) / a - (1 : ℝ)).
  Uses library mul_le_mul_of_nonneg_left.
  Lean, line 66
  have := mul_le_mul_of_nonneg_left h2 ha.le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 66 at 061cea5f5749 ↗
  hM.htail.s2.h4.e have a * ((1 : ℝ) / a) = (1 : ℝ) routine: field_simp
  Leaves a * (L2 - L1) ≤ (1 : ℝ), with e : a * ((1 : ℝ) / a) = (1 : ℝ).
  Lean, line 68
  have e : a * (1 / a) = 1 := by field_simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 68 at 061cea5f5749 ↗
  hM.htail.s2.h5 have L2 - L1 ≤ (1 : ℝ)
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (L2 + (2 : ℝ)) / (a + (1 : ℝ)), with h5 : L2 - L1 ≤ (1 : ℝ).
  Lean, lines 70–72
  have h5 : L2 - L1 ≤ 1 := by have : 1 / a ≤ 1 := by rw [div_le_one ha]; exact ha1 linarith [h3 ▸ h2]
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 70–72 at 061cea5f5749 ↗
  hM.htail.s2.h5.this have (1 : ℝ) / a ≤ (1 : ℝ)
  Leaves L2 - L1 ≤ (1 : ℝ), with this : (1 : ℝ) / a ≤ (1 : ℝ).
  Uses library div_le_one.
  Lean, line 71
  have : 1 / a ≤ 1 := by rw [div_le_one ha]; exact ha1
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 71 at 061cea5f5749 ↗
  hM.htail.s2.e have (L1 + (2 : ℝ)) / a - (L2 + (2 : ℝ)) / (a + (1 : ℝ)) - L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) = ((2 : ℝ) - (a * (L2 - L1) + (L2 - L1))) / (a * (a + (1 : ℝ)))
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (L2 + (2 : ℝ)) / (a + (1 : ℝ)), with e : (L1 + (2 : ℝ)) / a - (L2 + (2 : ℝ)) / (a + (1 : ℝ)) - L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) = ((2 : ℝ) - (a * (L2 - L1) + (L2 - L1))) / (a * (a + (1 : ℝ))).
  Lean, lines 73–77
  have e : (L1 + 2) / a - (L2 + 2) / (a + 1) - L2 / ((a + 1) * (a + 1 - 1)) = (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := by rw [show a + 1 - 1 = a by ring] field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 73–77 at 061cea5f5749 ↗
  hM.htail.s2.this have (0 : ℝ) ≤ ((2 : ℝ) - (a * (L2 - L1) + (L2 - L1))) / (a * (a + (1 : ℝ)))
  Leaves ∑ k ∈ Finset.Icc (2 : ℕ) (k + (1 : ℕ)), Real.log (↑k : ℝ) / ((↑k : ℝ) * ((↑k : ℝ) - (1 : ℝ))) + L2 / ((a + (1 : ℝ)) * (a + (1 : ℝ) - (1 : ℝ))) ≤ (2 : ℝ) - (L2 + (2 : ℝ)) / (a + (1 : ℝ)), with this : (0 : ℝ) ≤ ((2 : ℝ) - (a * (L2 - L1) + (L2 - L1))) / (a * (a + (1 : ℝ))).
  Uses library div_nonneg.
  Lean, lines 78–79
  have : 0 ≤ (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := div_nonneg (by linarith) (by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 78–79 at 061cea5f5749 ↗
3. hM.s3 case
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ).
  Lean, lines 84–85
  · subst h0 simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 84–85 at 061cea5f5749 ↗
4. hM.hn0 have (0 : ℝ) < (↑n : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hn0 : (0 : ℝ) < (↑n : ℝ).
  Lean, line 86
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 86 at 061cea5f5749 ↗
5. hM.hfne have n.factorial ≠ (0 : ℕ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hfne : n.factorial ≠ (0 : ℕ).
  Lean, line 87
  have hfne : n.factorial ≠ 0 := n.factorial_ne_zero
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 87 at 061cea5f5749 ↗
6. hM.hfac have Real.log (↑n.factorial : ℝ) = ∑ p ∈ n.primesLE, (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) * Real.log (↑p : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hfac : Real.log (↑n.factorial : ℝ) = ∑ p ∈ n.primesLE, (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) * Real.log (↑p : ℝ).
  Uses library Real.log, Nat.primesLE, Real.log_nat_eq_sum_factorization, Finsupp.sum_of_support_subset, Nat.support_factorization, Nat.mem_primeFactors, Nat.mem_primesLE, And.intro, Nat.Prime.dvd_factorial.
  Lean, lines 89–95
  have hfac : Real.log (n.factorial : ℝ) = ∑ p ∈ Nat.primesLE n, (n.factorial.factorization p : ℝ) * Real.log (p : ℝ) := by rw [Real.log_nat_eq_sum_factorization] refine Finsupp.sum_of_support_subset _ ?_ _ (fun i _ => by simp) intro p hp rw [Nat.support_factorization, Nat.mem_primeFactors] at hp exact Nat.mem_primesLE.mpr ⟨(Nat.Prime.dvd_factorial hp.1).mp hp.2.1, hp.1⟩
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 89–95 at 061cea5f5749 ↗
7. hM.hleg have ∀ p ∈ n.primesLE, (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ∧ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ))
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hleg : ∀ p ∈ n.primesLE, (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ∧ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)).
  Uses library Nat.primesLE.
  Lean, lines 97–131
  have hleg : ∀ p ∈ Nat.primesLE n, (n : ℝ) / p - 1 ≤ (n.factorial.factorization p : ℝ) ∧ (n.factorial.factorization p : ℝ) ≤ (n : ℝ) / ((p : ℝ) - 1) := by intro p hp have hpp := (Nat.mem_primesLE.mp hp).2 have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast hpp.two_le have hp0 : (0 : ℝ) < p := by linarith constructor · have hd : p ^ (n / p) ∣ n.factorial := by have h1 : n.factorial.factorization p ≥ n / p := by have h2 := Nat.factorization_factorial_mul (n := n / p) hpp have h3 : (p * (n / p)).factorial ∣ n.factorial := Nat.factorial_dvd_factorial (Nat.mul_div_le n p) have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p omega exact (hpp.pow_dvd_iff_le_factorization hfne).mpr h1 have h1 : n / p ≤ n.factorial.factorization p := (hpp.pow_dvd_iff_le_factorization hfne).mp hd have h2 : (n : ℝ) < ((n / p : ℕ) : ℝ) * p + p := by have : n < n / p * p + p := by have := Nat.div_add_mod n p have := Nat.mod_lt n hpp.pos nlinarith [Nat.mul_comm p (n / p)] exact_mod_cast this have h3 : ((n / p : ℕ) : ℝ) ≤ (n.factorial.factorization p : ℝ) := by exact_mod_cast h1 rw [sub_le_iff_le_add, div_le_iff₀ hp0] nlinarith · have h1 : (p - 1) * n.factorial.factorization p ≤ n := by rw [← Nat.multiplicity_eq_factorization hpp hfne, hpp.sub_one_mul_multiplicity_factorial] exact Nat.sub_le _ _ have h2 : ((p : ℝ) - 1) * (n.factorial.factorization p : ℝ) ≤ n := by have : (((p - 1 : ℕ) : ℝ)) * (n.factorial.factorization p : ℝ) ≤ n := by exact_mod_cast h1 rwa [Nat.cast_sub hpp.one_le, Nat.cast_one] at this rw [le_div_iff₀ (by linarith)] linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 97–131 at 061cea5f5749 ↗
  hM.hleg.hpp have Nat.Prime p
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ∧ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)), with hpp : Nat.Prime p.
  Uses library Nat.mem_primesLE.
  Lean, line 101
  have hpp := (Nat.mem_primesLE.mp hp).2
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 101 at 061cea5f5749 ↗
  hM.hleg.hp2 have (2 : ℝ) ≤ (↑p : ℝ)
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ∧ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)), with hp2 : (2 : ℝ) ≤ (↑p : ℝ).
  Lean, line 102
  have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast hpp.two_le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 102 at 061cea5f5749 ↗
  hM.hleg.hp0 have (0 : ℝ) < (↑p : ℝ) routine: linarith
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ∧ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)), with hp0 : (0 : ℝ) < (↑p : ℝ).
  Lean, line 103
  have hp0 : (0 : ℝ) < p := by linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 103 at 061cea5f5749 ↗
  hM.hleg.s4 case
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ).
  Uses library sub_le_iff_le_add, div_le_iff₀.
  Lean, lines 105–123
  · have hd : p ^ (n / p) ∣ n.factorial := by have h1 : n.factorial.factorization p ≥ n / p := by have h2 := Nat.factorization_factorial_mul (n := n / p) hpp have h3 : (p * (n / p)).factorial ∣ n.factorial := Nat.factorial_dvd_factorial (Nat.mul_div_le n p) have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p omega exact (hpp.pow_dvd_iff_le_factorization hfne).mpr h1 have h1 : n / p ≤ n.factorial.factorization p := (hpp.pow_dvd_iff_le_factorization hfne).mp hd have h2 : (n : ℝ) < ((n / p : ℕ) : ℝ) * p + p := by have : n < n / p * p + p := by have := Nat.div_add_mod n p have := Nat.mod_lt n hpp.pos nlinarith [Nat.mul_comm p (n / p)] exact_mod_cast this have h3 : ((n / p : ℕ) : ℝ) ≤ (n.factorial.factorization p : ℝ) := by exact_mod_cast h1 rw [sub_le_iff_le_add, div_le_iff₀ hp0] nlinarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 105–123 at 061cea5f5749 ↗
  hM.hleg.s4.hd have p ^ (n / p) ∣ n.factorial
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ), with hd : p ^ (n / p) ∣ n.factorial.
  Lean, lines 105–112
  · have hd : p ^ (n / p) ∣ n.factorial := by have h1 : n.factorial.factorization p ≥ n / p := by have h2 := Nat.factorization_factorial_mul (n := n / p) hpp have h3 : (p * (n / p)).factorial ∣ n.factorial := Nat.factorial_dvd_factorial (Nat.mul_div_le n p) have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p omega exact (hpp.pow_dvd_iff_le_factorization hfne).mpr h1
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 105–112 at 061cea5f5749 ↗
  hM.hleg.s4.hd.h1 have (n.factorial.factorization : ℕ → ℕ) p ≥ n / p
  Leaves p ^ (n / p) ∣ n.factorial, with h1 : (n.factorial.factorization : ℕ → ℕ) p ≥ n / p.
  Lean, lines 106–111
  have h1 : n.factorial.factorization p ≥ n / p := by have h2 := Nat.factorization_factorial_mul (n := n / p) hpp have h3 : (p * (n / p)).factorial ∣ n.factorial := Nat.factorial_dvd_factorial (Nat.mul_div_le n p) have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p omega
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 106–111 at 061cea5f5749 ↗
  hM.hleg.s4.hd.h1.h2 have ((p * (n / p)).factorial.factorization : ℕ → ℕ) p = ((n / p).factorial.factorization : ℕ → ℕ) p + n / p
  Leaves (n.factorial.factorization : ℕ → ℕ) p ≥ n / p, with h2 : ((p * (n / p)).factorial.factorization : ℕ → ℕ) p = ((n / p).factorial.factorization : ℕ → ℕ) p + n / p.
  Uses library Nat.factorization_factorial_mul.
  Lean, line 107
  have h2 := Nat.factorization_factorial_mul (n := n / p) hpp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 107 at 061cea5f5749 ↗
  hM.hleg.s4.hd.h1.h3 have (p * (n / p)).factorial ∣ n.factorial
  Leaves (n.factorial.factorization : ℕ → ℕ) p ≥ n / p, with h3 : (p * (n / p)).factorial ∣ n.factorial.
  Uses library Nat.factorial_dvd_factorial, Nat.mul_div_le.
  Lean, lines 108–109
  have h3 : (p * (n / p)).factorial ∣ n.factorial := Nat.factorial_dvd_factorial (Nat.mul_div_le n p)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 108–109 at 061cea5f5749 ↗
  hM.hleg.s4.hd.h1.h4 have ((p * (n / p)).factorial.factorization : ℕ → ℕ) p ≤ (n.factorial.factorization : ℕ → ℕ) p
  Leaves (n.factorial.factorization : ℕ → ℕ) p ≥ n / p, with h4 : ((p * (n / p)).factorial.factorization : ℕ → ℕ) p ≤ (n.factorial.factorization : ℕ → ℕ) p.
  Uses library Nat.factorization_le_iff_dvd, Nat.factorial_ne_zero.
  Lean, line 110
  have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 110 at 061cea5f5749 ↗
  hM.hleg.s4.h1 have n / p ≤ (n.factorial.factorization : ℕ → ℕ) p
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ), with h1 : n / p ≤ (n.factorial.factorization : ℕ → ℕ) p.
  Lean, lines 113–114
  have h1 : n / p ≤ n.factorial.factorization p := (hpp.pow_dvd_iff_le_factorization hfne).mp hd
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 113–114 at 061cea5f5749 ↗
  hM.hleg.s4.h2 have (↑n : ℝ) < (↑(n / p) : ℝ) * (↑p : ℝ) + (↑p : ℝ)
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ), with h2 : (↑n : ℝ) < (↑(n / p) : ℝ) * (↑p : ℝ) + (↑p : ℝ).
  Lean, lines 115–120
  have h2 : (n : ℝ) < ((n / p : ℕ) : ℝ) * p + p := by have : n < n / p * p + p := by have := Nat.div_add_mod n p have := Nat.mod_lt n hpp.pos nlinarith [Nat.mul_comm p (n / p)] exact_mod_cast this
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 115–120 at 061cea5f5749 ↗
  hM.hleg.s4.h2.this have n < n / p * p + p
  Leaves (↑n : ℝ) < (↑(n / p) : ℝ) * (↑p : ℝ) + (↑p : ℝ), with this : n < n / p * p + p.
  Uses library Nat.mul_comm.
  Lean, lines 116–119
  have : n < n / p * p + p := by have := Nat.div_add_mod n p have := Nat.mod_lt n hpp.pos nlinarith [Nat.mul_comm p (n / p)]
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 116–119 at 061cea5f5749 ↗
  hM.hleg.s4.h2.this.s1 have p * (n / p) + n % p = n
  Leaves n < n / p * p + p, with this : p * (n / p) + n % p = n.
  Uses library Nat.div_add_mod.
  Lean, line 117
  have := Nat.div_add_mod n p
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 117 at 061cea5f5749 ↗
  hM.hleg.s4.h2.this.s2 have n % p < p
  Leaves n < n / p * p + p, with this : n % p < p.
  Uses library Nat.mod_lt.
  Lean, line 118
  have := Nat.mod_lt n hpp.pos
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 118 at 061cea5f5749 ↗
  hM.hleg.s4.h3 have (↑(n / p) : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ)
  Leaves (↑n : ℝ) / (↑p : ℝ) - (1 : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ), with h3 : (↑(n / p) : ℝ) ≤ (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ).
  Lean, line 121
  have h3 : ((n / p : ℕ) : ℝ) ≤ (n.factorial.factorization p : ℝ) := by exact_mod_cast h1
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 121 at 061cea5f5749 ↗
  hM.hleg.s5 case
  Leaves (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)).
  Uses library le_div_iff₀.
  Lean, lines 124–131
  · have h1 : (p - 1) * n.factorial.factorization p ≤ n := by rw [← Nat.multiplicity_eq_factorization hpp hfne, hpp.sub_one_mul_multiplicity_factorial] exact Nat.sub_le _ _ have h2 : ((p : ℝ) - 1) * (n.factorial.factorization p : ℝ) ≤ n := by have : (((p - 1 : ℕ) : ℝ)) * (n.factorial.factorization p : ℝ) ≤ n := by exact_mod_cast h1 rwa [Nat.cast_sub hpp.one_le, Nat.cast_one] at this rw [le_div_iff₀ (by linarith)] linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 124–131 at 061cea5f5749 ↗
  hM.hleg.s5.h1 have (p - (1 : ℕ)) * (n.factorial.factorization : ℕ → ℕ) p ≤ n
  Leaves (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)), with h1 : (p - (1 : ℕ)) * (n.factorial.factorization : ℕ → ℕ) p ≤ n.
  Uses library Nat.multiplicity_eq_factorization, Nat.sub_le.
  Lean, lines 124–126
  · have h1 : (p - 1) * n.factorial.factorization p ≤ n := by rw [← Nat.multiplicity_eq_factorization hpp hfne, hpp.sub_one_mul_multiplicity_factorial] exact Nat.sub_le _ _
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 124–126 at 061cea5f5749 ↗
  hM.hleg.s5.h2 have ((↑p : ℝ) - (1 : ℝ)) * (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ)
  Leaves (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)), with h2 : ((↑p : ℝ) - (1 : ℝ)) * (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ).
  Uses library Nat.cast_sub, Nat.cast_one.
  Lean, lines 127–129
  have h2 : ((p : ℝ) - 1) * (n.factorial.factorization p : ℝ) ≤ n := by have : (((p - 1 : ℕ) : ℝ)) * (n.factorial.factorization p : ℝ) ≤ n := by exact_mod_cast h1 rwa [Nat.cast_sub hpp.one_le, Nat.cast_one] at this
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 127–129 at 061cea5f5749 ↗
  hM.hleg.s5.h2.this have (↑(p - (1 : ℕ)) : ℝ) * (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ)
  Leaves ((↑p : ℝ) - (1 : ℝ)) * (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ), with this : (↑(p - (1 : ℕ)) : ℝ) * (↑((n.factorial.factorization : ℕ → ℕ) p) : ℝ) ≤ (↑n : ℝ).
  Lean, line 128
  have : (((p - 1 : ℕ) : ℝ)) * (n.factorial.factorization p : ℝ) ≤ n := by exact_mod_cast h1
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 128 at 061cea5f5749 ↗
8. hM.hlogp have ∀ p ∈ n.primesLE, (0 : ℝ) ≤ Real.log (↑p : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hlogp : ∀ p ∈ n.primesLE, (0 : ℝ) ≤ Real.log (↑p : ℝ).
  Uses library Nat.primesLE, Real.log, Real.log_natCast_nonneg.
  Lean, lines 132–133
  have hlogp : ∀ p ∈ Nat.primesLE n, 0 ≤ Real.log (p : ℝ) := fun p _ => Real.log_natCast_nonneg p
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 132–133 at 061cea5f5749 ↗
9. hM.h_x3b8 (hθ) have ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) ≤ Real.log (4 : ℝ) * (↑n : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hθ : ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) ≤ Real.log (4 : ℝ) * (↑n : ℝ).
  Uses library Nat.primesLE, Real.log, Chebyshev.theta_eq_sum_Icc, Nat.floor_natCast, le_trans, le_of_eq, Finset.sum_congr, rfl, Nat.mem_primesLE.
  Lean, lines 135–141
  have hθ : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) ≤ Real.log 4 * n := by have h := Chebyshev.theta_le_log4_mul_x (x := (n : ℝ)) hn0.le rw [Chebyshev.theta_eq_sum_Icc, Nat.floor_natCast] at h refine le_trans (le_of_eq ?_) h refine Finset.sum_congr ?_ (fun _ _ => rfl) ext p simp [Nat.mem_primesLE]
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 135–141 at 061cea5f5749 ↗
  hM.h_x3b8.h have Chebyshev.theta (↑n : ℝ) ≤ Real.log (4 : ℝ) * (↑n : ℝ)
  Leaves ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) ≤ Real.log (4 : ℝ) * (↑n : ℝ), with h : Chebyshev.theta (↑n : ℝ) ≤ Real.log (4 : ℝ) * (↑n : ℝ).
  Uses library Chebyshev.theta_le_log4_mul_x.
  Lean, line 136
  have h := Chebyshev.theta_le_log4_mul_x (x := (n : ℝ)) hn0.le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 136 at 061cea5f5749 ↗
10. hM.hl4 have Real.log (4 : ℝ) ≤ (3 : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hl4 : Real.log (4 : ℝ) ≤ (3 : ℝ).
  Uses library Real.log.
  Lean, lines 142–144
  have hl4 : Real.log 4 ≤ 3 := by have := Real.log_le_sub_one_of_pos (show (0 : ℝ) < 4 by norm_num) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 142–144 at 061cea5f5749 ↗
  hM.hl4.this have Real.log (4 : ℝ) ≤ (4 : ℝ) - (1 : ℝ)
  Leaves Real.log (4 : ℝ) ≤ (3 : ℝ), with this : Real.log (4 : ℝ) ≤ (4 : ℝ) - (1 : ℝ).
  Uses library Real.log_le_sub_one_of_pos.
  Lean, line 143
  have := Real.log_le_sub_one_of_pos (show (0 : ℝ) < 4 by norm_num)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 143 at 061cea5f5749 ↗
11. hM.hup have (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ) + Real.log (4 : ℝ) * (↑n : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hup : (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ) + Real.log (4 : ℝ) * (↑n : ℝ).
  Uses library Nat.primesLE, Real.log.
  Lean, lines 146–162
  have hup : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) ≤ (n : ℝ) * Real.log n + Real.log 4 * n := by have h1 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ) ≤ Real.log (n.factorial : ℝ) := by rw [hfac] exact Finset.sum_le_sum fun p hp => mul_le_mul_of_nonneg_right (hleg p hp).1 (hlogp p hp) have h2 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ) = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) - ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) := by rw [Finset.mul_sum, ← Finset.sum_sub_distrib] exact Finset.sum_congr rfl fun p _ => by ring have h3 : Real.log (n.factorial : ℝ) ≤ (n : ℝ) * Real.log n := by rw [← Real.log_pow] exact Real.log_le_log (by exact_mod_cast n.factorial_pos) (by exact_mod_cast Nat.factorial_le_pow n) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 146–162 at 061cea5f5749 ↗
  hM.hup.h1 have ∑ p ∈ n.primesLE, ((↑n : ℝ) / (↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) ≤ Real.log (↑n.factorial : ℝ)
  Leaves (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ) + Real.log (4 : ℝ) * (↑n : ℝ), with h1 : ∑ p ∈ n.primesLE, ((↑n : ℝ) / (↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) ≤ Real.log (↑n.factorial : ℝ).
  Uses library Nat.primesLE, Real.log, Finset.sum_le_sum, mul_le_mul_of_nonneg_right.
  Lean, lines 148–152
  have h1 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ) ≤ Real.log (n.factorial : ℝ) := by rw [hfac] exact Finset.sum_le_sum fun p hp => mul_le_mul_of_nonneg_right (hleg p hp).1 (hlogp p hp)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 148–152 at 061cea5f5749 ↗
  hM.hup.h2 have ∑ p ∈ n.primesLE, ((↑n : ℝ) / (↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - ∑ p ∈ n.primesLE, Real.log (↑p : ℝ)
  Leaves (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ) + Real.log (4 : ℝ) * (↑n : ℝ), with h2 : ∑ p ∈ n.primesLE, ((↑n : ℝ) / (↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - ∑ p ∈ n.primesLE, Real.log (↑p : ℝ).
  Uses library Nat.primesLE, Real.log, Finset.mul_sum, Finset.sum_sub_distrib, Finset.sum_congr, rfl.
  Lean, lines 153–157
  have h2 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ) = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) - ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) := by rw [Finset.mul_sum, ← Finset.sum_sub_distrib] exact Finset.sum_congr rfl fun p _ => by ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 153–157 at 061cea5f5749 ↗
  hM.hup.h3 have Real.log (↑n.factorial : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ)
  Leaves (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ) + Real.log (4 : ℝ) * (↑n : ℝ), with h3 : Real.log (↑n.factorial : ℝ) ≤ (↑n : ℝ) * Real.log (↑n : ℝ).
  Uses library Real.log, Real.log_pow, Real.log_le_log, Nat.factorial_le_pow.
  Lean, lines 158–161
  have h3 : Real.log (n.factorial : ℝ) ≤ (n : ℝ) * Real.log n := by rw [← Real.log_pow] exact Real.log_le_log (by exact_mod_cast n.factorial_pos) (by exact_mod_cast Nat.factorial_le_pow n)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 158–161 at 061cea5f5749 ↗
12. hM.hlo have (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * (2 : ℝ)
  Leaves |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ (3 : ℝ), with hlo : (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * (2 : ℝ).
  Uses library Real.log, Nat.primesLE.
  Lean, lines 164–196
  have hlo : (n : ℝ) * Real.log n - n ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) + (n : ℝ) * 2 := by have h1 : Real.log (n.factorial : ℝ) ≤ ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ) := by rw [hfac] exact Finset.sum_le_sum fun p hp => mul_le_mul_of_nonneg_right (hleg p hp).2 (hlogp p hp) have h2 : ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ) = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) + (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) := by rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib] refine Finset.sum_congr rfl fun p hp => ?_ have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast (Nat.mem_primesLE.mp hp).2.two_le have : (p : ℝ) - 1 ≠ 0 := by linarith have : (p : ℝ) ≠ 0 := by linarith field_simp ring have h3 : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) ≤ 2 := by have hsub : Nat.primesLE n ⊆ Finset.Icc 2 (n - 1 + 1) := by intro p hp have := Nat.mem_primesLE.mp hp have := this.2.two_le rw [Finset.mem_Icc] omega refine (Finset.sum_le_sum_of_subset_of_nonneg hsub fun m hm _ => ?_).trans ?_ · have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast (Finset.mem_Icc.mp hm).1 exact div_nonneg (Real.log_natCast_nonneg m) (by nlinarith) · refine (htail (n - 1)).trans ?_ have : 0 ≤ (Real.log ((n - 1 + 1 : ℕ) : ℝ) + 2) / ((n - 1 + 1 : ℕ) : ℝ) := div_nonneg (by linarith [Real.log_natCast_nonneg (n - 1 + 1)]) (by positivity) linarith have h4 := mul_le_mul_of_nonneg_left h3 hn0.le linarith [hstir n]
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 164–196 at 061cea5f5749 ↗
  hM.hlo.h1 have Real.log (↑n.factorial : ℝ) ≤ ∑ p ∈ n.primesLE, (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ)
  Leaves (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * (2 : ℝ), with h1 : Real.log (↑n.factorial : ℝ) ≤ ∑ p ∈ n.primesLE, (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ).
  Uses library Real.log, Nat.primesLE, Finset.sum_le_sum, mul_le_mul_of_nonneg_right.
  Lean, lines 166–170
  have h1 : Real.log (n.factorial : ℝ) ≤ ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ) := by rw [hfac] exact Finset.sum_le_sum fun p hp => mul_le_mul_of_nonneg_right (hleg p hp).2 (hlogp p hp)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 166–170 at 061cea5f5749 ↗
  hM.hlo.h2 have ∑ p ∈ n.primesLE, (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ)))
  Leaves (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * (2 : ℝ), with h2 : ∑ p ∈ n.primesLE, (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ))).
  Uses library Nat.primesLE, Real.log, Finset.mul_sum, Finset.sum_add_distrib, Finset.sum_congr, rfl.
  Lean, lines 171–180
  have h2 : ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ) = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) + (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) := by rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib] refine Finset.sum_congr rfl fun p hp => ?_ have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast (Nat.mem_primesLE.mp hp).2.two_le have : (p : ℝ) - 1 ≠ 0 := by linarith have : (p : ℝ) ≠ 0 := by linarith field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 171–180 at 061cea5f5749 ↗
  hM.hlo.h2.hp2 have (2 : ℝ) ≤ (↑p : ℝ)
  Leaves (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * (Real.log (↑p : ℝ) / (↑p : ℝ)) + (↑n : ℝ) * (Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ)))), with hp2 : (2 : ℝ) ≤ (↑p : ℝ).
  Uses library Nat.mem_primesLE.
  Lean, line 176
  have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast (Nat.mem_primesLE.mp hp).2.two_le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 176 at 061cea5f5749 ↗
  hM.hlo.h2.s2 have (↑p : ℝ) - (1 : ℝ) ≠ (0 : ℝ) routine: linarith
  Leaves (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * (Real.log (↑p : ℝ) / (↑p : ℝ)) + (↑n : ℝ) * (Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ)))), with this : (↑p : ℝ) - (1 : ℝ) ≠ (0 : ℝ).
  Lean, line 177
  have : (p : ℝ) - 1 ≠ 0 := by linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 177 at 061cea5f5749 ↗
  hM.hlo.h2.s3 have (↑p : ℝ) ≠ (0 : ℝ) routine: linarith
  Leaves (↑n : ℝ) / ((↑p : ℝ) - (1 : ℝ)) * Real.log (↑p : ℝ) = (↑n : ℝ) * (Real.log (↑p : ℝ) / (↑p : ℝ)) + (↑n : ℝ) * (Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ)))), with this : (↑p : ℝ) ≠ (0 : ℝ).
  Lean, line 178
  have : (p : ℝ) ≠ 0 := by linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 178 at 061cea5f5749 ↗
  hM.hlo.h3 have ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ))) ≤ (2 : ℝ)
  Leaves (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * (2 : ℝ), with h3 : ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ))) ≤ (2 : ℝ).
  Uses library Nat.primesLE, Real.log, Finset.sum_le_sum_of_subset_of_nonneg.
  Lean, lines 181–194
  have h3 : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) ≤ 2 := by have hsub : Nat.primesLE n ⊆ Finset.Icc 2 (n - 1 + 1) := by intro p hp have := Nat.mem_primesLE.mp hp have := this.2.two_le rw [Finset.mem_Icc] omega refine (Finset.sum_le_sum_of_subset_of_nonneg hsub fun m hm _ => ?_).trans ?_ · have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast (Finset.mem_Icc.mp hm).1 exact div_nonneg (Real.log_natCast_nonneg m) (by nlinarith) · refine (htail (n - 1)).trans ?_ have : 0 ≤ (Real.log ((n - 1 + 1 : ℕ) : ℝ) + 2) / ((n - 1 + 1 : ℕ) : ℝ) := div_nonneg (by linarith [Real.log_natCast_nonneg (n - 1 + 1)]) (by positivity) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 181–194 at 061cea5f5749 ↗
  hM.hlo.h3.hsub have n.primesLE ⊆ Finset.Icc (2 : ℕ) (n - (1 : ℕ) + (1 : ℕ))
  Leaves ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ))) ≤ (2 : ℝ), with hsub : n.primesLE ⊆ Finset.Icc (2 : ℕ) (n - (1 : ℕ) + (1 : ℕ)).
  Uses library Nat.primesLE, Finset.Icc, Finset.mem_Icc.
  Lean, lines 182–187
  have hsub : Nat.primesLE n ⊆ Finset.Icc 2 (n - 1 + 1) := by intro p hp have := Nat.mem_primesLE.mp hp have := this.2.two_le rw [Finset.mem_Icc] omega
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 182–187 at 061cea5f5749 ↗
  hM.hlo.h3.hsub.s1 have p ≤ n ∧ Nat.Prime p
  Leaves p ∈ Finset.Icc (2 : ℕ) (n - (1 : ℕ) + (1 : ℕ)), with this : p ≤ n ∧ Nat.Prime p.
  Uses library Nat.mem_primesLE.
  Lean, line 184
  have := Nat.mem_primesLE.mp hp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 184 at 061cea5f5749 ↗
  hM.hlo.h3.hsub.s2 have (2 : ℕ) ≤ p
  Leaves p ∈ Finset.Icc (2 : ℕ) (n - (1 : ℕ) + (1 : ℕ)), with this : (2 : ℕ) ≤ p.
  Lean, line 185
  have := this.2.two_le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 185 at 061cea5f5749 ↗
  hM.hlo.h3.s2 case
  Leaves (0 : ℝ) ≤ Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))).
  Uses library div_nonneg, Real.log_natCast_nonneg.
  Lean, lines 189–190
  · have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast (Finset.mem_Icc.mp hm).1 exact div_nonneg (Real.log_natCast_nonneg m) (by nlinarith)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 189–190 at 061cea5f5749 ↗
  hM.hlo.h3.s2.hm2 have (2 : ℝ) ≤ (↑m : ℝ)
  Leaves (0 : ℝ) ≤ Real.log (↑m : ℝ) / ((↑m : ℝ) * ((↑m : ℝ) - (1 : ℝ))), with hm2 : (2 : ℝ) ≤ (↑m : ℝ).
  Uses library Finset.mem_Icc.
  Lean, line 189
  · have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast (Finset.mem_Icc.mp hm).1
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 189 at 061cea5f5749 ↗
  hM.hlo.h3.s3 case
  Leaves ∑ i ∈ Finset.Icc (2 : ℕ) (n - (1 : ℕ) + (1 : ℕ)), Real.log (↑i : ℝ) / ((↑i : ℝ) * ((↑i : ℝ) - (1 : ℝ))) ≤ (2 : ℝ).
  Lean, lines 191–194
  · refine (htail (n - 1)).trans ?_ have : 0 ≤ (Real.log ((n - 1 + 1 : ℕ) : ℝ) + 2) / ((n - 1 + 1 : ℕ) : ℝ) := div_nonneg (by linarith [Real.log_natCast_nonneg (n - 1 + 1)]) (by positivity) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 191–194 at 061cea5f5749 ↗
  hM.hlo.h3.s3.this have (0 : ℝ) ≤ (Real.log (↑(n - (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(n - (1 : ℕ) + (1 : ℕ)) : ℝ)
  Leaves (2 : ℝ) - (Real.log (↑(n - (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(n - (1 : ℕ) + (1 : ℕ)) : ℝ) ≤ (2 : ℝ), with this : (0 : ℝ) ≤ (Real.log (↑(n - (1 : ℕ) + (1 : ℕ)) : ℝ) + (2 : ℝ)) / (↑(n - (1 : ℕ) + (1 : ℕ)) : ℝ).
  Uses library Real.log, div_nonneg, Real.log_natCast_nonneg.
  Lean, lines 192–193
  have : 0 ≤ (Real.log ((n - 1 + 1 : ℕ) : ℝ) + 2) / ((n - 1 + 1 : ℕ) : ℝ) := div_nonneg (by linarith [Real.log_natCast_nonneg (n - 1 + 1)]) (by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 192–193 at 061cea5f5749 ↗
  hM.hlo.h4 have (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ))) ≤ (↑n : ℝ) * (2 : ℝ)
  Leaves (↑n : ℝ) * Real.log (↑n : ℝ) - (↑n : ℝ) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) + (↑n : ℝ) * (2 : ℝ), with h4 : (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / ((↑p : ℝ) * ((↑p : ℝ) - (1 : ℝ))) ≤ (↑n : ℝ) * (2 : ℝ).
  Uses library mul_le_mul_of_nonneg_left.
  Lean, line 195
  have h4 := mul_le_mul_of_nonneg_left h3 hn0.le
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 195 at 061cea5f5749 ↗
13. hM.s13 case
  Leaves (-3 : ℝ) ≤ ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ).
  Uses library le_of_mul_le_mul_left.
  Lean, lines 199–201
  · have : (n : ℝ) * (Real.log n - 3) ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) := by linarith linarith [le_of_mul_le_mul_left this hn0]
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 199–201 at 061cea5f5749 ↗
  hM.s13.this have (↑n : ℝ) * (Real.log (↑n : ℝ) - (3 : ℝ)) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) routine: linarith
  Leaves (-3 : ℝ) ≤ ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ), with this : (↑n : ℝ) * (Real.log (↑n : ℝ) - (3 : ℝ)) ≤ (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ).
  Uses library Real.log, Nat.primesLE.
  Lean, lines 199–200
  · have : (n : ℝ) * (Real.log n - 3) ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) := by linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 199–200 at 061cea5f5749 ↗
14. hM.s14 case
  Leaves ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ) ≤ (3 : ℝ).
  Uses library le_of_mul_le_mul_left.
  Lean, lines 202–204
  · have : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) ≤ (n : ℝ) * (Real.log n + 3) := by nlinarith linarith [le_of_mul_le_mul_left this hn0]
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 202–204 at 061cea5f5749 ↗
  hM.s14.this have (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * (Real.log (↑n : ℝ) + (3 : ℝ)) routine: nlinarith
  Leaves ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ) ≤ (3 : ℝ), with this : (↑n : ℝ) * ∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) ≤ (↑n : ℝ) * (Real.log (↑n : ℝ) + (3 : ℝ)).
  Uses library Nat.primesLE, Real.log.
  Lean, lines 202–203
  · have : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) ≤ (n : ℝ) * (Real.log n + 3) := by nlinarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 202–203 at 061cea5f5749 ↗
s2 obtain ∃ (C : ℝ), ∀ (n : ℕ), |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ C
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with C : ℝ, hC : ∀ (n : ℕ), |∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑n : ℝ)| ≤ C.
Lean, line 206
```
  obtain ⟨C, hC⟩ := hM
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 206 at 061cea5f5749 ↗
hC0 have (0 : ℝ) ≤ C
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with hC0 : (0 : ℝ) ≤ C.
Uses library abs_nonneg.
Lean, line 207
```
  have hC0 : 0 ≤ C := (abs_nonneg _).trans (hC 0)
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 207 at 061cea5f5749 ↗
hl2 have (0 : ℝ) < Real.log (2 : ℝ)
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with hl2 : (0 : ℝ) < Real.log (2 : ℝ).
Uses library Real.log, Real.log_pos.
Lean, line 208
```
  have hl2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 208 at 061cea5f5749 ↗
hL have ∀ (n : ℕ), (2 : ℕ) ≤ n → Real.log (2 : ℝ) ≤ Real.log (↑n : ℝ)
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with hL : ∀ (n : ℕ), (2 : ℕ) ≤ n → Real.log (2 : ℝ) ≤ Real.log (↑n : ℝ).
Uses library Real.log, Real.log_le_log.
Lean, lines 209–210
```
  have hL : ∀ n : ℕ, 2 ≤ n → Real.log 2 ≤ Real.log (n : ℝ) := fun n hn =>
    Real.log_le_log (by norm_num) (by exact_mod_cast hn)
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 209–210 at 061cea5f5749 ↗
htel have ∀ (f : ℕ → ℝ) (x : ℕ), (2 : ℕ) ≤ x → ∑ n ∈ Finset.Ico (2 : ℕ) x, (f (n + (1 : ℕ)) - f n) = f x - f (2 : ℕ)
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with htel : ∀ (f : ℕ → ℝ) (x : ℕ), (2 : ℕ) ≤ x → ∑ n ∈ Finset.Ico (2 : ℕ) x, (f (n + (1 : ℕ)) - f n) = f x - f (2 : ℕ).
Uses library Finset.Ico, Nat.le_induction.
Lean, lines 211–216
```
  have htel : ∀ f : ℕ → ℝ, ∀ x : ℕ, 2 ≤ x →
      ∑ n ∈ Finset.Ico 2 x, (f (n + 1) - f n) = f x - f 2 := by
    intro f x hx
    induction x, hx using Nat.le_induction with
    | base => simp
    | succ x hx ih => rw [Finset.sum_Ico_succ_top hx, ih]; ring
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 211–216 at 061cea5f5749 ↗
1. htel.s1 case routine: simp
  Leaves ∑ n ∈ Finset.Ico (2 : ℕ) (2 : ℕ), (f (n + (1 : ℕ)) - f n) = f (2 : ℕ) - f (2 : ℕ).
  Lean, line 215
  | base => simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 215 at 061cea5f5749 ↗
2. htel.s2 case
  Leaves ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (f (n + (1 : ℕ)) - f n) = f (x + (1 : ℕ)) - f (2 : ℕ), with x : ℕ, hx : (2 : ℕ) ≤ x, ih : ∑ n ∈ Finset.Ico (2 : ℕ) x, (f (n + (1 : ℕ)) - f n) = f x - f (2 : ℕ).
  Uses library Nat.succ, Finset.sum_Ico_succ_top.
  Lean, line 216
  | succ x hx ih => rw [Finset.sum_Ico_succ_top hx, ih]; ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 216 at 061cea5f5749 ↗
htel' have ∀ (f : ℕ → ℝ) (x : ℕ), (2 : ℕ) ≤ x → ∑ n ∈ Finset.Ico (2 : ℕ) x, (f n - f (n + (1 : ℕ))) = f (2 : ℕ) - f x
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with htel' : ∀ (f : ℕ → ℝ) (x : ℕ), (2 : ℕ) ≤ x → ∑ n ∈ Finset.Ico (2 : ℕ) x, (f n - f (n + (1 : ℕ))) = f (2 : ℕ) - f x.
Uses library Finset.Ico, Nat.le_induction.
Lean, lines 217–222
```
  have htel' : ∀ f : ℕ → ℝ, ∀ x : ℕ, 2 ≤ x →
      ∑ n ∈ Finset.Ico 2 x, (f n - f (n + 1)) = f 2 - f x := by
    intro f x hx
    induction x, hx using Nat.le_induction with
    | base => simp
    | succ x hx ih => rw [Finset.sum_Ico_succ_top hx, ih]; ring
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 217–222 at 061cea5f5749 ↗
1. htel'.s1 case routine: simp
  Leaves ∑ n ∈ Finset.Ico (2 : ℕ) (2 : ℕ), (f n - f (n + (1 : ℕ))) = f (2 : ℕ) - f (2 : ℕ).
  Lean, line 221
  | base => simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 221 at 061cea5f5749 ↗
2. htel'.s2 case
  Leaves ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (f n - f (n + (1 : ℕ))) = f (2 : ℕ) - f (x + (1 : ℕ)), with x : ℕ, hx : (2 : ℕ) ≤ x, ih : ∑ n ∈ Finset.Ico (2 : ℕ) x, (f n - f (n + (1 : ℕ))) = f (2 : ℕ) - f x.
  Uses library Nat.succ, Finset.sum_Ico_succ_top.
  Lean, line 222
  | succ x hx ih => rw [Finset.sum_Ico_succ_top hx, ih]; ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 222 at 061cea5f5749 ↗
habel have ∀ (x : ℕ), (2 : ℕ) ≤ x → ∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ))
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with habel : ∀ (x : ℕ), (2 : ℕ) ≤ x → ∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)).
Uses library Nat.primesLE, Real.log, Finset.Ico, Nat.le_induction.
Lean, lines 223–250
```
  have habel : ∀ x : ℕ, 2 ≤ x →
      ∑ p ∈ Nat.primesLE x, (1 : ℝ) / p
        = (∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ)) / Real.log (x : ℝ)
          + ∑ n ∈ Finset.Ico 2 x, (∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ))
              * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ)) := by
    intro x hx
    induction x, hx using Nat.le_induction with
    | base =>
      have h2 : Nat.primesLE 2 = {2} := by decide
      have : Real.log 2 ≠ 0 := hl2.ne'
      simp [h2]
      field_simp
    | succ x hx ih =>
      have ha : Real.log (x : ℝ) ≠ 0 := (lt_of_lt_of_le hl2 (hL x hx)).ne'
      have hb : Real.log ((x + 1 : ℕ) : ℝ) ≠ 0 :=
        (lt_of_lt_of_le hl2 (hL (x + 1) (by omega))).ne'
      have hnot : x + 1 ∉ Nat.primesLE x := fun h => by
        have := (Nat.mem_primesLE.mp h).1
        omega
      have hx1 : ((x + 1 : ℕ) : ℝ) ≠ 0 := by positivity
      rw [Finset.sum_Ico_succ_top hx, Nat.primesLE_succ]
      split_ifs with hp
      · rw [Finset.sum_insert hnot, Finset.sum_insert hnot, ih]
        field_simp
        ring
      · rw [ih]
        field_simp
        ring
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 223–250 at 061cea5f5749 ↗
1. habel.s1 case
  Leaves ∑ p ∈ Nat.primesLE (2 : ℕ), (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ Nat.primesLE (2 : ℕ), Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(2 : ℕ) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (2 : ℕ), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)).
  Lean, lines 230–234
  | base => have h2 : Nat.primesLE 2 = {2} := by decide have : Real.log 2 ≠ 0 := hl2.ne' simp [h2] field_simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 230–234 at 061cea5f5749 ↗
  habel.s1.h2 have Nat.primesLE (2 : ℕ) = {(2 : ℕ)} routine: decide
  Leaves ∑ p ∈ Nat.primesLE (2 : ℕ), (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ Nat.primesLE (2 : ℕ), Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(2 : ℕ) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (2 : ℕ), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with h2 : Nat.primesLE (2 : ℕ) = {(2 : ℕ)}.
  Uses library Nat.primesLE.
  Lean, line 231
  have h2 : Nat.primesLE 2 = {2} := by decide
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 231 at 061cea5f5749 ↗
  habel.s1.this have Real.log (2 : ℝ) ≠ (0 : ℝ)
  Leaves ∑ p ∈ Nat.primesLE (2 : ℕ), (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ Nat.primesLE (2 : ℕ), Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(2 : ℕ) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (2 : ℕ), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with this : Real.log (2 : ℝ) ≠ (0 : ℝ).
  Uses library Real.log.
  Lean, line 232
  have : Real.log 2 ≠ 0 := hl2.ne'
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 232 at 061cea5f5749 ↗
2. habel.s2 case
  Leaves ∑ p ∈ (x + (1 : ℕ)).primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ (x + (1 : ℕ)).primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with x : ℕ, hx : (2 : ℕ) ≤ x, ih : ∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)).
  Uses library Nat.succ, Finset.sum_Ico_succ_top, Nat.primesLE_succ.
  Lean, lines 235–250
  | succ x hx ih => have ha : Real.log (x : ℝ) ≠ 0 := (lt_of_lt_of_le hl2 (hL x hx)).ne' have hb : Real.log ((x + 1 : ℕ) : ℝ) ≠ 0 := (lt_of_lt_of_le hl2 (hL (x + 1) (by omega))).ne' have hnot : x + 1 ∉ Nat.primesLE x := fun h => by have := (Nat.mem_primesLE.mp h).1 omega have hx1 : ((x + 1 : ℕ) : ℝ) ≠ 0 := by positivity rw [Finset.sum_Ico_succ_top hx, Nat.primesLE_succ] split_ifs with hp · rw [Finset.sum_insert hnot, Finset.sum_insert hnot, ih] field_simp ring · rw [ih] field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 235–250 at 061cea5f5749 ↗
  habel.s2.ha have Real.log (↑x : ℝ) ≠ (0 : ℝ)
  Leaves ∑ p ∈ (x + (1 : ℕ)).primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ (x + (1 : ℕ)).primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with ha : Real.log (↑x : ℝ) ≠ (0 : ℝ).
  Uses library Real.log, lt_of_lt_of_le.
  Lean, line 236
  have ha : Real.log (x : ℝ) ≠ 0 := (lt_of_lt_of_le hl2 (hL x hx)).ne'
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 236 at 061cea5f5749 ↗
  habel.s2.hb have Real.log (↑(x + (1 : ℕ)) : ℝ) ≠ (0 : ℝ)
  Leaves ∑ p ∈ (x + (1 : ℕ)).primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ (x + (1 : ℕ)).primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hb : Real.log (↑(x + (1 : ℕ)) : ℝ) ≠ (0 : ℝ).
  Uses library Real.log, lt_of_lt_of_le.
  Lean, lines 237–238
  have hb : Real.log ((x + 1 : ℕ) : ℝ) ≠ 0 := (lt_of_lt_of_le hl2 (hL (x + 1) (by omega))).ne'
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 237–238 at 061cea5f5749 ↗
  habel.s2.hnot have x + (1 : ℕ) ∉ x.primesLE
  Leaves ∑ p ∈ (x + (1 : ℕ)).primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ (x + (1 : ℕ)).primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hnot : x + (1 : ℕ) ∉ x.primesLE.
  Uses library Nat.primesLE.
  Lean, lines 239–241
  have hnot : x + 1 ∉ Nat.primesLE x := fun h => by have := (Nat.mem_primesLE.mp h).1 omega
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 239–241 at 061cea5f5749 ↗
  habel.s2.hnot.this have x + (1 : ℕ) ≤ x
  Leaves False, with this : x + (1 : ℕ) ≤ x.
  Uses library Nat.mem_primesLE.
  Lean, line 240
  have := (Nat.mem_primesLE.mp h).1
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 240 at 061cea5f5749 ↗
  habel.s2.hx1 have (↑(x + (1 : ℕ)) : ℝ) ≠ (0 : ℝ) routine: positivity
  Leaves ∑ p ∈ (x + (1 : ℕ)).primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ (x + (1 : ℕ)).primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) (x + (1 : ℕ)), (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hx1 : (↑(x + (1 : ℕ)) : ℝ) ≠ (0 : ℝ).
  Lean, line 242
  have hx1 : ((x + 1 : ℕ) : ℝ) ≠ 0 := by positivity
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 242 at 061cea5f5749 ↗
  habel.s2.s5 case
  Leaves ∑ x ∈ insert (x + (1 : ℕ)) x.primesLE, (1 : ℝ) / (↑x : ℝ) = (∑ x ∈ insert (x + (1 : ℕ)) x.primesLE, Real.log (↑x : ℝ) / (↑x : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + (∑ k ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ k.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑k : ℝ) - (1 : ℝ) / Real.log (↑(k + (1 : ℕ)) : ℝ)) + (∑ x ∈ x.primesLE, Real.log (↑x : ℝ) / (↑x : ℝ)) * ((1 : ℝ) / Real.log (↑x : ℝ) - (1 : ℝ) / Real.log (↑(x + (1 : ℕ)) : ℝ))).
  Uses library Finset.sum_insert.
  Lean, lines 245–247
  · rw [Finset.sum_insert hnot, Finset.sum_insert hnot, ih] field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 245–247 at 061cea5f5749 ↗
  habel.s2.s6 case
  Leaves ∑ x ∈ x.primesLE, (1 : ℝ) / (↑x : ℝ) = (∑ x ∈ x.primesLE, Real.log (↑x : ℝ) / (↑x : ℝ)) / Real.log (↑(x + (1 : ℕ)) : ℝ) + (∑ k ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ k.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑k : ℝ) - (1 : ℝ) / Real.log (↑(k + (1 : ℕ)) : ℝ)) + (∑ x ∈ x.primesLE, Real.log (↑x : ℝ) / (↑x : ℝ)) * ((1 : ℝ) / Real.log (↑x : ℝ) - (1 : ℝ) / Real.log (↑(x + (1 : ℕ)) : ℝ))).
  Lean, lines 248–250
  · rw [ih] field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 248–250 at 061cea5f5749 ↗
hreal have ∀ (a b A : ℝ), (0 : ℝ) < a → a ≤ b → b - a ≤ (1 : ℝ) → |A - a| ≤ C → (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b)
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with hreal : ∀ (a b A : ℝ), (0 : ℝ) < a → a ≤ b → b - a ≤ (1 : ℝ) → |A - a| ≤ C → (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b).
Uses library Real.log, And.intro, abs_le.
Lean, lines 251–280
```
  have hreal : ∀ a b A : ℝ, 0 < a → a ≤ b → b - a ≤ 1 → |A - a| ≤ C →
      0 ≤ 1 / a - 1 / b ∧
        |A * (1 / a - 1 / b) - (Real.log b - Real.log a)| ≤ (C + 1) * (1 / a - 1 / b) := by
    intro a b A ha0 hab hba hA
    have hb0 : 0 < b := ha0.trans_le hab
    have hd0 : 0 ≤ 1 / a - 1 / b := by
      rw [sub_nonneg]
      exact one_div_le_one_div_of_le ha0 hab
    have hv : Real.log b - Real.log a = Real.log (b / a) :=
      (Real.log_div hb0.ne' ha0.ne').symm
    have hlow := Real.one_sub_inv_le_log_of_pos (show 0 < b / a by positivity)
    have hup := Real.log_le_sub_one_of_pos (show 0 < b / a by positivity)
    have hR := abs_le.mp hA
    have hu : a * (1 / a - 1 / b) = 1 - (b / a)⁻¹ := by
      field_simp
    have hw : b / a - 1 - (1 - (b / a)⁻¹) = (b - a) * (1 / a - 1 / b) := by
      field_simp
    have hw2 : (b - a) * (1 / a - 1 / b) ≤ 1 * (1 / a - 1 / b) :=
      mul_le_mul_of_nonneg_right hba hd0
    have h1 : -C * (1 / a - 1 / b) ≤ (A - a) * (1 / a - 1 / b) :=
      mul_le_mul_of_nonneg_right hR.1 hd0
    have h2 : (A - a) * (1 / a - 1 / b) ≤ C * (1 / a - 1 / b) :=
      mul_le_mul_of_nonneg_right hR.2 hd0
    have e : A * (1 / a - 1 / b) - (Real.log b - Real.log a)
        = (A - a) * (1 / a - 1 / b) + (a * (1 / a - 1 / b) - Real.log (b / a)) := by
      rw [hv]
      ring
    refine ⟨hd0, ?_⟩
    rw [e, abs_le]
    constructor <;> nlinarith
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 251–280 at 061cea5f5749 ↗
1. hreal.hb0 have (0 : ℝ) < b
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hb0 : (0 : ℝ) < b.
  Lean, line 255
  have hb0 : 0 < b := ha0.trans_le hab
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 255 at 061cea5f5749 ↗
2. hreal.hd0 have (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hd0 : (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b.
  Uses library sub_nonneg, one_div_le_one_div_of_le.
  Lean, lines 256–258
  have hd0 : 0 ≤ 1 / a - 1 / b := by rw [sub_nonneg] exact one_div_le_one_div_of_le ha0 hab
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 256–258 at 061cea5f5749 ↗
3. hreal.hv have Real.log b - Real.log a = Real.log (b / a)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hv : Real.log b - Real.log a = Real.log (b / a).
  Uses library Real.log, Real.log_div.
  Lean, lines 259–260
  have hv : Real.log b - Real.log a = Real.log (b / a) := (Real.log_div hb0.ne' ha0.ne').symm
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 259–260 at 061cea5f5749 ↗
4. hreal.hlow have (1 : ℝ) - (b / a)⁻¹ ≤ Real.log (b / a)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hlow : (1 : ℝ) - (b / a)⁻¹ ≤ Real.log (b / a).
  Uses library Real.one_sub_inv_le_log_of_pos.
  Lean, line 261
  have hlow := Real.one_sub_inv_le_log_of_pos (show 0 < b / a by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 261 at 061cea5f5749 ↗
5. hreal.hup have Real.log (b / a) ≤ b / a - (1 : ℝ)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hup : Real.log (b / a) ≤ b / a - (1 : ℝ).
  Uses library Real.log_le_sub_one_of_pos.
  Lean, line 262
  have hup := Real.log_le_sub_one_of_pos (show 0 < b / a by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 262 at 061cea5f5749 ↗
6. hreal.hR have -C ≤ A - a ∧ A - a ≤ C
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hR : -C ≤ A - a ∧ A - a ≤ C.
  Uses library abs_le.
  Lean, line 263
  have hR := abs_le.mp hA
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 263 at 061cea5f5749 ↗
7. hreal.hu have a * ((1 : ℝ) / a - (1 : ℝ) / b) = (1 : ℝ) - (b / a)⁻¹ routine: field_simp
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hu : a * ((1 : ℝ) / a - (1 : ℝ) / b) = (1 : ℝ) - (b / a)⁻¹.
  Lean, lines 264–265
  have hu : a * (1 / a - 1 / b) = 1 - (b / a)⁻¹ := by field_simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 264–265 at 061cea5f5749 ↗
8. hreal.hw have b / a - (1 : ℝ) - ((1 : ℝ) - (b / a)⁻¹) = (b - a) * ((1 : ℝ) / a - (1 : ℝ) / b) routine: field_simp
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hw : b / a - (1 : ℝ) - ((1 : ℝ) - (b / a)⁻¹) = (b - a) * ((1 : ℝ) / a - (1 : ℝ) / b).
  Lean, lines 266–267
  have hw : b / a - 1 - (1 - (b / a)⁻¹) = (b - a) * (1 / a - 1 / b) := by field_simp
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 266–267 at 061cea5f5749 ↗
9. hreal.hw2 have (b - a) * ((1 : ℝ) / a - (1 : ℝ) / b) ≤ (1 : ℝ) * ((1 : ℝ) / a - (1 : ℝ) / b)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with hw2 : (b - a) * ((1 : ℝ) / a - (1 : ℝ) / b) ≤ (1 : ℝ) * ((1 : ℝ) / a - (1 : ℝ) / b).
  Uses library mul_le_mul_of_nonneg_right.
  Lean, lines 268–269
  have hw2 : (b - a) * (1 / a - 1 / b) ≤ 1 * (1 / a - 1 / b) := mul_le_mul_of_nonneg_right hba hd0
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 268–269 at 061cea5f5749 ↗
10. hreal.h1 have -C * ((1 : ℝ) / a - (1 : ℝ) / b) ≤ (A - a) * ((1 : ℝ) / a - (1 : ℝ) / b)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with h1 : -C * ((1 : ℝ) / a - (1 : ℝ) / b) ≤ (A - a) * ((1 : ℝ) / a - (1 : ℝ) / b).
  Uses library mul_le_mul_of_nonneg_right.
  Lean, lines 270–271
  have h1 : -C * (1 / a - 1 / b) ≤ (A - a) * (1 / a - 1 / b) := mul_le_mul_of_nonneg_right hR.1 hd0
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 270–271 at 061cea5f5749 ↗
11. hreal.h2 have (A - a) * ((1 : ℝ) / a - (1 : ℝ) / b) ≤ C * ((1 : ℝ) / a - (1 : ℝ) / b)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with h2 : (A - a) * ((1 : ℝ) / a - (1 : ℝ) / b) ≤ C * ((1 : ℝ) / a - (1 : ℝ) / b).
  Uses library mul_le_mul_of_nonneg_right.
  Lean, lines 272–273
  have h2 : (A - a) * (1 / a - 1 / b) ≤ C * (1 / a - 1 / b) := mul_le_mul_of_nonneg_right hR.2 hd0
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 272–273 at 061cea5f5749 ↗
12. hreal.e have A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a) = (A - a) * ((1 : ℝ) / a - (1 : ℝ) / b) + (a * ((1 : ℝ) / a - (1 : ℝ) / b) - Real.log (b / a))
  Leaves (0 : ℝ) ≤ (1 : ℝ) / a - (1 : ℝ) / b ∧ |A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a)| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / a - (1 : ℝ) / b), with e : A * ((1 : ℝ) / a - (1 : ℝ) / b) - (Real.log b - Real.log a) = (A - a) * ((1 : ℝ) / a - (1 : ℝ) / b) + (a * ((1 : ℝ) / a - (1 : ℝ) / b) - Real.log (b / a)).
  Uses library Real.log.
  Lean, lines 274–277
  have e : A * (1 / a - 1 / b) - (Real.log b - Real.log a) = (A - a) * (1 / a - 1 / b) + (a * (1 / a - 1 / b) - Real.log (b / a)) := by rw [hv] ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 274–277 at 061cea5f5749 ↗
hpt have ∀ (n : ℕ), (2 : ℕ) ≤ n → |(∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ)))| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ))
Leaves ∃ (C : ℝ), (0 : ℝ) ≤ C ∧ ∀ (x : ℕ), (2 : ℕ) ≤ x → |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ C, with hpt : ∀ (n : ℕ), (2 : ℕ) ≤ n → |(∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ)))| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)).
Uses library Nat.primesLE, Real.log, lt_of_lt_of_le.
Lean, lines 281–303
```
  have hpt : ∀ n : ℕ, 2 ≤ n →
      |(∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ))
            * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ))
          - (Real.log (Real.log ((n + 1 : ℕ) : ℝ)) - Real.log (Real.log (n : ℝ)))|
        ≤ (C + 1) * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ)) := by
    intro n hn
    have hn0 : (0 : ℝ) < n := by exact_mod_cast (by omega : 0 < n)
    have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
    have hab : Real.log (n : ℝ) ≤ Real.log ((n + 1 : ℕ) : ℝ) :=
      Real.log_le_log hn0 (by push_cast; linarith)
    have hba : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) ≤ 1 := by
      have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)
          = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm
      have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity)
      have h3 : ((n + 1 : ℕ) : ℝ) / n - 1 = 1 / n := by
        push_cast
        field_simp
        ring
      have h4 : (1 : ℝ) / n ≤ 1 := by
        rw [div_le_one hn0]
        exact_mod_cast (by omega : 1 ≤ n)
      linarith
    exact (hreal _ _ _ (lt_of_lt_of_le hl2 (hL n hn)) hab hba (hC n)).2
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 281–303 at 061cea5f5749 ↗
1. hpt.hn0 have (0 : ℝ) < (↑n : ℝ)
  Leaves |(∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ)))| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hn0 : (0 : ℝ) < (↑n : ℝ).
  Lean, line 287
  have hn0 : (0 : ℝ) < n := by exact_mod_cast (by omega : 0 < n)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 287 at 061cea5f5749 ↗
2. hpt.hn1 have (0 : ℝ) < (↑(n + (1 : ℕ)) : ℝ) routine: positivity
  Leaves |(∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ)))| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hn1 : (0 : ℝ) < (↑(n + (1 : ℕ)) : ℝ).
  Lean, line 288
  have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 288 at 061cea5f5749 ↗
3. hpt.hab have Real.log (↑n : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ)
  Leaves |(∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ)))| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hab : Real.log (↑n : ℝ) ≤ Real.log (↑(n + (1 : ℕ)) : ℝ).
  Uses library Real.log, Real.log_le_log.
  Lean, lines 289–290
  have hab : Real.log (n : ℝ) ≤ Real.log ((n + 1 : ℕ) : ℝ) := Real.log_le_log hn0 (by push_cast; linarith)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 289–290 at 061cea5f5749 ↗
4. hpt.hba have Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) ≤ (1 : ℝ)
  Leaves |(∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ)))| ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)), with hba : Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) ≤ (1 : ℝ).
  Uses library Real.log.
  Lean, lines 291–302
  have hba : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) ≤ 1 := by have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity) have h3 : ((n + 1 : ℕ) : ℝ) / n - 1 = 1 / n := by push_cast field_simp ring have h4 : (1 : ℝ) / n ≤ 1 := by rw [div_le_one hn0] exact_mod_cast (by omega : 1 ≤ n) linarith
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 291–302 at 061cea5f5749 ↗
  hpt.hba.h1 have Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) = Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ))
  Leaves Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) ≤ (1 : ℝ), with h1 : Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) = Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ)).
  Uses library Real.log, Real.log_div.
  Lean, lines 292–293
  have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 292–293 at 061cea5f5749 ↗
  hpt.hba.h2 have Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ)) ≤ (↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ)
  Leaves Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) ≤ (1 : ℝ), with h2 : Real.log ((↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ)) ≤ (↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ).
  Uses library Real.log_le_sub_one_of_pos.
  Lean, line 294
  have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 294 at 061cea5f5749 ↗
  hpt.hba.h3 have (↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ) = (1 : ℝ) / (↑n : ℝ)
  Leaves Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) ≤ (1 : ℝ), with h3 : (↑(n + (1 : ℕ)) : ℝ) / (↑n : ℝ) - (1 : ℝ) = (1 : ℝ) / (↑n : ℝ).
  Lean, lines 295–298
  have h3 : ((n + 1 : ℕ) : ℝ) / n - 1 = 1 / n := by push_cast field_simp ring
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 295–298 at 061cea5f5749 ↗
  hpt.hba.h4 have (1 : ℝ) / (↑n : ℝ) ≤ (1 : ℝ)
  Leaves Real.log (↑(n + (1 : ℕ)) : ℝ) - Real.log (↑n : ℝ) ≤ (1 : ℝ), with h4 : (1 : ℝ) / (↑n : ℝ) ≤ (1 : ℝ).
  Uses library div_le_one.
  Lean, lines 299–301
  have h4 : (1 : ℝ) / n ≤ 1 := by rw [div_le_one hn0] exact_mod_cast (by omega : 1 ≤ n)
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 299–301 at 061cea5f5749 ↗
hLx have Real.log (2 : ℝ) ≤ Real.log (↑x : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hLx : Real.log (2 : ℝ) ≤ Real.log (↑x : ℝ).
Uses library Real.log.
Lean, line 306
```
  have hLx : Real.log 2 ≤ Real.log (x : ℝ) := hL x hx
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 306 at 061cea5f5749 ↗
hLx0 have (0 : ℝ) < Real.log (↑x : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hLx0 : (0 : ℝ) < Real.log (↑x : ℝ).
Uses library Real.log.
Lean, line 307
```
  have hLx0 : 0 < Real.log (x : ℝ) := hl2.trans_le hLx
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 307 at 061cea5f5749 ↗
hv have ∑ n ∈ Finset.Ico (2 : ℕ) x, (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ))) = Real.log (Real.log (↑x : ℝ)) - Real.log (Real.log (↑(2 : ℕ) : ℝ))
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hv : ∑ n ∈ Finset.Ico (2 : ℕ) x, (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ))) = Real.log (Real.log (↑x : ℝ)) - Real.log (Real.log (↑(2 : ℕ) : ℝ)).
Uses library Real.log.
Lean, line 308
```
  have hv := htel (fun n => Real.log (Real.log (n : ℝ))) x hx
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 308 at 061cea5f5749 ↗
hd have ∑ n ∈ Finset.Ico (2 : ℕ) x, ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) = (1 : ℝ) / Real.log (↑(2 : ℕ) : ℝ) - (1 : ℝ) / Real.log (↑x : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hd : ∑ n ∈ Finset.Ico (2 : ℕ) x, ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) = (1 : ℝ) / Real.log (↑(2 : ℕ) : ℝ) - (1 : ℝ) / Real.log (↑x : ℝ).
Uses library Real.log.
Lean, line 309
```
  have hd := htel' (fun n => 1 / Real.log (n : ℝ)) x hx
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 309 at 061cea5f5749 ↗
hsum have |∑ n ∈ Finset.Ico (2 : ℕ) x, ((∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ))))| ≤ (C + (1 : ℝ)) / Real.log (2 : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hsum : |∑ n ∈ Finset.Ico (2 : ℕ) x, ((∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑(n + (1 : ℕ)) : ℝ)) - Real.log (Real.log (↑n : ℝ))))| ≤ (C + (1 : ℝ)) / Real.log (2 : ℝ).
Uses library Finset.Ico, Nat.primesLE, Real.log, Finset.abs_sum_le_sum_abs, Finset.sum_le_sum, Finset.mem_Ico, Finset.mul_sum, div_eq_mul_one_div.
Lean, lines 311–319
```
  have hsum : |∑ n ∈ Finset.Ico 2 x, ((∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ))
            * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ))
          - (Real.log (Real.log ((n + 1 : ℕ) : ℝ)) - Real.log (Real.log (n : ℝ))))|
        ≤ (C + 1) / Real.log 2 := by
    refine (Finset.abs_sum_le_sum_abs _ _).trans ?_
    refine (Finset.sum_le_sum (fun n hn => hpt n (Finset.mem_Ico.mp hn).1)).trans ?_
    rw [← Finset.mul_sum, hd, div_eq_mul_one_div (C + 1)]
    have : 0 ≤ 1 / Real.log (x : ℝ) := by positivity
    nlinarith
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 311–319 at 061cea5f5749 ↗
1. hsum.this have (0 : ℝ) ≤ (1 : ℝ) / Real.log (↑x : ℝ) routine: positivity
  Leaves (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (2 : ℝ) - (1 : ℝ) / Real.log (↑x : ℝ)) ≤ (C + (1 : ℝ)) * ((1 : ℝ) / Real.log (2 : ℝ)), with this : (0 : ℝ) ≤ (1 : ℝ) / Real.log (↑x : ℝ).
  Uses library Real.log.
  Lean, line 318
  have : 0 ≤ 1 / Real.log (x : ℝ) := by positivity
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 318 at 061cea5f5749 ↗
hq have |(∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ)| ≤ C / Real.log (2 : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hq : |(∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ)| ≤ C / Real.log (2 : ℝ).
Uses library Nat.primesLE, Real.log, abs_div, abs_of_pos.
Lean, lines 321–325
```
  have hq : |(∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ) - Real.log (x : ℝ)) / Real.log (x : ℝ)|
      ≤ C / Real.log 2 := by
    rw [abs_div, abs_of_pos hLx0]
    calc _ ≤ C / Real.log (x : ℝ) := by gcongr; exact hC x
      _ ≤ C / Real.log 2 := by gcongr
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 321–325 at 061cea5f5749 ↗
1. hq.s1 calc |∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)| / Real.log (↑x : ℝ) ≤ C / Real.log (↑x : ℝ)
  Closes the goal.
  Uses library Real.log.
  Lean, line 324
  calc _ ≤ C / Real.log (x : ℝ) := by gcongr; exact hC x
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 324 at 061cea5f5749 ↗
2. hq.s2 calc
  Closes the goal.
  Uses library Real.log.
  Lean, line 325
  _ ≤ C / Real.log 2 := by gcongr
  targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 325 at 061cea5f5749 ↗
e1 have (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) = (1 : ℝ) + (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with e1 : (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) = (1 : ℝ) + (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ).
Uses library Nat.primesLE, Real.log, sub_div, div_self.
Lean, lines 326–329
```
  have e1 : (∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ)) / Real.log (x : ℝ)
      = 1 + (∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ) - Real.log (x : ℝ)) / Real.log (x : ℝ) := by
    rw [sub_div, div_self hLx0.ne']
    ring
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, lines 326–329 at 061cea5f5749 ↗
hab have ∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ))
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with hab : ∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) = (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) / Real.log (↑x : ℝ) + ∑ n ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ n.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑n : ℝ) - (1 : ℝ) / Real.log (↑(n + (1 : ℕ)) : ℝ)).
Lean, line 330
```
  have hab := habel x hx
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 330 at 061cea5f5749 ↗
h3 have -((C + (1 : ℝ)) / Real.log (2 : ℝ)) ≤ ∑ x ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑x : ℝ) - (1 : ℝ) / Real.log (↑(x + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑x : ℝ)) - Real.log (Real.log (2 : ℝ))) ∧ ∑ x ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑x : ℝ) - (1 : ℝ) / Real.log (↑(x + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑x : ℝ)) - Real.log (Real.log (2 : ℝ))) ≤ (C + (1 : ℝ)) / Real.log (2 : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with h3 : -((C + (1 : ℝ)) / Real.log (2 : ℝ)) ≤ ∑ x ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑x : ℝ) - (1 : ℝ) / Real.log (↑(x + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑x : ℝ)) - Real.log (Real.log (2 : ℝ))) ∧ ∑ x ∈ Finset.Ico (2 : ℕ) x, (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ)) * ((1 : ℝ) / Real.log (↑x : ℝ) - (1 : ℝ) / Real.log (↑(x + (1 : ℕ)) : ℝ)) - (Real.log (Real.log (↑x : ℝ)) - Real.log (Real.log (2 : ℝ))) ≤ (C + (1 : ℝ)) / Real.log (2 : ℝ).
Uses library abs_le.
Lean, line 331
```
  have h3 := abs_le.mp hsum
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 331 at 061cea5f5749 ↗
h4 have -(C / Real.log (2 : ℝ)) ≤ (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ) ∧ (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ) ≤ C / Real.log (2 : ℝ)
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with h4 : -(C / Real.log (2 : ℝ)) ≤ (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ) ∧ (∑ p ∈ x.primesLE, Real.log (↑p : ℝ) / (↑p : ℝ) - Real.log (↑x : ℝ)) / Real.log (↑x : ℝ) ≤ C / Real.log (2 : ℝ).
Uses library abs_le.
Lean, line 332
```
  have h4 := abs_le.mp hq
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 332 at 061cea5f5749 ↗
h5 have -|Real.log (Real.log (2 : ℝ))| ≤ Real.log (Real.log (2 : ℝ))
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with h5 : -|Real.log (Real.log (2 : ℝ))| ≤ Real.log (Real.log (2 : ℝ)).
Uses library neg_abs_le, Real.log.
Lean, line 333
```
  have h5 := neg_abs_le (Real.log (Real.log 2))
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 333 at 061cea5f5749 ↗
h6 have Real.log (Real.log (2 : ℝ)) ≤ |Real.log (Real.log (2 : ℝ))|
Leaves |∑ p ∈ x.primesLE, (1 : ℝ) / (↑p : ℝ) - Real.log (Real.log (↑x : ℝ))| ≤ (1 : ℝ) + C / Real.log (2 : ℝ) + |Real.log (Real.log (2 : ℝ))| + (C + (1 : ℝ)) / Real.log (2 : ℝ), with h6 : Real.log (Real.log (2 : ℝ)) ≤ |Real.log (Real.log (2 : ℝ))|.
Uses library le_abs_self, Real.log.
Lean, line 334
```
  have h6 := le_abs_self (Real.log (Real.log 2))
```
targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, line 334 at 061cea5f5749 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000343.json, merge commit 061cea5f5749.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/spec-7d098d5c/Proof.lean, sha256 8570ff8364c6.

import Mathlib
import Nodes.«spec-7d098d5c».Context

/-- Mertens' second theorem, bounded-error form: the sum of `1 / p` over the primes `p ≤ x`
is `log log x + O(1)`, uniformly for natural `x ≥ 2`. Mathlib at this target's pin has
Chebyshev's bounds but no Mertens estimate; this is the one analytic fact outside Mathlib that
the composite-dilation argument for erdos-69 uses (annex 9445873d on `erdos-69`). It is an
ingredient, not the hard step: nothing about `ω` or irrationality is in it. -/
theorem Opn.erdos_69_mertens_reciprocal_primes :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : ℕ, 2 ≤ x →
      |∑ p ∈ Nat.primesLE x, (1 : ℝ) / p - Real.log (Real.log (x : ℝ))| ≤ C := by
  -- Step 1 (69-R2-a, written from Mathlib alone): `∑_{p ≤ n} (log p)/p = log n + O(1)`,
  -- from `log n! = ∑_p v_p(n!) log p`, Legendre's bounds `n/p - 1 ≤ v_p(n!) ≤ n/(p-1)`,
  -- `n log n - n ≤ log n! ≤ n log n` and Chebyshev's `θ(n) ≤ n log 4`.
  have hM : ∃ C : ℝ, ∀ n : ℕ,
      |∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) - Real.log n| ≤ C := by
    -- (a) Stirling lower bound, by induction
    have hstir : ∀ n : ℕ, (n : ℝ) * Real.log n - n ≤ Real.log (n.factorial : ℝ) := by
      intro n
      induction n with
      | zero => simp
      | succ n ih =>
        have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast n.factorial_pos
        have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
        rw [Nat.factorial_succ, Nat.cast_mul, Real.log_mul hn1.ne' hf.ne']
        rcases Nat.eq_zero_or_pos n with h0 | hpos
        · subst h0
          simp
        · have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos
          have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)
              = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm
          have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity)
          have h3 : (n : ℝ) * (((n + 1 : ℕ) : ℝ) / n - 1) = 1 := by
            push_cast
            field_simp
            ring
          have h4 : (n : ℝ) * (Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)) ≤ 1 := by
            rw [h1, ← h3]
            exact mul_le_mul_of_nonneg_left h2 hn0.le
          push_cast at h4 ih ⊢
          nlinarith
    -- (b) the prime-power tail: ∑_{2 ≤ m ≤ k+1} log m / (m (m-1)) ≤ 2
    have htail : ∀ k : ℕ, ∑ m ∈ Finset.Icc 2 (k + 1), Real.log (m : ℝ) / ((m : ℝ) * ((m : ℝ) - 1))
        ≤ 2 - (Real.log ((k + 1 : ℕ) : ℝ) + 2) / ((k + 1 : ℕ) : ℝ) := by
      intro k
      induction k with
      | zero => simp
      | succ k ih =>
        rw [Finset.sum_Icc_succ_top (by omega)]
        have ha : (0 : ℝ) < ((k + 1 : ℕ) : ℝ) := by positivity
        have ha1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ k + 1)
        have hb : (0 : ℝ) < ((k + 1 + 1 : ℕ) : ℝ) := by positivity
        have hbe : ((k + 1 + 1 : ℕ) : ℝ) = ((k + 1 : ℕ) : ℝ) + 1 := by push_cast; ring
        have h1 : Real.log ((k + 1 + 1 : ℕ) : ℝ) - Real.log ((k + 1 : ℕ) : ℝ)
            = Real.log (((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ)) :=
          (Real.log_div hb.ne' ha.ne').symm
        have h2 := Real.log_le_sub_one_of_pos
          (show 0 < ((k + 1 + 1 : ℕ) : ℝ) / ((k + 1 : ℕ) : ℝ) by positivity)
        rw [← h1, hbe] at h2
        rw [hbe] at hb ⊢
        generalize ((k + 1 : ℕ) : ℝ) = a at *
        generalize Real.log a = L1 at *
        generalize Real.log (a + 1) = L2 at *
        have h3 : (a + 1) / a - 1 = 1 / a := by field_simp; ring
        have h4 : a * (L2 - L1) ≤ 1 := by
          have := mul_le_mul_of_nonneg_left h2 ha.le
          rw [h3] at this
          have e : a * (1 / a) = 1 := by field_simp
          linarith
        have h5 : L2 - L1 ≤ 1 := by
          have : 1 / a ≤ 1 := by rw [div_le_one ha]; exact ha1
          linarith [h3 ▸ h2]
        have e : (L1 + 2) / a - (L2 + 2) / (a + 1) - L2 / ((a + 1) * (a + 1 - 1))
            = (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) := by
          rw [show a + 1 - 1 = a by ring]
          field_simp
          ring
        have : 0 ≤ (2 - (a * (L2 - L1) + (L2 - L1))) / (a * (a + 1)) :=
          div_nonneg (by linarith) (by positivity)
        linarith
    refine ⟨3, ?_⟩
    intro n
    rcases Nat.eq_zero_or_pos n with h0 | hpos
    · subst h0
      simp
    have hn0 : (0 : ℝ) < n := by exact_mod_cast hpos
    have hfne : n.factorial ≠ 0 := n.factorial_ne_zero
    -- (c) log n! as a sum over primes ≤ n
    have hfac : Real.log (n.factorial : ℝ)
        = ∑ p ∈ Nat.primesLE n, (n.factorial.factorization p : ℝ) * Real.log (p : ℝ) := by
      rw [Real.log_nat_eq_sum_factorization]
      refine Finsupp.sum_of_support_subset _ ?_ _ (fun i _ => by simp)
      intro p hp
      rw [Nat.support_factorization, Nat.mem_primeFactors] at hp
      exact Nat.mem_primesLE.mpr ⟨(Nat.Prime.dvd_factorial hp.1).mp hp.2.1, hp.1⟩
    -- (d) Legendre bounds on the exponent
    have hleg : ∀ p ∈ Nat.primesLE n,
        (n : ℝ) / p - 1 ≤ (n.factorial.factorization p : ℝ) ∧
          (n.factorial.factorization p : ℝ) ≤ (n : ℝ) / ((p : ℝ) - 1) := by
      intro p hp
      have hpp := (Nat.mem_primesLE.mp hp).2
      have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast hpp.two_le
      have hp0 : (0 : ℝ) < p := by linarith
      constructor
      · have hd : p ^ (n / p) ∣ n.factorial := by
          have h1 : n.factorial.factorization p ≥ n / p := by
            have h2 := Nat.factorization_factorial_mul (n := n / p) hpp
            have h3 : (p * (n / p)).factorial ∣ n.factorial :=
              Nat.factorial_dvd_factorial (Nat.mul_div_le n p)
            have h4 := (Nat.factorization_le_iff_dvd (Nat.factorial_ne_zero _) hfne).mpr h3 p
            omega
          exact (hpp.pow_dvd_iff_le_factorization hfne).mpr h1
        have h1 : n / p ≤ n.factorial.factorization p :=
          (hpp.pow_dvd_iff_le_factorization hfne).mp hd
        have h2 : (n : ℝ) < ((n / p : ℕ) : ℝ) * p + p := by
          have : n < n / p * p + p := by
            have := Nat.div_add_mod n p
            have := Nat.mod_lt n hpp.pos
            nlinarith [Nat.mul_comm p (n / p)]
          exact_mod_cast this
        have h3 : ((n / p : ℕ) : ℝ) ≤ (n.factorial.factorization p : ℝ) := by exact_mod_cast h1
        rw [sub_le_iff_le_add, div_le_iff₀ hp0]
        nlinarith
      · have h1 : (p - 1) * n.factorial.factorization p ≤ n := by
          rw [← Nat.multiplicity_eq_factorization hpp hfne, hpp.sub_one_mul_multiplicity_factorial]
          exact Nat.sub_le _ _
        have h2 : ((p : ℝ) - 1) * (n.factorial.factorization p : ℝ) ≤ n := by
          have : (((p - 1 : ℕ) : ℝ)) * (n.factorial.factorization p : ℝ) ≤ n := by exact_mod_cast h1
          rwa [Nat.cast_sub hpp.one_le, Nat.cast_one] at this
        rw [le_div_iff₀ (by linarith)]
        linarith
    have hlogp : ∀ p ∈ Nat.primesLE n, 0 ≤ Real.log (p : ℝ) := fun p _ =>
      Real.log_natCast_nonneg p
    -- (e) Chebyshev
    have hθ : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) ≤ Real.log 4 * n := by
      have h := Chebyshev.theta_le_log4_mul_x (x := (n : ℝ)) hn0.le
      rw [Chebyshev.theta_eq_sum_Icc, Nat.floor_natCast] at h
      refine le_trans (le_of_eq ?_) h
      refine Finset.sum_congr ?_ (fun _ _ => rfl)
      ext p
      simp [Nat.mem_primesLE]
    have hl4 : Real.log 4 ≤ 3 := by
      have := Real.log_le_sub_one_of_pos (show (0 : ℝ) < 4 by norm_num)
      linarith
    -- (f) upper bound
    have hup : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ)
        ≤ (n : ℝ) * Real.log n + Real.log 4 * n := by
      have h1 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ)
          ≤ Real.log (n.factorial : ℝ) := by
        rw [hfac]
        exact Finset.sum_le_sum fun p hp =>
          mul_le_mul_of_nonneg_right (hleg p hp).1 (hlogp p hp)
      have h2 : ∑ p ∈ Nat.primesLE n, ((n : ℝ) / p - 1) * Real.log (p : ℝ)
          = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ)
            - ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) := by
        rw [Finset.mul_sum, ← Finset.sum_sub_distrib]
        exact Finset.sum_congr rfl fun p _ => by ring
      have h3 : Real.log (n.factorial : ℝ) ≤ (n : ℝ) * Real.log n := by
        rw [← Real.log_pow]
        exact Real.log_le_log (by exact_mod_cast n.factorial_pos)
          (by exact_mod_cast Nat.factorial_le_pow n)
      linarith
    -- (g) lower bound
    have hlo : (n : ℝ) * Real.log n - n
        ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) + (n : ℝ) * 2 := by
      have h1 : Real.log (n.factorial : ℝ)
          ≤ ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ) := by
        rw [hfac]
        exact Finset.sum_le_sum fun p hp =>
          mul_le_mul_of_nonneg_right (hleg p hp).2 (hlogp p hp)
      have h2 : ∑ p ∈ Nat.primesLE n, (n : ℝ) / ((p : ℝ) - 1) * Real.log (p : ℝ)
          = (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ)
            + (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) := by
        rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
        refine Finset.sum_congr rfl fun p hp => ?_
        have hp2 : (2 : ℝ) ≤ p := by exact_mod_cast (Nat.mem_primesLE.mp hp).2.two_le
        have : (p : ℝ) - 1 ≠ 0 := by linarith
        have : (p : ℝ) ≠ 0 := by linarith
        field_simp
        ring
      have h3 : ∑ p ∈ Nat.primesLE n, Real.log (p : ℝ) / ((p : ℝ) * ((p : ℝ) - 1)) ≤ 2 := by
        have hsub : Nat.primesLE n ⊆ Finset.Icc 2 (n - 1 + 1) := by
          intro p hp
          have := Nat.mem_primesLE.mp hp
          have := this.2.two_le
          rw [Finset.mem_Icc]
          omega
        refine (Finset.sum_le_sum_of_subset_of_nonneg hsub fun m hm _ => ?_).trans ?_
        · have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast (Finset.mem_Icc.mp hm).1
          exact div_nonneg (Real.log_natCast_nonneg m) (by nlinarith)
        · refine (htail (n - 1)).trans ?_
          have : 0 ≤ (Real.log ((n - 1 + 1 : ℕ) : ℝ) + 2) / ((n - 1 + 1 : ℕ) : ℝ) :=
            div_nonneg (by linarith [Real.log_natCast_nonneg (n - 1 + 1)]) (by positivity)
          linarith
      have h4 := mul_le_mul_of_nonneg_left h3 hn0.le
      linarith [hstir n]
    rw [abs_le]
    constructor
    · have : (n : ℝ) * (Real.log n - 3) ≤ (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) := by
        linarith
      linarith [le_of_mul_le_mul_left this hn0]
    · have : (n : ℝ) * ∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ) ≤ (n : ℝ) * (Real.log n + 3) := by
        nlinarith
      linarith [le_of_mul_le_mul_left this hn0]
  -- Step 2 (69-R1-b's own work, annex b8402c93): discrete Abel summation against `1 / log n`.
  obtain ⟨C, hC⟩ := hM
  have hC0 : 0 ≤ C := (abs_nonneg _).trans (hC 0)
  have hl2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
  have hL : ∀ n : ℕ, 2 ≤ n → Real.log 2 ≤ Real.log (n : ℝ) := fun n hn =>
    Real.log_le_log (by norm_num) (by exact_mod_cast hn)
  have htel : ∀ f : ℕ → ℝ, ∀ x : ℕ, 2 ≤ x →
      ∑ n ∈ Finset.Ico 2 x, (f (n + 1) - f n) = f x - f 2 := by
    intro f x hx
    induction x, hx using Nat.le_induction with
    | base => simp
    | succ x hx ih => rw [Finset.sum_Ico_succ_top hx, ih]; ring
  have htel' : ∀ f : ℕ → ℝ, ∀ x : ℕ, 2 ≤ x →
      ∑ n ∈ Finset.Ico 2 x, (f n - f (n + 1)) = f 2 - f x := by
    intro f x hx
    induction x, hx using Nat.le_induction with
    | base => simp
    | succ x hx ih => rw [Finset.sum_Ico_succ_top hx, ih]; ring
  have habel : ∀ x : ℕ, 2 ≤ x →
      ∑ p ∈ Nat.primesLE x, (1 : ℝ) / p
        = (∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ)) / Real.log (x : ℝ)
          + ∑ n ∈ Finset.Ico 2 x, (∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ))
              * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ)) := by
    intro x hx
    induction x, hx using Nat.le_induction with
    | base =>
      have h2 : Nat.primesLE 2 = {2} := by decide
      have : Real.log 2 ≠ 0 := hl2.ne'
      simp [h2]
      field_simp
    | succ x hx ih =>
      have ha : Real.log (x : ℝ) ≠ 0 := (lt_of_lt_of_le hl2 (hL x hx)).ne'
      have hb : Real.log ((x + 1 : ℕ) : ℝ) ≠ 0 :=
        (lt_of_lt_of_le hl2 (hL (x + 1) (by omega))).ne'
      have hnot : x + 1 ∉ Nat.primesLE x := fun h => by
        have := (Nat.mem_primesLE.mp h).1
        omega
      have hx1 : ((x + 1 : ℕ) : ℝ) ≠ 0 := by positivity
      rw [Finset.sum_Ico_succ_top hx, Nat.primesLE_succ]
      split_ifs with hp
      · rw [Finset.sum_insert hnot, Finset.sum_insert hnot, ih]
        field_simp
        ring
      · rw [ih]
        field_simp
        ring
  have hreal : ∀ a b A : ℝ, 0 < a → a ≤ b → b - a ≤ 1 → |A - a| ≤ C →
      0 ≤ 1 / a - 1 / b ∧
        |A * (1 / a - 1 / b) - (Real.log b - Real.log a)| ≤ (C + 1) * (1 / a - 1 / b) := by
    intro a b A ha0 hab hba hA
    have hb0 : 0 < b := ha0.trans_le hab
    have hd0 : 0 ≤ 1 / a - 1 / b := by
      rw [sub_nonneg]
      exact one_div_le_one_div_of_le ha0 hab
    have hv : Real.log b - Real.log a = Real.log (b / a) :=
      (Real.log_div hb0.ne' ha0.ne').symm
    have hlow := Real.one_sub_inv_le_log_of_pos (show 0 < b / a by positivity)
    have hup := Real.log_le_sub_one_of_pos (show 0 < b / a by positivity)
    have hR := abs_le.mp hA
    have hu : a * (1 / a - 1 / b) = 1 - (b / a)⁻¹ := by
      field_simp
    have hw : b / a - 1 - (1 - (b / a)⁻¹) = (b - a) * (1 / a - 1 / b) := by
      field_simp
    have hw2 : (b - a) * (1 / a - 1 / b) ≤ 1 * (1 / a - 1 / b) :=
      mul_le_mul_of_nonneg_right hba hd0
    have h1 : -C * (1 / a - 1 / b) ≤ (A - a) * (1 / a - 1 / b) :=
      mul_le_mul_of_nonneg_right hR.1 hd0
    have h2 : (A - a) * (1 / a - 1 / b) ≤ C * (1 / a - 1 / b) :=
      mul_le_mul_of_nonneg_right hR.2 hd0
    have e : A * (1 / a - 1 / b) - (Real.log b - Real.log a)
        = (A - a) * (1 / a - 1 / b) + (a * (1 / a - 1 / b) - Real.log (b / a)) := by
      rw [hv]
      ring
    refine ⟨hd0, ?_⟩
    rw [e, abs_le]
    constructor <;> nlinarith
  have hpt : ∀ n : ℕ, 2 ≤ n →
      |(∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ))
            * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ))
          - (Real.log (Real.log ((n + 1 : ℕ) : ℝ)) - Real.log (Real.log (n : ℝ)))|
        ≤ (C + 1) * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ)) := by
    intro n hn
    have hn0 : (0 : ℝ) < n := by exact_mod_cast (by omega : 0 < n)
    have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
    have hab : Real.log (n : ℝ) ≤ Real.log ((n + 1 : ℕ) : ℝ) :=
      Real.log_le_log hn0 (by push_cast; linarith)
    have hba : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ) ≤ 1 := by
      have h1 : Real.log ((n + 1 : ℕ) : ℝ) - Real.log (n : ℝ)
          = Real.log (((n + 1 : ℕ) : ℝ) / n) := (Real.log_div hn1.ne' hn0.ne').symm
      have h2 := Real.log_le_sub_one_of_pos (show 0 < ((n + 1 : ℕ) : ℝ) / n by positivity)
      have h3 : ((n + 1 : ℕ) : ℝ) / n - 1 = 1 / n := by
        push_cast
        field_simp
        ring
      have h4 : (1 : ℝ) / n ≤ 1 := by
        rw [div_le_one hn0]
        exact_mod_cast (by omega : 1 ≤ n)
      linarith
    exact (hreal _ _ _ (lt_of_lt_of_le hl2 (hL n hn)) hab hba (hC n)).2
  refine ⟨1 + C / Real.log 2 + |Real.log (Real.log 2)| + (C + 1) / Real.log 2, by positivity, ?_⟩
  intro x hx
  have hLx : Real.log 2 ≤ Real.log (x : ℝ) := hL x hx
  have hLx0 : 0 < Real.log (x : ℝ) := hl2.trans_le hLx
  have hv := htel (fun n => Real.log (Real.log (n : ℝ))) x hx
  have hd := htel' (fun n => 1 / Real.log (n : ℝ)) x hx
  simp only [Nat.cast_ofNat] at hv hd
  have hsum : |∑ n ∈ Finset.Ico 2 x, ((∑ p ∈ Nat.primesLE n, Real.log p / (p : ℝ))
            * (1 / Real.log (n : ℝ) - 1 / Real.log ((n + 1 : ℕ) : ℝ))
          - (Real.log (Real.log ((n + 1 : ℕ) : ℝ)) - Real.log (Real.log (n : ℝ))))|
        ≤ (C + 1) / Real.log 2 := by
    refine (Finset.abs_sum_le_sum_abs _ _).trans ?_
    refine (Finset.sum_le_sum (fun n hn => hpt n (Finset.mem_Ico.mp hn).1)).trans ?_
    rw [← Finset.mul_sum, hd, div_eq_mul_one_div (C + 1)]
    have : 0 ≤ 1 / Real.log (x : ℝ) := by positivity
    nlinarith
  rw [Finset.sum_sub_distrib, hv] at hsum
  have hq : |(∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ) - Real.log (x : ℝ)) / Real.log (x : ℝ)|
      ≤ C / Real.log 2 := by
    rw [abs_div, abs_of_pos hLx0]
    calc _ ≤ C / Real.log (x : ℝ) := by gcongr; exact hC x
      _ ≤ C / Real.log 2 := by gcongr
  have e1 : (∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ)) / Real.log (x : ℝ)
      = 1 + (∑ p ∈ Nat.primesLE x, Real.log p / (p : ℝ) - Real.log (x : ℝ)) / Real.log (x : ℝ) := by
    rw [sub_div, div_self hLx0.ne']
    ring
  have hab := habel x hx
  have h3 := abs_le.mp hsum
  have h4 := abs_le.mp hq
  have h5 := neg_abs_le (Real.log (Real.log 2))
  have h6 := le_abs_self (Real.log (Real.log 2))
  rw [abs_le]
  constructor <;> linarith

What is known

Work on it

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

Write the explainer →

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

Record

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

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

import Mathlib
import Nodes.«spec-7d098d5c».Context

/-- Mertens' second theorem, bounded-error form: the sum of `1 / p` over the primes `p ≤ x`
is `log log x + O(1)`, uniformly for natural `x ≥ 2`. Mathlib at this target's pin has
Chebyshev's bounds but no Mertens estimate; this is the one analytic fact outside Mathlib that
the composite-dilation argument for erdos-69 uses (annex 9445873d on `erdos-69`). It is an
ingredient, not the hard step: nothing about `ω` or irrationality is in it. -/
theorem Opn.erdos_69_mertens_reciprocal_primes :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : ℕ, 2 ≤ x →
      |∑ p ∈ Nat.primesLE x, (1 : ℝ) / p - Real.log (Real.log (x : ℝ))| ≤ C := by
  sorry

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

Draft · drafted, by the model named above

$\displaystyle \exists C\ge 0\ \ \forall x\in\mathbb{N},\ x\ge 2:\quad \Bigl\lvert \sum_{p\le x,\ p\ \text{prime}}\frac{1}{p} - \log\log x \Bigr\rvert \le C$

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

Rendered from targets/erdos-69/nodes/spec-7d098d5c/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000343.json, merge commit 061cea5f5749.

Verdict pass, from attestations/000343.json.

Submitter: t1001-69-b
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

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

Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000343.json, merge commit 061cea5f5749.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-7d098d5c/Witness.lean, sha256 b84e7037ab4c.

import Mathlib

theorem witness : True := trivial

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

Acknowledged findings (3)

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

Untrusted: acknowledgment of a div-zero finding at 1 / ↑p

p ranges over primes, so p ≥ 2 and 1/p is never the junk value.

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

Untrusted: acknowledgment of a off-by-one-range finding at 2 ≤ x

Inclusive on purpose: the bound is claimed for every x ≥ 2; below 2, log log x is not meaningful (log 1 = 0).

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

Untrusted: acknowledgment of a junk-value finding at Real.log (Real.log ↑x)

The hypothesis 2 ≤ x gives log x ≥ log 2 > 0, so the outer logarithm is taken of a positive number.

How to read this page

How to read a statement’s page →