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

State before:
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Icc 1 n, (↑d)⁻¹ ≤ 1 + (↑n).log
Tactic:
rw [← Finset.sum_erase_add (Icc 1 n) _ (by simp [hn] : 1 ∈ Icc 1 n), add_comm]
State after:
n : ℕ
hn : 1 ≤ n
⊢ (↑1)⁻¹ + ∑ x ∈ (Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + (↑n).log

State before:
n : ℕ
hn : 1 ≤ n
⊢ (↑1)⁻¹ + ∑ x ∈ (Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + (↑n).log
Tactic:
gcongr
State after:
case h₁
n : ℕ
hn : 1 ≤ n
⊢ (↑1)⁻¹ ≤ 1

case h₂
n : ℕ
hn : 1 ≤ n
⊢ ∑ x ∈ (Icc 1 n).erase 1, (↑x)⁻¹ ≤ (↑n).log

State before:
case h₂
n : ℕ
hn : 1 ≤ n
⊢ ∑ x ∈ (Icc 1 n).erase 1, (↑x)⁻¹ ≤ (↑n).log
Tactic:
simp only [gt_iff_lt, lt_one_iff, mem_Icc, true_and, not_le, Icc_erase_left]
State after:
case h₂
n : ℕ
hn : 1 ≤ n
⊢ ∑ x ∈ Ioc 1 n, (↑x)⁻¹ ≤ (↑n).log

State before:
case h₂
n : ℕ
hn : 1 ≤ n
⊢ ∑ x ∈ Ioc 1 n, (↑x)⁻¹ ≤ (↑n).log
Tactic:
calc
  ∑ d : ℕ in Ico 2 (n + 1), (d : ℝ)⁻¹ = ∑ d in Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
  _ ≤ ∫ x in (2).. ↑(n + 1), (x - 1)⁻¹  := ?_
  _ = Real.log ↑n := ?_
State after:
case h₂.calc_1
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Ico 2 (n + 1), (↑d)⁻¹ = ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹

case h₂.calc_2
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ ≤ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹

case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹ = (↑n).log

State before:
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹ = (↑n).log
Tactic:
rw [intervalIntegral.integral_comp_sub_right _ 1, integral_inv]
State after:
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ((↑(n + 1) - 1) / (2 - 1)).log = (↑n).log

case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc (2 - 1) (↑(n + 1) - 1)

State before:
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc (2 - 1) (↑(n + 1) - 1)
Tactic:
norm_num
State after:
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc 1 ↑n

State before:
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc 1 ↑n
Tactic:
simp[hn, show (0:ℝ) < 1 by norm_num]
State after:
no goals

State before:
n : ℕ
hn : 1 ≤ n
⊢ 1 ∈ Icc 1 n
Tactic:
simp [hn]
State after:
no goals

State before:
case h₁
n : ℕ
hn : 1 ≤ n
⊢ (↑1)⁻¹ ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
case h₂.calc_1
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Ico 2 (n + 1), (↑d)⁻¹ = ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹
Tactic:
congr
State after:
case h₂.calc_1.e_f
n : ℕ
hn : 1 ≤ n
⊢ (fun d => (↑d)⁻¹) = fun d => (↑(d + 1) - 1)⁻¹

State before:
case h₂.calc_1.e_f
n : ℕ
hn : 1 ≤ n
⊢ (fun d => (↑d)⁻¹) = fun d => (↑(d + 1) - 1)⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case h₂.calc_2
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ ≤ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹
Tactic:
apply @AntitoneOn.sum_le_integral_Ico 2 (n + 1) fun x : ℝ => (x - 1)⁻¹
State after:
case h₂.calc_2.hab
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ n + 1

case h₂.calc_2.hf
n : ℕ
hn : 1 ≤ n
⊢ AntitoneOn (fun x => (x - 1)⁻¹) (Set.Icc ↑2 ↑(n + 1))

State before:
case h₂.calc_2.hf
n : ℕ
hn : 1 ≤ n
⊢ AntitoneOn (fun x => (x - 1)⁻¹) (Set.Icc ↑2 ↑(n + 1))
Tactic:
apply inv_sub_antitoneOn_Icc
State after:
case h₂.calc_2.hf.ha
n : ℕ
hn : 1 ≤ n
⊢ 1 < ↑2

State before:
case h₂.calc_2.hf.ha
n : ℕ
hn : 1 ≤ n
⊢ 1 < ↑2
Tactic:
norm_num
State after:
no goals

State before:
case h₂.calc_2.hab
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ n + 1
Tactic:
linarith [hn]
State after:
no goals

State before:
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ((↑(n + 1) - 1) / (2 - 1)).log = (↑n).log
Tactic:
norm_num
State after:
no goals

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