awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
neg : LE.le (α := ℝ) (↑⌈y⌉₊ : ℝ) (↑(⌊y⌋₊ + 1) : ℝ)
⊢ y ≤ (↑(⌊y⌋₊ + 1) : ℝ)

Tactic:
apply (Nat.le_ceil y).trans

Premises used: Nat.le_ceil, LE.le.trans
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
neg : ⌈y⌉₊ ≤ ⌊y⌋₊ + 1
⊢ LE.le (α := ℝ) (↑⌈y⌉₊ : ℝ) (↑(⌊y⌋₊ + 1) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ ⌈y⌉₊ ≤ ⌊y⌋₊ + 1

Tactic:
Nat.ceil_le_floor_add_one y

Premises used: Nat.ceil_le_floor_add_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ ⌈y⌉₊ ≤ ⌊y⌋₊ + 1

Tactic:
exact Nat.ceil_le_floor_add_one y

Premises used: Nat.ceil_le_floor_add_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 1 ≤ y
⊢ (↑(harmonic ⌊y⌋₊) : ℝ) ≤ 1 + Real.log y

Tactic:
(harmonic_le_one_add_log _).trans ?_

Premises used: harmonic_le_one_add_log, LE.le.trans
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 1 ≤ y
refine : 1 + Real.log (↑⌊y⌋₊ : ℝ) ≤ 1 + Real.log y
⊢ (↑(harmonic ⌊y⌋₊) : ℝ) ≤ 1 + Real.log y

Tactic:
refine (harmonic_le_one_add_log _).trans ?_

Premises used: harmonic_le_one_add_log, LE.le.trans
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 1 ≤ y
bc : LT.lt (α := ℝ) 0 (↑⌊y⌋₊ : ℝ)
bc₁ : (↑⌊y⌋₊ : ℝ) ≤ y
⊢ 1 + Real.log (↑⌊y⌋₊ : ℝ) ≤ 1 + Real.log y

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 1 ≤ y
⊢ LT.lt (α := ℝ) 0 (↑⌊y⌋₊ : ℝ)

Tactic:
exact_mod_cast Nat.floor_pos.mpr hy

Premises used: Iff.mpr, Nat.floor_pos
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 1 ≤ y
⊢ (↑⌊y⌋₊ : ℝ) ≤ y

Tactic:
Nat.floor_le <| zero_le_one.trans hy

Premises used: zero_le_one, Nat.floor_le, LE.le.trans
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 1 ≤ y
⊢ (↑⌊y⌋₊ : ℝ) ≤ y

Tactic:
exact Nat.floor_le <| zero_le_one.trans hy

Premises used: zero_le_one, Nat.floor_le, LE.le.trans
-- Module: Mathlib.NumberTheory.Harmonic.Defs
Goal:
⊢ harmonic 0 = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, harmonic, List.foldr, Finset.sum, rfl
-- Module: Mathlib.NumberTheory.Harmonic.Defs
Goal:
n : ℕ
⊢ harmonic (n + 1) = harmonic n + (↑(n + 1) : ℚ)⁻¹

Tactic:
Finset.sum_range_succ ..

Premises used: harmonic, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ eulerMascheroniSeq 0 = 0

Tactic:
simp [eulerMascheroniSeq, harmonic_zero]

Premises used: Real.eulerMascheroniSeq, harmonic_zero
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ StrictMono eulerMascheroniSeq

Tactic:
strictMono_nat_of_lt_succ (fun n ↦ ?_)

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
refine : ∀ (n : ℕ), eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)
⊢ StrictMono eulerMascheroniSeq

Tactic:
refine strictMono_nat_of_lt_succ (fun n ↦ ?_)

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
rw : log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)

Tactic:
rw [eulerMascheroniSeq, eulerMascheroniSeq, ← sub_pos, sub_sub_sub_comm,
    harmonic_succ, add_comm, Rat.cast_add, add_sub_cancel_right,
    ← log_div (by positivity) (by positivity), add_div, Nat.cast_add_one,
    Nat.cast_add_one, div_self (by positivity), sub_pos, one_div, Rat.cast_inv, Rat.cast_add,
    Rat.cast_one, Rat.cast_natCast]

Premises used: sub_pos, sub_sub_sub_comm, Real.eulerMascheroniSeq, Real.log_div, add_comm, Rat.cast_inv, harmonic_succ, Rat.cast_natCast, one_div, Rat.cast_add, add_sub_cancel_right, Nat.cast_add_one, div_self, Rat.cast_one, add_div
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
(log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)

Premises used: lt_add_of_pos_right, ne_of_gt, Real.log_lt_sub_one_of_pos, LT.lt.trans_le, le_of_eq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
refine_1 : 0 < 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
refine_2 : 0 < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
refine_3 : 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ - 1 = (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)

