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

State before:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ HasProd f 0
Tactic:
rw [HasProd]
State after:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 0)

State before:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 0)
Tactic:
rw [Metric.tendsto_atTop]
State after:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < ε

State before:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < ε
Tactic:
intro e ep
State after:
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < e

State before:
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < e
Tactic:
use Finset.range 1
State after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∀ n ≥ Finset.range 1, dist (n.prod fun b => f b) 0 < e

State before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∀ n ≥ Finset.range 1, dist (n.prod fun b => f b) 0 < e
Tactic:
intro N N1
State after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : N ≥ Finset.range 1
⊢ dist (N.prod fun b => f b) 0 < e

State before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : N ≥ Finset.range 1
⊢ dist (N.prod fun b => f b) 0 < e
Tactic:
simp at N1
State after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist (N.prod fun b => f b) 0 < e

State before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist (N.prod fun b => f b) 0 < e
Tactic:
rw [Finset.prod_eq_zero N1 f0]
State after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist 0 0 < e

State before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist 0 0 < e
Tactic:
simpa
State after:
no goals