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

State before:
f : ℕ → ℂ
p : ℕ
h : ProdExists f
⊢ tprod f ^ p = ∏' (n : ℕ), f n ^ p
Tactic:
rcases h with ⟨g, h⟩
State after:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ tprod f ^ p = ∏' (n : ℕ), f n ^ p

State before:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ tprod f ^ p = ∏' (n : ℕ), f n ^ p
Tactic:
rw [HasProd.tprod_eq h]
State after:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ g ^ p = ∏' (n : ℕ), f n ^ p

State before:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ g ^ p = ∏' (n : ℕ), f n ^ p
Tactic:
rw [HasProd.tprod_eq _]
State after:
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f n ^ p) (g ^ p)

State before:
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f n ^ p) (g ^ p)
Tactic:
exact product_pow p h
State after:
no goals