-- Mathlib/RingTheory/PowerSeries/PiTopology.lean
theorem hasSum_of_monomials_self (f : PowerSeries R) :
    HasSum (fun d : ℕ => monomial R d (coeff R d f)) f

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

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

Tactic:
all_goals { ext; simp }

Result:
no goals

Proof state:
case h.e'_5.h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ ((fun d => (monomial R d) ((coeff R d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) x✝ =
    (MvPowerSeries.monomial R x✝) ((MvPowerSeries.coeff R x✝) f)

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

Result:
case h.e'_5.h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ (MvPowerSeries.monomial R (Finsupp.single () (x✝ PUnit.unit)))
      ((MvPowerSeries.coeff R (Finsupp.single () (x✝ PUnit.unit))) f) =
    (MvPowerSeries.monomial R x✝) ((MvPowerSeries.coeff R x✝) f)

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

Tactic:
simp

Result:
no goals

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

Tactic:
ext

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

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum (fun d => (monomial R d) ((coeff R d) f)) f

Tactic:
rw [← (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.hasSum_iff]

Result:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum ((fun d => (monomial R d) ((coeff R d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) f

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum ((fun d => (monomial R d) ((coeff R d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) f

Tactic:
convert MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f

Result:
case h.e'_5.h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ ((fun d => (monomial R d) ((coeff R d) f)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) x✝ =
    (MvPowerSeries.monomial R x✝) ((MvPowerSeries.coeff R x✝) f)

Proof state:
case h.e'_5.h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ (MvPowerSeries.monomial R (Finsupp.single () (x✝ PUnit.unit)))
      ((MvPowerSeries.coeff R (Finsupp.single () (x✝ PUnit.unit))) f) =
    (MvPowerSeries.monomial R x✝) ((MvPowerSeries.coeff R x✝) f)

Tactic:
congr

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

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