-- Mathlib/RingTheory/PowerSeries/PiTopology.lean
theorem tendsto_iff_coeff_tendsto [Semiring R] {ι : Type*}
    (f : ι → PowerSeries R) (u : Filter ι) (g : PowerSeries R) :
    Tendsto f u (nhds g) ↔
    ∀ d : ℕ, Tendsto (fun i => coeff R d (f i)) u (nhds (coeff R d g))

Proof state:
case a.e_f.h.e_a.e_n.h
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d default = (Finsupp.single () (d PUnit.unit)) default

Tactic:
simp

Result:
no goals

Proof state:
case a.e_f
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i => (MvPowerSeries.coeff R d) (f i)) = fun i => (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f i)

Tactic:
ext _

Result:
case a.e_f.h
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ (MvPowerSeries.coeff R d) (f x✝) = (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f x✝)

Proof state:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ Tendsto f u (nhds g) ↔ ∀ (d : ℕ), Tendsto (fun i => (coeff R d) (f i)) u (nhds ((coeff R d) g))

Tactic:
rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]

Result:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ), Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g))) ↔
    ∀ (d : ℕ), Tendsto (fun i => (coeff R d) (f i)) u (nhds ((coeff R d) g))

Proof state:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g)) ↔
    Tendsto (fun i => (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) g))

Tactic:
apply iff_of_eq

Result:
case a
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g)) =
    Tendsto (fun i => (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) g))

Proof state:
case a.e_f.h
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ (MvPowerSeries.coeff R d) (f x✝) = (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f x✝)

Tactic:
congr

Result:
case a.e_f.h.e_a.e_n
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d = Finsupp.single () (d PUnit.unit)

Proof state:
case a.e_l₂.e_x.e_a.e_n.h
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d PUnit.unit)) default

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ), Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g))) ↔
    ∀ (d : ℕ), Tendsto (fun i => (coeff R d) (f i)) u (nhds ((coeff R d) g))

Tactic:
apply (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.forall_congr

Result:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ ∀ (a : Unit →₀ ℕ),
    Tendsto (fun i => (MvPowerSeries.coeff R a) (f i)) u (nhds ((MvPowerSeries.coeff R a) g)) ↔
      Tendsto (fun i => (coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv a)) (f i)) u
        (nhds ((coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv a)) g))

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

Tactic:
ext

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

Proof state:
case a
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g)) =
    Tendsto (fun i => (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) g))

Tactic:
congr

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

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

Proof state:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ ∀ (a : Unit →₀ ℕ),
    Tendsto (fun i => (MvPowerSeries.coeff R a) (f i)) u (nhds ((MvPowerSeries.coeff R a) g)) ↔
      Tendsto (fun i => (coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv a)) (f i)) u
        (nhds ((coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv a)) g))

Tactic:
intro d

Result:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g)) ↔
    Tendsto (fun i => (coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) (f i)) u
      (nhds ((coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) g))

Proof state:
case a.e_f.h.e_a.e_n
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d = Finsupp.single () (d PUnit.unit)

Tactic:
ext

Result:
case a.e_f.h.e_a.e_n.h
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d default = (Finsupp.single () (d PUnit.unit)) default

Proof state:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g)) ↔
    Tendsto (fun i => (coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) (f i)) u
      (nhds ((coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) g))

Tactic:
simp only [LinearEquiv.coe_toEquiv, Finsupp.LinearEquiv.finsuppUnique_apply,
  PUnit.default_eq_unit, coeff]

Result:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g)) ↔
    Tendsto (fun i => (MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff R (Finsupp.single () (d PUnit.unit))) g))