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

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Tactic:
have c := @product_cons (f 0)⁻¹ _ _ h
State after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ HasProd (fun n => f (n + 1)) (g / f 0)

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Tactic:
rw [HasProd]
State after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
rw [inv_mul_eq_div, HasProd, ← tendsto_comp_push, ← tendsto_comp_push] at c
State after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
have s : ((fun N : Finset ℕ ↦ N.prod fun n ↦ (Stream'.cons (f 0)⁻¹ f) n) ∘ push) ∘ push =
    fun N : Finset ℕ ↦ N.prod fun n ↦ f (n + 1) := by
  clear c h g; apply funext; intro N; simp
  nth_rw 2 [← Stream'.eta f]
  simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel f0,
    one_mul]
State after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
rw [s] at c
State after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (fun N => N.prod fun n => f (n + 1)) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (fun N => N.prod fun n => f (n + 1)) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
assumption
State after:
no goals

State before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
⊢ ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
Tactic:
clear c h g
State after:
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)

State before:
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
Tactic:
apply funext
State after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ∀ (x : Finset ℕ), (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) x = x.prod fun n => f (n + 1)

State before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ∀ (x : Finset ℕ), (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) x = x.prod fun n => f (n + 1)
Tactic:
intro N
State after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) N = N.prod fun n => f (n + 1)

State before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) N = N.prod fun n => f (n + 1)
Tactic:
simp
State after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ f n) = N.prod fun n => f (n + 1)

State before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ f n) = N.prod fun n => f (n + 1)
Tactic:
nth_rw 2 [← Stream'.eta f]
State after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.prod fun n => f (n + 1)

State before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.prod fun n => f (n + 1)
Tactic:
simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel f0,
  one_mul]
State after:
no goals