Theorem: product_pow (Ray/Analytic/Products.lean)

State before:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ HasProd (fun n => f n ^ p) (g ^ p)
Tactic:
rw [HasProd]
State after:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => s.prod fun b => f b ^ p) atTop (𝓝 (g ^ p))

State before:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => s.prod fun b => f b ^ p) atTop (𝓝 (g ^ p))
Tactic:
simp_rw [Finset.prod_pow]
State after:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => (s.prod fun x => f x) ^ p) atTop (𝓝 (g ^ p))

State before:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => (s.prod fun x => f x) ^ p) atTop (𝓝 (g ^ p))
Tactic:
exact Filter.Tendsto.comp (Continuous.tendsto (continuous_pow p) g) h
State after:
no goals