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

State before:
a g : ℂ
f : ℕ → ℂ
h : HasProd f g
⊢ HasProd (Stream'.cons a f) (a * g)
Tactic:
rw [HasProd] at h ⊢
State after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))

State before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_mul_left a) g) h
State after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))

State before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
have s : ((fun z ↦ a * z) ∘ fun N : Finset ℕ ↦ N.prod f) =
    (fun N : Finset ℕ ↦ N.prod (Stream'.cons a f)) ∘ push := by
  apply funext; intro N; simp; exact push_prod
State after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))

State before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
rw [s] at ha
State after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.prod (Stream'.cons a f)) ∘ push) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))

State before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.prod (Stream'.cons a f)) ∘ push) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
exact tendsto_comp_push.mp ha
State after:
no goals

State before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
Tactic:
apply funext
State after:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ ∀ (x : Finset ℕ), ((fun z => a * z) ∘ fun N => N.prod f) x = ((fun N => N.prod (Stream'.cons a f)) ∘ push) x

State before:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ ∀ (x : Finset ℕ), ((fun z => a * z) ∘ fun N => N.prod f) x = ((fun N => N.prod (Stream'.cons a f)) ∘ push) x
Tactic:
intro N
State after:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ ((fun z => a * z) ∘ fun N => N.prod f) N = ((fun N => N.prod (Stream'.cons a f)) ∘ push) N

State before:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ ((fun z => a * z) ∘ fun N => N.prod f) N = ((fun N => N.prod (Stream'.cons a f)) ∘ push) N
Tactic:
simp
State after:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ a * N.prod f = (push N).prod (Stream'.cons a f)

State before:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ a * N.prod f = (push N).prod (Stream'.cons a f)
Tactic:
exact push_prod
State after:
no goals