Premises used: lt_add_of_pos_right, ne_of_gt, Real.log_lt_sub_one_of_pos, LT.lt.trans_le, le_of_eq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ 0 < 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ 0 < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ - 1 = (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
simp only [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ (↑(harmonic 6) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑6 : ℝ) 1) = 49 / 20 - log 7

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ eulerMascheroniSeq 6 = 49 / 20 - log 7

Tactic:
have : eulerMascheroniSeq 6 = 49 / 20 - log 7 := by
    rw [eulerMascheroniSeq]
    norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ LT.lt (α := ℝ) 0 7

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
rw : 7 < rexp (49 / 20 - 1 / 2)
⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
rw [this, lt_sub_iff_add_lt, ← lt_sub_iff_add_lt', log_lt_iff_lt_exp (by positivity)]

Premises used: lt_sub_iff_add_lt', Real.log_lt_iff_lt_exp, lt_sub_iff_add_lt
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 0 ≤ 49 / 20 - 1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
refine : LT.lt (α := ℝ) 7 (∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / (↑i.factorial : ℝ))
⊢ 7 < rexp (49 / 20 - 1 / 2)

Tactic:
refine lt_of_lt_of_le ?_ (Real.sum_le_exp_of_nonneg (by norm_num) 7)

Premises used: Real.sum_le_exp_of_nonneg, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
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)))))) :
          ℝ)
⊢ LT.lt (α := ℝ) 7 (∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / (↑i.factorial : ℝ))

Tactic:
simp_rw [Finset.sum_range_succ, Nat.factorial_succ]

Premises used: Nat.factorial_succ, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 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:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ eulerMascheroniSeq' 1 = 1

