Theorem: log_add_one_sub_log_le (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
have l1 : ContinuousOn Real.log (Icc x (x + 1)) := by
  apply continuousOn_log.mono ; intro t ⟨h1, _⟩ ; simp ; linarith
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
⊢ nabla Real.log x ≤ x⁻¹

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
have l2 t (ht : t ∈ Ioo x (x + 1)) : HasDerivAt Real.log t⁻¹ t := Real.hasDerivAt_log (by linarith [ht.1])
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
⊢ nabla Real.log x ≤ x⁻¹

State before:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
htx : t⁻¹ = ((x + 1).log - x.log) / (x + 1 - x)
ht1 : x < t
right✝ : t < x + 1
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
simp at htx
State after:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ nabla Real.log x ≤ x⁻¹

State before:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
rw [nabla, ← htx, inv_le_inv (by linarith) hx]
State after:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ x ≤ t

State before:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ x ≤ t
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ ContinuousOn Real.log (Icc x (x + 1))
Tactic:
apply continuousOn_log.mono
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ Icc x (x + 1) ⊆ {0}ᶜ

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ Icc x (x + 1) ⊆ {0}ᶜ
Tactic:
intro t ⟨h1, _⟩
State after:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ t ∈ {0}ᶜ

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ t ∈ {0}ᶜ
Tactic:
simp
State after:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ ¬t = 0

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ ¬t = 0
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
t : ℝ
ht : t ∈ Ioo x (x + 1)
⊢ t ≠ 0
Tactic:
linarith [ht.1]
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
⊢ x < x + 1
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ 0 < t
Tactic:
linarith
State after:
no goals