Theorem: first_fourier_aux2a (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) = -(↑y * ↑(↑n / x).log)
Tactic:
calc
  _ = -(y * (((2 : ℂ) * π) / (2 * π) * Real.log ((n) / x))) := by ring
  _ = _ := by rw [div_self (by norm_num; exact pi_ne_zero), one_mul]
State after:
no goals

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

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ -(↑y * (2 * ↑π / (2 * ↑π) * ↑(↑n / x).log)) = -(↑y * ↑(↑n / x).log)
Tactic:
rw [div_self (by norm_num; exact pi_ne_zero), one_mul]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 * ↑π ≠ 0
Tactic:
norm_num
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ¬π = 0

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ¬π = 0
Tactic:
exact pi_ne_zero
State after:
no goals