Tactic:
simp [eulerMascheroniSeq']

Premises used: Real.eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ StrictAnti eulerMascheroniSeq'

Tactic:
strictAnti_nat_of_succ_lt (fun n ↦ ?_)

Premises used: strictAnti_nat_of_succ_lt
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
refine : ∀ (n : ℕ), eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
⊢ StrictAnti eulerMascheroniSeq'

Tactic:
refine strictAnti_nat_of_succ_lt (fun n ↦ ?_)

Premises used: strictAnti_nat_of_succ_lt
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
inl : eulerMascheroniSeq' (HAdd.hAdd (α := ℕ) 0 1) < eulerMascheroniSeq' 0
inr : ∀ (hn : n > 0), eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ eulerMascheroniSeq' (HAdd.hAdd (α := ℕ) 0 1) < eulerMascheroniSeq' 0

Tactic:
simp [eulerMascheroniSeq']

Premises used: Real.eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
inr : (↑(harmonic (n + 1)) : ℝ) - log (↑(n + 1) : ℝ) < (↑(harmonic n) : ℝ) - log (↑n : ℝ)
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
simp_rw [eulerMascheroniSeq', eq_false_intro hn.ne', reduceCtorEq, if_false]

Premises used: reduceCtorEq, if_false, LT.lt.ne', Real.eulerMascheroniSeq', eq_false_intro
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
⊢ Ne (α := ℝ) (↑(n + 1) : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
inr : log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
⊢ (↑(harmonic (n + 1)) : ℝ) - log (↑(n + 1) : ℝ) < (↑(harmonic n) : ℝ) - log (↑n : ℝ)

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]

Premises used: sub_pos, neg_lt_neg_iff, neg_sub, sub_self, sub_sub_sub_comm, sub_eq_neg_add, sub_eq_add_neg, Real.log_div, sub_sub, harmonic_succ, Rat.cast_add, Real.log_inv, zero_sub
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
⊢ log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)

Tactic:
(log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)

Premises used: Real.log_lt_sub_one_of_pos, LT.lt.trans_le, le_of_eq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
inr : 0 < (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹
inr₁ : (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ ≠ 1
inr₂ : (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ - 1 = -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)
⊢ log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ < -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)

Tactic:
refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)

Premises used: Real.log_lt_sub_one_of_pos, LT.lt.trans_le, le_of_eq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
⊢ 0 < (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
⊢ (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ ≠ 1

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n > 0
⊢ (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ))⁻¹ - 1 = -(↑(↑(n + 1) : ℚ)⁻¹ : ℝ)

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ (if Eq (α := ℕ) 6 0 then 2 else (↑(harmonic 6) : ℝ) - log (↑6 : ℝ)) = 49 / 20 - log 6

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ eulerMascheroniSeq' 6 = 49 / 20 - log 6

Tactic:
have h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6 := by
    rw [eulerMascheroniSeq']
    norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ LT.lt (α := ℝ) 0 6

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
rw : rexp (49 / 20 - 2 / 3) < 6
⊢ eulerMascheroniSeq' 6 < 2 / 3

Tactic:
rw [h1, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add', lt_log_iff_exp_lt (by positivity)]

Premises used: Real.lt_log_iff_exp_lt, sub_lt_iff_lt_add', sub_lt_iff_lt_add
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
norm_num : rexp (107 / 60) < 6
⊢ rexp (49 / 20 - 2 / 3) < 6

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 0 < 107 / 60

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 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)
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp 1 ^ (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)

Tactic:
rw [exp_one_rpow] at this

Premises used: Real.exp_one_rpow
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ rexp (107 / 60) < 6

Tactic:
lt_trans this ?_

Premises used: lt_trans
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
refine : HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 6
⊢ rexp (107 / 60) < 6

Tactic:
refine lt_trans this ?_

Premises used: lt_trans
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
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
hz : LT.lt (α := ℝ) 0 60
⊢ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60) < 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]

Premises used: Nat.cast_ofNat, div_mul_cancel₀, Real.rpow_lt_rpow_iff, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2.7182818286 107 < HPow.hPow (α := ℝ) (β := ℕ) 6 (OfNat.ofNat 60)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ Ne (α := ℝ) 60 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ LE.le (α := ℝ) 0 2.7182818286

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ 0 ≤ HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ LE.le (α := ℝ) 0 6

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < HPow.hPow (α := ℝ) 2.7182818286 (107 / 60)
⊢ LT.lt (α := ℝ) 0 60

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n r : ℕ
inl : eulerMascheroniSeq 0 < eulerMascheroniSeq' 0
inr : ∀ (hr : 0 < r), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
rcases eq_zero_or_pos r with rfl | hr

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n : ℕ
⊢ eulerMascheroniSeq 0 < eulerMascheroniSeq' 0

Tactic:
simp [eulerMascheroniSeq, eulerMascheroniSeq']

Premises used: Real.eulerMascheroniSeq, Real.eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n r : ℕ
hr : 0 < r
inr : (↑(harmonic r) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1) < (↑(harmonic r) : ℝ) - log (↑r : ℝ)
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]

Premises used: if_false, Real.eulerMascheroniSeq, LT.lt.ne', Real.eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n r : ℕ
hr : 0 < r
inr : (↑r : ℝ) < HAdd.hAdd (α := ℝ) (↑r : ℝ) 1
⊢ (↑(harmonic r) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1) < (↑(harmonic r) : ℝ) - log (↑r : ℝ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n r : ℕ
hr : 0 < r
linarith : HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 ≤ (↑r : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 - (↑r : ℝ)) = 0
⊢ (↑r : ℝ) < HAdd.hAdd (α := ℝ) (↑r : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n : ℕ
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
apply : eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n

Tactic:
apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt

Premises used: StrictMono.monotone, Real.strictMono_eulerMascheroniSeq, le_max_left, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n

Tactic:
(this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

Premises used: le_max_right, Real.strictAnti_eulerMascheroniSeq', LT.lt.trans_le, StrictAnti.antitone
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n

Tactic:
exact (this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

Premises used: le_max_right, Real.strictAnti_eulerMascheroniSeq', LT.lt.trans_le, StrictAnti.antitone
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
refine_2 :
  ∀ (this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ (i : ℕ), eulerMascheroniSeq i))),
    Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
refine_1 : BddAbove (Set.range eulerMascheroniSeq)
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ (i : ℕ), eulerMascheroniSeq i))
refine_2 : Tendsto eulerMascheroniSeq atTop (𝓝 (limUnder atTop eulerMascheroniSeq))
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ (i : ℕ), eulerMascheroniSeq i))
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
rwa [eulerMascheroniConstant, this.limUnder_eq]

Premises used: Real.eulerMascheroniConstant, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ BddAbove (Set.range eulerMascheroniSeq)

Tactic:
⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩

Premises used: LE.le, BddAbove, Set.Nonempty, Exists.intro, _private.0.Real.tendsto_eulerMascheroniSeq.match_2
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ BddAbove (Set.range eulerMascheroniSeq)

Tactic:
exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) atTop (𝓝 eulerMascheroniConstant)

Tactic:
tendsto_eulerMascheroniSeq

Premises used: Real.eulerMascheroniSeq, Real.tendsto_eulerMascheroniSeq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
simpa using this.add tendsto_eulerMascheroniSeq

Premises used: Filter.Tendsto.add, Real.tendsto_eulerMascheroniSeq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
suffices : Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
suffices Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0) by
    simpa using this.add tendsto_eulerMascheroniSeq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
apply :
  EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) fun (n : ℕ) ↦
    eulerMascheroniSeq' n - eulerMascheroniSeq n
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)

Tactic:
apply (this.comp tendsto_natCast_atTop_atTop).congr'

Premises used: tendsto_natCast_atTop_atTop, Filter.Tendsto.comp, Filter.Tendsto.congr'