-- Mathlib/NumberTheory/Harmonic/Bounds.lean
theorem harmonic_le_one_add_log (n : ℕ) :
    harmonic n ≤ 1 + Real.log n

Proof state:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Icc 1 n, (↑x)⁻¹ ≤ 1 + Real.log ↑n

Tactic:
rw [← Finset.sum_erase_add (Finset.Icc 1 n) _ (Finset.left_mem_Icc.mpr hn), add_comm,
  Nat.cast_one, inv_one]

Result:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 + ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + Real.log ↑n

Proof state:
case h.e'_3.h.e'_5
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 = 2 - 1

Tactic:
norm_num

Result:
no goals

Proof state:
case neg.calc_2
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ ≤ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹

Tactic:
exact @AntitoneOn.sum_le_integral_Ico 2 (n + 1) (fun x : ℝ ↦ (x - 1)⁻¹) (by linarith [hn]) <|
  sub_inv_antitoneOn_Icc_right (by norm_num)

Result:
no goals

Proof state:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ Real.log ↑n

Tactic:
simp only [Nat.lt_one_iff, Finset.mem_Icc, Finset.Icc_erase_left]

Result:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Ioc 1 n, (↑x)⁻¹ ≤ Real.log ↑n

Proof state:
case pos
n : ℕ
hn0 : n = 0
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Tactic:
simp [hn0]

Result:
no goals

Proof state:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 + ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + Real.log ↑n

Tactic:
refine add_le_add_left ?_ 1

Result:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ Real.log ↑n

Proof state:
case neg.calc_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑d)⁻¹ = ∑ d ∈ Finset.Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹

Tactic:
simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]

Result:
no goals

Proof state:
n : ℕ
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Tactic:
by_cases hn0 : n = 0

Result:
case pos
n : ℕ
hn0 : n = 0
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

case neg
n : ℕ
hn0 : ¬n = 0
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Proof state:
case neg.calc_4
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1 ..↑n, x⁻¹ = Real.log ↑n

Tactic:
convert integral_inv _

Result:
case h.e'_3.h.e'_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑n / 1

case neg.calc_4.convert_3
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc 1 ↑n

Proof state:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 2 ≤ n + 1

Tactic:
linarith [hn]

Result:
no goals

Proof state:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Ioc 1 n, (↑x)⁻¹ ≤ Real.log ↑n

Tactic:
calc ∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
  _ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
  _ ≤ ∫ x in (2).. ↑(n + 1), (x - 1)⁻¹  := ?_
  _ = ∫ x in (1)..n, x⁻¹ := ?_
  _ = Real.log ↑n := ?_

Result:
case neg.calc_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑d)⁻¹ = ∑ d ∈ Finset.Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹

case neg.calc_2
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ ≤ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹

case neg.calc_3
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹ = ∫ (x : ℝ) in 1 ..↑n, x⁻¹

case neg.calc_4
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1 ..↑n, x⁻¹ = Real.log ↑n

Proof state:
case neg.calc_4.convert_3
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc 1 ↑n

Tactic:
simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg,
  and_true, not_le, zero_lt_one]

Result:
no goals

Proof state:
case neg.calc_3
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹ = ∫ (x : ℝ) in 1 ..↑n, x⁻¹

Tactic:
convert intervalIntegral.integral_comp_sub_right _ 1

Result:
case h.e'_3.h.e'_5
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 = 2 - 1

case h.e'_3.h.e'_6
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑(n + 1) - 1

Proof state:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 < ↑2

Tactic:
norm_num

Result:
no goals

Proof state:
case neg
n : ℕ
hn0 : ¬n = 0
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Tactic:
have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0

Result:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Proof state:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Tactic:
simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Result:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Icc 1 n, (↑x)⁻¹ ≤ 1 + Real.log ↑n

Proof state:
case h.e'_3.h.e'_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑n / 1

Tactic:
rw [div_one]

Result:
no goals

Proof state:
case h.e'_3.h.e'_6
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑(n + 1) - 1

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]

Result:
no goals