Theorem: one_div_sub_one (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n : ℕ
⊢ 1 / ↑(n - 1) ≤ 2 / ↑n
Tactic:
match n with
| 0 => simp
| 1 => simp
| n + 2 => { norm_cast ; rw [div_le_div_iff] <;> simp [mul_add] <;> linarith }
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n : ℕ
⊢ 1 / ↑(0 - 1) ≤ 2 / ↑0
Tactic:
simp
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n : ℕ
⊢ 1 / ↑(1 - 1) ≤ 2 / ↑1
Tactic:
simp
State after:
no goals

State before:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n✝ n : ℕ
⊢ 1 / ↑(n + 2 - 1) ≤ 2 / ↑(n + 2)
Tactic:
rw [div_le_div_iff] <;> simp [mul_add] <;> linarith
State after:
no goals