Theorem: PowerSeries.hasSum_of_monomials_self (DividedPowers/ForMathlib/PowerSeries/Topology.lean)

State before:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
⊢ HasSum (fun d => (monomial α d) ((coeff α d) f)) f
Tactic:
rw [← (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.hasSum_iff]
State after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
⊢ HasSum ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) f

State before:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
⊢ HasSum ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) f
Tactic:
convert MvPowerSeries.hasSum_of_monomials_self f
State after:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) x✝ =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)

State before:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ ((fun d => (monomial α d) ((coeff α d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) x✝ =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)
Tactic:
simp only [LinearEquiv.coe_toEquiv, comp_apply, monomial, coeff,
  Finsupp.LinearEquiv.finsuppUnique_apply, PUnit.default_eq_unit]
State after:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (MvPowerSeries.monomial α (Finsupp.single () (x✝ PUnit.unit)))
      ((MvPowerSeries.coeff α (Finsupp.single () (x✝ PUnit.unit))) f) =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)

State before:
case h.e'_5.h.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (MvPowerSeries.monomial α (Finsupp.single () (x✝ PUnit.unit)))
      ((MvPowerSeries.coeff α (Finsupp.single () (x✝ PUnit.unit))) f) =
    (MvPowerSeries.monomial α x✝) ((MvPowerSeries.coeff α x✝) f)
Tactic:
congr
State after:
case h.e'_5.h.h.h.e_5.h.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝

case h.e'_5.h.h.h.e_6.h.e_a.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝

State before:
case h.e'_5.h.h.h.e_5.h.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝

case h.e'_5.h.h.h.e_6.h.e_a.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝
Tactic:
all_goals { ext ; simp }
State after:
no goals

State before:
case h.e'_5.h.h.h.e_6.h.e_a.e_n
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () (x✝ PUnit.unit) = x✝
Tactic:
ext
State after:
case h.e'_5.h.h.h.e_6.h.e_a.e_n.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () (x✝ PUnit.unit)) default = x✝ default

State before:
case h.e'_5.h.h.h.e_6.h.e_a.e_n.h
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : α⟦X⟧
e_1✝ : α⟦X⟧ = MvPowerSeries Unit α
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () (x✝ PUnit.unit)) default = x✝ default
Tactic:
simp
State after:
no goals