-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma eulerMascheroniSeq'_six_lt_two_thirds : eulerMascheroniSeq' 6 < 2 / 3

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 0 < 6

Tactic:
positivity

Result:
no goals

Proof state:
case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Tactic:
all_goals positivity

Result:
no goals

Proof state:
⊢ eulerMascheroniSeq' 6 < 2 / 3

Tactic:
have h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6 := by
  rw [eulerMascheroniSeq']
  norm_num

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ eulerMascheroniSeq' 6 < 2 / 3

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6

Tactic:
refine lt_trans this ?_

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ (107 / 60) < 6

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 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]

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ 107 < 6 ^ OfNat.ofNat 60

case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Proof state:
case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Tactic:
positivity

Result:
no goals

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (107 / 60) < 6

Tactic:
have := rpow_lt_rpow (exp_pos _).le exp_one_lt_d9 (by norm_num : (0 : ℝ) < 107 / 60)

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp 1 ^ (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6

Proof state:
⊢ (if 6 = 0 then 2 else ↑(harmonic 6) - log ↑6) = 49 / 20 - log 6

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ eulerMascheroniSeq' 6 = 49 / 20 - log 6

Tactic:
rw [eulerMascheroniSeq']

Result:
⊢ (if 6 = 0 then 2 else ↑(harmonic 6) - log ↑6) = 49 / 20 - log 6

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (49 / 20 - 2 / 3) < 6

Tactic:
norm_num

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (107 / 60) < 6

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp 1 ^ (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6

Tactic:
rw [exp_one_rpow] at this

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ 107 < 6 ^ OfNat.ofNat 60

Tactic:
norm_num

Result:
no goals

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 0 < 107 / 60

Tactic:
norm_num

Result:
no goals

Proof state:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 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)]

Result:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (49 / 20 - 2 / 3) < 6