α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (sum (sum f fun i a => a • B i) fun i a => a • A i) = sum f fun i a => a • sum (B i) fun i a => a • A i
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ↑(Finsupp.total α M R A) (↑(Finsupp.total β (α →₀ R) R B) f) =
    ↑(Finsupp.total β M R fun b => ↑(Finsupp.total α M R A) (B b)) f
simp only [total_apply]
case h0
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (sum (sum 0 fun i a => a • B i) fun i a => a • A i) = sum 0 fun i a => a • sum (B i) fun i a => a • A i

case hadd
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (f g : β →₀ R),
    ((sum (sum f fun i a => a • B i) fun i a => a • A i) = sum f fun i a => a • sum (B i) fun i a => a • A i) →
      ((sum (sum g fun i a => a • B i) fun i a => a • A i) = sum g fun i a => a • sum (B i) fun i a => a • A i) →
        (sum (sum (f + g) fun i a => a • B i) fun i a => a • A i) =
          sum (f + g) fun i a => a • sum (B i) fun i a => a • A i

case hsingle
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (a : β) (b : R),
    (sum (sum (single a b) fun i a => a • B i) fun i a => a • A i) =
      sum (single a b) fun i a => a • sum (B i) fun i a => a • A i
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (sum (sum f fun i a => a • B i) fun i a => a • A i) = sum f fun i a => a • sum (B i) fun i a => a • A i
apply induction_linear f
no goals
case h0
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (sum (sum 0 fun i a => a • B i) fun i a => a • A i) = sum 0 fun i a => a • sum (B i) fun i a => a • A i
simp only [sum_zero_index]
case hadd
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
f₁ f₂ : β →₀ R
h₁ : (sum (sum f₁ fun i a => a • B i) fun i a => a • A i) = sum f₁ fun i a => a • sum (B i) fun i a => a • A i
h₂ : (sum (sum f₂ fun i a => a • B i) fun i a => a • A i) = sum f₂ fun i a => a • sum (B i) fun i a => a • A i
⊢ (sum (sum (f₁ + f₂) fun i a => a • B i) fun i a => a • A i) =
    sum (f₁ + f₂) fun i a => a • sum (B i) fun i a => a • A i
case hadd
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (f g : β →₀ R),
    ((sum (sum f fun i a => a • B i) fun i a => a • A i) = sum f fun i a => a • sum (B i) fun i a => a • A i) →
      ((sum (sum g fun i a => a • B i) fun i a => a • A i) = sum g fun i a => a • sum (B i) fun i a => a • A i) →
        (sum (sum (f + g) fun i a => a • B i) fun i a => a • A i) =
          sum (f + g) fun i a => a • sum (B i) fun i a => a • A i
intro f₁ f₂ h₁ h₂
no goals
case hadd
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
f₁ f₂ : β →₀ R
h₁ : (sum (sum f₁ fun i a => a • B i) fun i a => a • A i) = sum f₁ fun i a => a • sum (B i) fun i a => a • A i
h₂ : (sum (sum f₂ fun i a => a • B i) fun i a => a • A i) = sum f₂ fun i a => a • sum (B i) fun i a => a • A i
⊢ (sum (sum (f₁ + f₂) fun i a => a • B i) fun i a => a • A i) =
    sum (f₁ + f₂) fun i a => a • sum (B i) fun i a => a • A i
simp [sum_add_index, h₁, h₂, add_smul]
no goals
case hsingle
α✝ : Type ?u.399000
M : Type u_4
N : Type ?u.399006
P : Type ?u.399009
R : Type u_3
S : Type ?u.399015
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.399107
M' : Type ?u.399110
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α✝ → M
v' : α' → M'
α : Type u_1
β : Type u_2
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (a : β) (b : R),
    (sum (sum (single a b) fun i a => a • B i) fun i a => a • A i) =
      sum (single a b) fun i a => a • sum (B i) fun i a => a • A i
simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]