internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.StronglySummable.coeff_sum
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
i : ι
a✝ : i ∈ s
hi' : i ∉ ⋯.toFinset
⊢ (coeff α d) (f i) = 0
Tactic:
simpa only [Finite.mem_toFinset, Function.mem_support, Classical.not_not] using hi'
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_congr
Proof 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
Proof 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
Theorem: MvPowerSeries.StronglySummable.sum_congr
Proof 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]
Proof 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)
Theorem: MvPowerSeries.StronglySummable.sum_congr
Proof 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]
Proof 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
Theorem: MvPowerSeries.StronglySummable.sum_congr
Proof 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
Proof 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
Theorem: MvPowerSeries.StronglySummable.sum_congr
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_congr
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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
Proof 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)
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof 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
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof 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 ι
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof 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 ι
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof 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)
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_add
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable (f + g)
⊢ hh.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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable (f + g)
⊢ hh.sum = hf.sum + hg.sum
Tactic:
ext d
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (coeff α d) hh.sum = (coeff α d) (hf.sum + hg.sum)
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (coeff α d) hh.sum = (coeff α d) (hf.sum + hg.sum)
Tactic:
simp only [coeff_sum, Pi.add_apply, map_add]
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (coeff α d) hh.sum = (coeff α d) hf.sum + (coeff α d) hg.sum
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (coeff α d) hh.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]
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ ∑ i ∈ ⋯.toFinset ∪ ⋯.toFinset, (coeff α d) ((f + g) i) =
    ∑ i ∈ ?m.52863, (coeff α d) (f i) + ∑ i ∈ ?m.52985, (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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.52985

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

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ Finset ι
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ ∑ i ∈ ⋯.toFinset ∪ ⋯.toFinset, (coeff α d) ((f + g) i) =
    ∑ i ∈ ?m.52863, (coeff α d) (f i) + ∑ i ∈ ?m.52985, (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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.52985

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

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

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

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ Finset ι
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset ∪ ⋯.toFinset, ((coeff α d) (f x) + (coeff α d) (g x)) =
    ∑ i ∈ ?m.52863, (coeff α d) (f i) + ∑ i ∈ ?m.52985, (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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (g i)) ⊆ ↑?m.52985

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

σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ Finset ι
Tactic:
rw [sum_add_distrib]
Proof 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
hh : StronglySummable (f + 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
hh : StronglySummable (f + g)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)) ⊆ ↑(⋯.toFinset ∪ ⋯.toFinset)
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof 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
hh : StronglySummable (f + 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
hh : StronglySummable (f + 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_add'
Proof 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
hh : StronglySummable (f + 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]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ ⋯.sum = hf.sum * hg.sum
Tactic:
classical
ext d
simp_rw [coeff_sum d (support_mul hf hg d), coeff_mul]
rw [sum_comm]
apply Finset.sum_congr rfl
rintro bc hbc
erw [Finset.sum_product]
rw [coeff_sum _, coeff_sum _, sum_mul_sum]
all_goals
  intro x hx
  apply @Finset.subset_biUnion_of_mem _ _ _ _ _ bc hbc
  exact (Finite.mem_toFinset _).mpr hx
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ ⋯.sum = hf.sum * hg.sum
Tactic:
ext d
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (coeff α d) ⋯.sum = (coeff α d) (hf.sum * hg.sum)