Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto (DividedPowers/ForMathlib/PowerSeries/Topology.lean)

State before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ Filter.Tendsto f u (nhds g) ↔ ∀ (d : ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]
State after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ),
      Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g))) ↔
    ∀ (d : ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))

State before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ),
      Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g))) ↔
    ∀ (d : ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
apply (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.forall_congr
State after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ ∀ {x : Unit →₀ ℕ},
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α x) (f i)) u (nhds ((MvPowerSeries.coeff α x) g)) ↔
      Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) (f i)) u
        (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) g))

State before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ ∀ {x : Unit →₀ ℕ},
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α x) (f i)) u (nhds ((MvPowerSeries.coeff α x) g)) ↔
      Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) (f i)) u
        (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) g))
Tactic:
intro d
State after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) (f i)) u
      (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) g))

State before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) (f i)) u
      (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) g))
Tactic:
simp only [LinearEquiv.coe_toEquiv, Finsupp.LinearEquiv.finsuppUnique_apply,
  PUnit.default_eq_unit, coeff]
State after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))

State before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))
Tactic:
apply iff_of_eq
State after:
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) =
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))

State before:
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) =
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))
Tactic:
congr
State after:
case a.e_f
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i => (MvPowerSeries.coeff α d) (f i)) = fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)

State before:
case a.e_f
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i => (MvPowerSeries.coeff α d) (f i)) = fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
ext i
State after:
case a.e_f.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ (MvPowerSeries.coeff α d) (f i) = (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)

State before:
case a.e_f.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ (MvPowerSeries.coeff α d) (f i) = (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
congr
State after:
case a.e_f.h.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ d = Finsupp.single () (d PUnit.unit)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)

State before:
case a.e_f.h.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ d = Finsupp.single () (d PUnit.unit)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
all_goals { ext; simp }
State after:
no goals

State before:
case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
ext
State after:
case a.e_l₂.e_x.e_a.e_n.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d PUnit.unit)) default

State before:
case a.e_l₂.e_x.e_a.e_n.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d PUnit.unit)) default
Tactic:
simp
State after:
no goals