Theorem: pp_pos (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < pp a x
Tactic:
simp [pp]
State after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Tactic:
have : 0 < 1 - a := by linarith [ha.2]
State after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this : 0 < 1 - a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this : 0 < 1 - a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Tactic:
have : 0 < 1 + a := by linarith [ha.1]
State after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this✝ : 0 < 1 - a
this : 0 < 1 + a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this✝ : 0 < 1 - a
this : 0 < 1 + a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < 1 - a
Tactic:
linarith [ha.2]
State after:
no goals

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