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

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

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

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (homogeneousComponent w i) f d) (f d)
Tactic:
have hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0 := by
  intro p h
  rw [← coeff_apply (homogeneousComponent w p f) d, coeff_homogeneousComponent,
    if_neg (Ne.symm h)]
State after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ HasSum (fun i => (homogeneousComponent w i) f d) (f d)

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

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

State before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : p ≠ (weight w) d
⊢ (homogeneousComponent w p) f d = 0
Tactic:
rw [← coeff_apply (homogeneousComponent w p f) d, coeff_homogeneousComponent,
  if_neg (Ne.symm h)]
State after:
no goals

State before:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ f d = (homogeneousComponent w ((weight w) d)) f d
Tactic:
rw [← coeff_apply f d, ← coeff_apply (homogeneousComponent w (weight w d) f) d,
  coeff_homogeneousComponent]
State after:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ (coeff α d) f = if (weight w) d = (weight w) d then (coeff α d) f else 0

State before:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ (coeff α d) f = if (weight w) d = (weight w) d then (coeff α d) f else 0
Tactic:
simp only [eq_self_iff_true, if_true]
State after:
no goals