Theorem: Aux.log_add_one_le_sum_inv (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
n : ℕ
⊢ (↑(n + 1)).log ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹
Tactic:
calc _ = ∫ x in (1)..↑(n+1), x⁻¹ := ?_
     _ = ∫ x in (1:ℕ)..↑(n+1), x⁻¹ := ?_
     _ ≤ _ := ?_
State after:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹

case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹ = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹

case calc_3
n : ℕ
⊢ ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹

State before:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹
Tactic:
rw[integral_inv (by simp[(show ¬ (1:ℝ) ≤ 0 by norm_num)] )]
State after:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = (↑(n + 1) / 1).log

State before:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = (↑(n + 1) / 1).log
Tactic:
congr
State after:
case calc_1.e_x
n : ℕ
⊢ ↑(n + 1) = ↑(n + 1) / 1

State before:
case calc_1.e_x
n : ℕ
⊢ ↑(n + 1) = ↑(n + 1) / 1
Tactic:
ring
State after:
no goals

State before:
n : ℕ
⊢ 0 ∉ Set.uIcc 1 ↑(n + 1)
Tactic:
simp[(show ¬ (1:ℝ) ≤ 0 by norm_num)]
State after:
no goals

State before:
n : ℕ
⊢ ¬1 ≤ 0
Tactic:
norm_num
State after:
no goals

State before:
case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹ = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹
Tactic:
congr
State after:
case calc_2.e_a
n : ℕ
⊢ 1 = ↑1

State before:
case calc_2.e_a
n : ℕ
⊢ 1 = ↑1
Tactic:
norm_num
State after:
no goals

State before:
case calc_3
n : ℕ
⊢ ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹
Tactic:
apply AntitoneOn.integral_le_sum_Ico (by norm_num)
State after:
case calc_3
n : ℕ
⊢ AntitoneOn (fun x => x⁻¹) (Set.Icc ↑1 ↑(n + 1))

State before:
case calc_3
n : ℕ
⊢ AntitoneOn (fun x => x⁻¹) (Set.Icc ↑1 ↑(n + 1))
Tactic:
apply inv_antitoneOn_Icc
State after:
case calc_3.ha
n : ℕ
⊢ 0 < ↑1

State before:
case calc_3.ha
n : ℕ
⊢ 0 < ↑1
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
⊢ 1 ≤ n + 1
Tactic:
norm_num
State after:
no goals