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

State before:
f : ℕ → ℂ
h : ProdExists f
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
by_cases f0 : f 0 = 0
State after:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)

case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)

State before:
case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
rw [product_drop' f0 h]
State after:
case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * (tprod f / f 0)

State before:
case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * (tprod f / f 0)
Tactic:
field_simp
State after:
no goals

State before:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
rw [f0, (product_head_zero f0).tprod_eq]
State after:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ 0 = 0 * ∏' (n : ℕ), f (n + 1)

State before:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ 0 = 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
simp
State after:
no goals