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

State before:
a : ℂ
f : ℕ → ℂ
h : ProdExists f
⊢ tprod (Stream'.cons a f) = a * tprod f
Tactic:
rcases h with ⟨g, h⟩
State after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * tprod f

State before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * tprod f
Tactic:
rw [HasProd.tprod_eq h]
State after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * g

State before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * g
Tactic:
rw [HasProd.tprod_eq _]
State after:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ HasProd (fun b => Stream'.cons a f b) (a * g)

State before:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ HasProd (fun b => Stream'.cons a f b) (a * g)
Tactic:
exact product_cons h
State after:
no goals