awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ LT.lt (α := ℝ) 7 (∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / (↑i.factorial : ℝ))
have simp_rw : 7 <
  ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / (↑i.factorial : ℝ) +
                HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 0 / (↑(Nat.factorial 0) : ℝ) +
              HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 1 / (↑(HAdd.hAdd (α := ℕ) 0 1 * Nat.factorial 0) : ℝ) +
            HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 2 /
              (↑(HAdd.hAdd (α := ℕ) 1 1 * (HAdd.hAdd (α := ℕ) 0 1 * Nat.factorial 0)) : ℝ) +
          HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 3 /
            (↑(HAdd.hAdd (α := ℕ) 2 1 * (HAdd.hAdd (α := ℕ) 1 1 * (HAdd.hAdd (α := ℕ) 0 1 * Nat.factorial 0))) : ℝ) +
        HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 4 /
          (↑(HAdd.hAdd (α := ℕ) 3 1 *
                (HAdd.hAdd (α := ℕ) 2 1 * (HAdd.hAdd (α := ℕ) 1 1 * (HAdd.hAdd (α := ℕ) 0 1 * Nat.factorial 0)))) :
            ℝ) +
      HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 5 /
        (↑(HAdd.hAdd (α := ℕ) 4 1 *
              (HAdd.hAdd (α := ℕ) 3 1 *
                (HAdd.hAdd (α := ℕ) 2 1 * (HAdd.hAdd (α := ℕ) 1 1 * (HAdd.hAdd (α := ℕ) 0 1 * Nat.factorial 0))))) :
          ℝ) +
    HPow.hPow (β := ℕ) (49 / 20 - 1 / 2) 6 /
      (↑(HAdd.hAdd (α := ℕ) 5 1 *
            (HAdd.hAdd (α := ℕ) 4 1 *
              (HAdd.hAdd (α := ℕ) 3 1 *
                (HAdd.hAdd (α := ℕ) 2 1 * (HAdd.hAdd (α := ℕ) 1 1 * (HAdd.hAdd (α := ℕ) 0 1 * Nat.factorial 0)))))) :
        ℝ)
