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

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
⊢ HasSum (fun d => (monomial α d) ((coeff α d) f)) f
Tactic:
rw [Pi.hasSum]
State after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (monomial α i) ((coeff α i) f) x) (f x)

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (monomial α i) ((coeff α i) f) x) (f x)
Tactic:
intro d
State after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)
Tactic:
have hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0 := by
  intro d' h
  change coeff α d ((monomial α d') ((coeff α d') f)) = 0
  rw [coeff_monomial_ne (Ne.symm h)]
State after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)
Tactic:
convert hasSum_single d hd using 1
State after:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ f d = (monomial α d) ((coeff α d) f) d

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
Tactic:
intro d' h
State after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (monomial α d') ((coeff α d') f) d = 0

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (monomial α d') ((coeff α d') f) d = 0
Tactic:
change coeff α d ((monomial α d') ((coeff α d') f)) = 0
State after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (coeff α d) ((monomial α d') ((coeff α d') f)) = 0

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (coeff α d) ((monomial α d') ((coeff α d') f)) = 0
Tactic:
rw [coeff_monomial_ne (Ne.symm h)]
State after:
no goals

State before:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ f d = (monomial α d) ((coeff α d) f) d
Tactic:
rw [← coeff_apply f d, ← coeff_apply (monomial α d (coeff α d f)) d, coeff_apply,
  coeff_monomial_same]
State after:
no goals