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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
⊢ hf.sum = hg.sum
Tactic:
ext d
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) hg.sum

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) hg.sum
Tactic:
simp only [coeff_sum_def]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
⊢ ∑ i ∈ ⋯.toFinset, (coeff α d) (f i) = ∑ i ∈ ⋯.toFinset, (coeff α d) (g i)

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
⊢ ∑ i ∈ ⋯.toFinset, (coeff α d) (f i) = ∑ i ∈ ⋯.toFinset, (coeff α d) (g i)
Tactic:
refine' Finset.sum_congr _ fun i _ => by rw [h]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
⊢ ⋯.toFinset = ⋯.toFinset

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
⊢ ⋯.toFinset = ⋯.toFinset
Tactic:
ext i
State after:
case h.a
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
i : ι
⊢ i ∈ ⋯.toFinset ↔ i ∈ ⋯.toFinset

State before:
case h.a
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
i : ι
⊢ i ∈ ⋯.toFinset ↔ i ∈ ⋯.toFinset
Tactic:
simp only [Finite.mem_toFinset, mem_support, ne_eq, h]
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
h : f = g
d : σ →₀ ℕ
i : ι
x✝ : i ∈ ⋯.toFinset
⊢ (coeff α d) (f i) = (coeff α d) (g i)
Tactic:
rw [h]
State after:
no goals