Theorem: limiting_cor_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Tactic:
have l1 : ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, x ^ (t * I) = exp (log x * t * I) := by
  filter_upwards [eventually_ne_atTop 0, eventually_ge_atTop 0] with x hx hx' t
  rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr hx), ofReal_log hx'] ; ring_nf
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Tactic:
have l2 : ∀ᶠ x : ℝ in atTop, ∫ t, f t * x ^ (t * I) = ∫ t, f t * exp (log x * t * I) := by
  filter_upwards [l1] with x hx
  refine integral_congr_ae (eventually_of_forall (fun x => by simp [hx]))
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Tactic:
simp_rw [tendsto_congr' l2]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) atTop (𝓝 0)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) atTop (𝓝 0)
Tactic:
convert_to Tendsto (fun x => 𝓕 f (-Real.log x / (2 * π))) atTop (𝓝 0)
State after:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) = fun x => 𝓕 f (-x.log / (2 * π))

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => 𝓕 f (-x.log / (2 * π))) atTop (𝓝 0)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => 𝓕 f (-x.log / (2 * π))) atTop (𝓝 0)
Tactic:
refine (zero_at_infty_fourierIntegral f).comp <| Tendsto.mono_right ?_ _root_.atBot_le_cocompact
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => -x.log / (2 * π)) atTop atBot

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => -x.log / (2 * π)) atTop atBot
Tactic:
exact (tendsto_neg_atBot_iff.mpr tendsto_log_atTop).atBot_mul_const (inv_pos.mpr two_pi_pos)
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
Tactic:
filter_upwards [eventually_ne_atTop 0, eventually_ge_atTop 0] with x hx hx' t
State after:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)

State before:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
Tactic:
rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr hx), ofReal_log hx']
State after:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ cexp ((↑x).log * (↑t * I)) = cexp ((↑x).log * ↑t * I)

State before:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ cexp ((↑x).log * (↑t * I)) = cexp ((↑x).log * ↑t * I)
Tactic:
ring_nf
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
Tactic:
filter_upwards [l1] with x hx
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
x : ℝ
hx : ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
x : ℝ
hx : ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
Tactic:
refine integral_congr_ae (eventually_of_forall (fun x => by simp [hx]))
State after:
no goals

State before:
n : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
x✝ : ℝ
hx : ∀ (t : ℝ), ↑x✝ ^ (↑t * I) = cexp (↑x✝.log * ↑t * I)
x : ℝ
⊢ (fun t => f t * ↑x✝ ^ (↑t * I)) x = (fun t => f t * cexp (↑x✝.log * ↑t * I)) x
Tactic:
simp [hx]
State after:
no goals

State before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) = fun x => 𝓕 f (-x.log / (2 * π))
Tactic:
ext
State after:
case h.e'_3.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ ∫ (t : ℝ), f t * cexp (↑x✝.log * ↑t * I) = 𝓕 f (-x✝.log / (2 * π))

State before:
case h.e'_3.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ ∫ (t : ℝ), f t * cexp (↑x✝.log * ↑t * I) = 𝓕 f (-x✝.log / (2 * π))
Tactic:
congr
State after:
case h.e'_3.h.e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ (fun t => f t * cexp (↑x✝.log * ↑t * I)) = fun v => 𝐞 (-((innerₗ ℝ) v) (-x✝.log / (2 * π))) • f v

State before:
case h.e'_3.h.e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ (fun t => f t * cexp (↑x✝.log * ↑t * I)) = fun v => 𝐞 (-((innerₗ ℝ) v) (-x✝.log / (2 * π))) • f v
Tactic:
ext
State after:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ f x✝ * cexp (↑x✝¹.log * ↑x✝ * I) = 𝐞 (-((innerₗ ℝ) x✝) (-x✝¹.log / (2 * π))) • f x✝

State before:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ f x✝ * cexp (↑x✝¹.log * ↑x✝ * I) = 𝐞 (-((innerₗ ℝ) x✝) (-x✝¹.log / (2 * π))) • f x✝
Tactic:
simp [Real.fourierChar, expMapCircle, mul_comm (f _)]
State after:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)) ∨ f x✝ = 0

State before:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)) ∨ f x✝ = 0
Tactic:
left
State after:
case h.e'_3.h.e_f.h.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I))

State before:
case h.e'_3.h.e_f.h.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I))
Tactic:
congr
State after:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)

State before:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)
Tactic:
rw [← neg_mul]
State after:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π)))) * I

State before:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π)))) * I
Tactic:
congr
State after:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))))

State before:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))))
Tactic:
norm_cast
State after:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = -(2 * π * (x✝ * (-x✝¹.log / (2 * π))))

State before:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = -(2 * π * (x✝ * (-x✝¹.log / (2 * π))))
Tactic:
field_simp
State after:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = x✝ * x✝¹.log

State before:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = x✝ * x✝¹.log
Tactic:
ring
State after:
no goals