Theorem: MvPowerSeries.as_sum_of_homogeneous_components' (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ ∀ (hf : StronglySummable fun p => (homogeneousComponent w p) f), f = hf.sum
Tactic:
intro hf
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
⊢ f = hf.sum

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
⊢ f = hf.sum
Tactic:
ext d
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) hf.sum

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) hf.sum
Tactic:
simp_rw [coeff_apply, StronglySummable.sum, coeff_homogeneousComponent]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = ∑ i ∈ ⋯.toFinset, if (weight w) d = i then (coeff α d) f else 0

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = ∑ i ∈ ⋯.toFinset, if (weight w) d = i then (coeff α d) f else 0
Tactic:
rw [sum_eq_single (weight w d)]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = if (weight w) d = (weight w) d then (coeff α d) f else 0

case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then (coeff α d) f else 0) = 0

case h.h₁
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then (coeff α d) f else 0) = 0

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = if (weight w) d = (weight w) d then (coeff α d) f else 0
Tactic:
simp only [eq_self_iff_true, if_true]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = (coeff α d) f

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = (coeff α d) f
Tactic:
rfl
State after:
no goals

State before:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then (coeff α d) f else 0) = 0
Tactic:
intro b _ h'
State after:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
b : ℕ
a✝ : b ∈ ⋯.toFinset
h' : b ≠ (weight w) d
⊢ (if (weight w) d = b then (coeff α d) f else 0) = 0

State before:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
b : ℕ
a✝ : b ∈ ⋯.toFinset
h' : b ≠ (weight w) d
⊢ (if (weight w) d = b then (coeff α d) f else 0) = 0
Tactic:
rw [if_neg (Ne.symm h')]
State after:
no goals

State before:
case h.h₁
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then (coeff α d) f else 0) = 0
Tactic:
simp only [Finite.mem_toFinset, Function.mem_support, Classical.not_not, imp_self]
State after:
no goals