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

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
State after:
no goals

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
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)

State before:
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)
Tactic:
simp_rw [coeff_sum d (support_mul hf hg d), coeff_mul]
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 : σ →₀ ℕ
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      ∑ p ∈ antidiagonal d, (coeff α p.1) (f x.1) * (coeff α p.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum

State before:
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 : σ →₀ ℕ
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      ∑ p ∈ antidiagonal d, (coeff α p.1) (f x.1) * (coeff α p.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum
Tactic:
rw [sum_comm]
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 : σ →₀ ℕ
⊢ ∑ y ∈ antidiagonal d,
      ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α y.1) (f x.1) * (coeff α y.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum

State before:
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 : σ →₀ ℕ
⊢ ∑ y ∈ antidiagonal d,
      ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α y.1) (f x.1) * (coeff α y.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum
Tactic:
apply Finset.sum_congr rfl
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 : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    ∑ x_1 ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α x.1) (f x_1.1) * (coeff α x.2) (g x_1.2) =
      (coeff α x.1) hf.sum * (coeff α x.2) hg.sum

State before:
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 : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    ∑ x_1 ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α x.1) (f x_1.1) * (coeff α x.2) (g x_1.2) =
      (coeff α x.1) hf.sum * (coeff α x.2) hg.sum
Tactic:
rintro bc hbc
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      (coeff α bc.1) (f x.1) * (coeff α bc.2) (g x.2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum

State before:
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      (coeff α bc.1) (f x.1) * (coeff α bc.2) (g x.2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum
Tactic:
erw [Finset.sum_product]
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset,
      ∑ y ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset, (coeff α bc.1) (f (x, y).1) * (coeff α bc.2) (g (x, y).2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum

State before:
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset,
      ∑ y ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset, (coeff α bc.1) (f (x, y).1) * (coeff α bc.2) (g (x, y).2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum
Tactic:
rw [coeff_sum _, coeff_sum _, sum_mul_sum]
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.2) (g i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)

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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.1) (f i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)

State before:
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.2) (g i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)

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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.1) (f i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Tactic:
all_goals
  intro x hx
  apply @Finset.subset_biUnion_of_mem _ _ _ _ _ bc hbc
  exact (Finite.mem_toFinset _).mpr hx
State after:
no goals

State before:
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.1) (f i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Tactic:
intro x hx
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)

State before:
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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Tactic:
apply @Finset.subset_biUnion_of_mem _ _ _ _ _ bc hbc
State after:
case h.a
σ : 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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ⋯.toFinset

State before:
case h.a
σ : 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 : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ⋯.toFinset
Tactic:
exact (Finite.mem_toFinset _).mpr hx
State after:
no goals