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

State before:
f : ℕ → ℂ
f0 : f 0 ≠ 0
h : ProdExists f
⊢ ∏' (n : ℕ), f (n + 1) = tprod f / f 0
Tactic:
rcases h with ⟨g, h⟩
State after:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = tprod f / f 0

State before:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = tprod f / f 0
Tactic:
rw [HasProd.tprod_eq h]
State after:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = g / f 0

State before:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = g / f 0
Tactic:
rw [HasProd.tprod_eq _]
State after:
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f (n + 1)) (g / f 0)

State before:
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Tactic:
exact product_drop f0 h
State after:
no goals