Theorem: MvPowerSeries.StronglySummable.sum_add (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
⊢ ⋯.sum = hf.sum + hg.sum
Tactic:
classical
ext d
simp only [coeff_sum, Pi.add_apply, map_add]
rw [coeff_sum d (support_add hf hg d), coeff_sum d, coeff_sum d]
simp only [Pi.add_apply, map_add, Finset.union_assoc]
rw [sum_add_distrib]
all_goals
  simp only [coe_union, Finite.coe_toFinset, Set.subset_union_right, Set.subset_union_left]
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
⊢ ⋯.sum = 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
d : σ →₀ ℕ
⊢ (coeff α d) ⋯.sum = (coeff α d) (hf.sum + 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
d : σ →₀ ℕ
⊢ (coeff α d) ⋯.sum = (coeff α d) (hf.sum + hg.sum)
Tactic:
simp only [coeff_sum, Pi.add_apply, map_add]
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
d : σ →₀ ℕ
⊢ (coeff α d) ⋯.sum = (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
d : σ →₀ ℕ
⊢ (coeff α d) ⋯.sum = (coeff α d) hf.sum + (coeff α d) hg.sum
Tactic:
rw [coeff_sum d (support_add hf hg d), coeff_sum d, coeff_sum 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
d : σ →₀ ℕ
⊢ ∑ i ∈ ⋯.toFinset ∪ ⋯.toFinset, (coeff α d) ((f + g) i) =
    ∑ i ∈ ?m.48819, (coeff α d) (f i) + ∑ i ∈ ?m.48941, (coeff α d) (g i)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.48941

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑?m.48819

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

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
d : σ →₀ ℕ
⊢ ∑ i ∈ ⋯.toFinset ∪ ⋯.toFinset, (coeff α d) ((f + g) i) =
    ∑ i ∈ ?m.48819, (coeff α d) (f i) + ∑ i ∈ ?m.48941, (coeff α d) (g i)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.48941

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑?m.48819

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι
Tactic:
simp only [Pi.add_apply, map_add, Finset.union_assoc]
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
d : σ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset ∪ ⋯.toFinset, ((coeff α d) (f x) + (coeff α d) (g x)) =
    ∑ i ∈ ?m.48819, (coeff α d) (f i) + ∑ i ∈ ?m.48941, (coeff α d) (g i)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.48941

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑?m.48819

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

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
d : σ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset ∪ ⋯.toFinset, ((coeff α d) (f x) + (coeff α d) (g x)) =
    ∑ i ∈ ?m.48819, (coeff α d) (f i) + ∑ i ∈ ?m.48941, (coeff α d) (g i)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.48941

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑?m.48819

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ Finset ι
Tactic:
rw [sum_add_distrib]
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
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑(⋯.toFinset ∪ ⋯.toFinset)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑(⋯.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
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑(⋯.toFinset ∪ ⋯.toFinset)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑(⋯.toFinset ∪ ⋯.toFinset)
Tactic:
all_goals
  simp only [coe_union, Finite.coe_toFinset, Set.subset_union_right, Set.subset_union_left]
State after:
no goals

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
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑(⋯.toFinset ∪ ⋯.toFinset)
Tactic:
simp only [coe_union, Finite.coe_toFinset, Set.subset_union_right, Set.subset_union_left]
State after:
no goals