Tactic: simp_rw [Finset.sum_range_succ, Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ StrictAnti eulerMascheroniSeq'
have refine : ∀ (n : ℕ), eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
Tactic: refine strictAnti_nat_of_succ_lt (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
have inl : eulerMascheroniSeq' (HAdd.hAdd (α := ℕ) 0 1) < eulerMascheroniSeq' 0
Tactic: rcases Nat.eq_zero_or_pos n with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
inl : eulerMascheroniSeq' (HAdd.hAdd (α := ℕ) 0 1) < eulerMascheroniSeq' 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
have inr : ∀ (hn : n > 0), eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
Tactic: rcases Nat.eq_zero_or_pos n with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
have inr : (↑(harmonic (n + 1)) : ℝ) - log (↑(n + 1) : ℝ) < (↑(harmonic n) : ℝ) - log (↑n : ℝ)
Tactic: simp_rw [eulerMascheroniSeq', eq_false_intro hn.ne', reduceCtorEq, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n > 0
⊢ (↑(harmonic (n + 1)) : ℝ) - log (↑(n + 1) : ℝ) < (↑(harmonic n) : ℝ) - log (↑n : ℝ)
have inr : log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
Tactic: rw [← sub_pos, sub_sub_sub_comm,
    harmonic_succ, Rat.cast_add, ← sub_sub, sub_self, zero_sub, sub_eq_add_neg, neg_sub,
    ← sub_eq_neg_add, sub_pos, ← log_div (by positivity) (by positivity), ← neg_lt_neg_iff,
    ← log_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n > 0
⊢ log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
have inr : 0 < (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹
Tactic: refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n > 0
inr : 0 < (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹
⊢ log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
have inr₁ : (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ ≠ 1
Tactic: refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n > 0
inr : 0 < (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹
inr₁ : (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ ≠ 1
⊢ log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
have inr₂ : (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ - 1 = -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
Tactic: refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (hypothesis)
Goal:
⊢ eulerMascheroniSeq' 6 < 2 / 3
have h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
Tactic: have h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6 := by
    rw [eulerMascheroniSeq']
    norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ eulerMascheroniSeq' 6 < 2 / 3
have rw : rexp (49 / 20 - 2 / 3) < 6
Tactic: rw [h1, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add', lt_log_iff_exp_lt (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (49 / 20 - 2 / 3) < 6
have norm_num : rexp (107 / 60) < 6
Tactic: norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (hypothesis)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (107 / 60) < 6
have this : rexp 1 ^ (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
Tactic: have := rpow_lt_rpow (exp_pos _).le exp_one_lt_d9 (by simp : (0 : ℝ) < 107 / 60)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (hypothesis)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp 1 ^ (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ rexp (107 / 60) < 6
have this₁ : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
Tactic: rw [exp_one_rpow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ rexp (107 / 60) < 6
have refine : HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
Tactic: refine lt_trans this ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
have rw : HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)
Tactic: rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat,
    ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
have h : Ne (α := ℝ) 60 0
Tactic: rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat,
    ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)
h : Ne (α := ℝ) 60 0
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
have hx : LE.le (α := ℝ) 0 2.7182818286
Tactic: rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat,
    ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)
h : Ne (α := ℝ) 60 0
hx : LE.le (α := ℝ) 0 2.7182818286
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
have hx₁ : 0 ≤ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
Tactic: rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat,
    ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)
h : Ne (α := ℝ) 60 0
hx : LE.le (α := ℝ) 0 2.7182818286
hx₁ : 0 ≤ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
have hy : LE.le (α := ℝ) 0 6
Tactic: rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat,
    ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)
h : Ne (α := ℝ) 60 0
hx : LE.le (α := ℝ) 0 2.7182818286
hx₁ : 0 ≤ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
hy : LE.le (α := ℝ) 0 6
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
have hz : LT.lt (α := ℝ) 0 60
Tactic: rw [← rpow_lt_rpow_iff (z := 60), ← rpow_mul, div_mul_cancel₀, ← Nat.cast_ofNat,
    ← Nat.cast_ofNat, rpow_natCast, Nat.cast_ofNat, ← Nat.cast_ofNat (n := 60), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
m n r : ℕ
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r
have inl : eulerMascheroniSeq 0 < eulerMascheroniSeq' 0
Tactic: rcases eq_zero_or_pos r with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
m n r : ℕ
inl : eulerMascheroniSeq 0 < eulerMascheroniSeq' 0
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r
have inr : ∀ (hr : 0 < r), eulerMascheroniSeq r < eulerMascheroniSeq' r
Tactic: rcases eq_zero_or_pos r with rfl | hr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
m n r : ℕ
hr : 0 < r
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r
have inr : (↑(harmonic r) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1) < (↑(harmonic r) : ℝ) - log (↑r : ℝ)
Tactic: simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
m n r : ℕ
hr : 0 < r
⊢ (↑(harmonic r) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1) < (↑(harmonic r) : ℝ) - log (↑r : ℝ)
have inr : (↑r : ℝ) < HAdd.hAdd (α := ℝ) (↑r : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
m n r : ℕ
hr : 0 < r
⊢ (↑r : ℝ) < HAdd.hAdd (α := ℝ) (↑r : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 ≤ (↑r : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 - (↑r : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (hypothesis)
Goal:
m n : ℕ
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n
have this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
Tactic: have (r : ℕ) : eulerMascheroniSeq r < eulerMascheroniSeq' r := by
    rcases eq_zero_or_pos r with rfl | hr
    · simp [eulerMascheroniSeq, eulerMascheroniSeq']
    simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]
    gcongr
    linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n
have apply : eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n
Tactic: apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
have refine_2 : ∀ (this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ (i : ℕ), eulerMascheroniSeq i))),
  Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
Tactic: have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
refine_2 :
  ∀ (this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ (i : ℕ), eulerMascheroniSeq i))),
    Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
have refine_1 : BddAbove (Set.range eulerMascheroniSeq)
Tactic: have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ (i : ℕ), eulerMascheroniSeq i))
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
have refine_2 : Tendsto eulerMascheroniSeq atTop (𝓝 (limUnder atTop eulerMascheroniSeq))
Tactic: rwa [eulerMascheroniConstant, this.limUnder_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)
have suffices : Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
Tactic: suffices Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0) by
    simpa using this.add tendsto_eulerMascheroniSeq
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
have apply : EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) fun (n : ℕ) ↦
  eulerMascheroniSeq' n - eulerMascheroniSeq n
Tactic: apply (this.comp tendsto_natCast_atTop_atTop).congr'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) fun (n : ℕ) ↦
    eulerMascheroniSeq' n - eulerMascheroniSeq n
have h : ∀ (n : ℕ) (hn : n ≠ 0),
  ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) n = eulerMascheroniSeq' n - eulerMascheroniSeq n
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
have suffices : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
Tactic: suffices Tendsto (fun x : ℝ ↦ log (x + 1) - log x) atTop (𝓝 0) by
    apply (this.comp tendsto_natCast_atTop_atTop).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn
    simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (↑n : ℝ)) atTop (𝓝 eulerMascheroniConstant)
have apply : eulerMascheroniSeq' =ᶠ[atTop] fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (↑n : ℝ)
Tactic: apply tendsto_eulerMascheroniSeq'.congr'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ eulerMascheroniSeq' =ᶠ[atTop] fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (↑n : ℝ)
have h : ∀ (n : ℕ) (hn : n ≠ 0), eulerMascheroniSeq' n = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
have h : (if n = 0 then 2 else (↑(harmonic n) : ℝ) - log (↑n : ℝ)) = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
Tactic: simp_rw [eulerMascheroniSeq', hn, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
hn : n ≠ 0
h : (if n = 0 then 2 else (↑(harmonic n) : ℝ) - log (↑n : ℝ)) = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
⊢ eulerMascheroniSeq' n = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
have h₁ : (if False then 2 else (↑(harmonic n) : ℝ) - log (↑n : ℝ)) = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
Tactic: simp_rw [eulerMascheroniSeq', hn, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniConstant
have refine : eulerMascheroniSeq n.succ ≤ eulerMascheroniConstant
Tactic: refine (strictMono_eulerMascheroniSeq (Nat.lt_succ_self n)).trans_le ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n
have refine : eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ
Tactic: refine lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
m : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ -(↑m : ℝ)
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = -(↑m : ℝ) →
  -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + HSub.hSub (α := ℝ) 0 (↑m : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - -(↑m : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have rwa : ∀ (this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
  deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
Tactic: rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
rwa :
  ∀ (this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have rwa₁ : ∀
  (this :
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
  deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
Tactic: rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
rwa :
  ∀ (this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₁ :
  ∀
    (this :
      deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have rwa₂ : ∀ (this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / (↑n ! : ℝ) = -γ + (↑(harmonic n) : ℝ)),
  deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
Tactic: rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
rwa :
  ∀ (this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₁ :
  ∀
    (this :
      deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₂ :
  ∀ (this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / (↑n ! : ℝ) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have rwa₃ : ∀ (this : (-γ + (↑(harmonic n) : ℝ)) * (↑n ! : ℝ) = deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
  deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
Tactic: rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
rwa :
  ∀ (this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₁ :
  ∀
    (this :
      deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₂ :
  ∀ (this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / (↑n ! : ℝ) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₃ :
  ∀ (this : (-γ + (↑(harmonic n) : ℝ)) * (↑n ! : ℝ) = deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have rwa₄ : ∀ (this : (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ)) = deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
  deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
Tactic: rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
Cleared hypotheses: this