l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * exp (↑b₁ * z) = z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z => z ^ a₁ * exp (↑b₁ * z)) z = (fun z => z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)) z
simp only
no goals
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * exp (↑b₁ * z) = z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)
rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel'_right]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₁ * z) * exp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel'_right]
no goals
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
norm_cast