-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_linearCombination {α β : Type*} (A : α → M) (B : β → α →₀ R)
    (f : β →₀ R) : linearCombination R A (linearCombination R B f) =
      linearCombination R (fun b => linearCombination R A (B b)) f

Proof state:
case hsingle
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (a : β) (b : R),
    (((single a b).sum fun i a => a • B i).sum fun i a => a • A i) =
      (single a b).sum fun i a => a • (B i).sum fun i a => a • A i

Tactic:
simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Result:
no goals

Proof state:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (linearCombination R A) ((linearCombination R B) f) = (linearCombination R fun b => (linearCombination R A) (B b)) f

Tactic:
simp only [linearCombination_apply]

Result:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ((f.sum fun i a => a • B i).sum fun i a => a • A i) = f.sum fun i a => a • (B i).sum fun i a => a • A i

Proof state:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ((f.sum fun i a => a • B i).sum fun i a => a • A i) = f.sum fun i a => a • (B i).sum fun i a => a • A i

Tactic:
apply induction_linear f

Result:
case h0
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ((sum 0 fun i a => a • B i).sum fun i a => a • A i) = sum 0 fun i a => a • (B i).sum fun i a => a • A i

case hadd
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (f g : β →₀ R),
    (((f.sum fun i a => a • B i).sum fun i a => a • A i) = f.sum fun i a => a • (B i).sum fun i a => a • A i) →
      (((g.sum fun i a => a • B i).sum fun i a => a • A i) = g.sum fun i a => a • (B i).sum fun i a => a • A i) →
        (((f + g).sum fun i a => a • B i).sum fun i a => a • A i) =
          (f + g).sum fun i a => a • (B i).sum fun i a => a • A i

case hsingle
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (a : β) (b : R),
    (((single a b).sum fun i a => a • B i).sum fun i a => a • A i) =
      (single a b).sum fun i a => a • (B i).sum fun i a => a • A i

Proof state:
case hadd
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ∀ (f g : β →₀ R),
    (((f.sum fun i a => a • B i).sum fun i a => a • A i) = f.sum fun i a => a • (B i).sum fun i a => a • A i) →
      (((g.sum fun i a => a • B i).sum fun i a => a • A i) = g.sum fun i a => a • (B i).sum fun i a => a • A i) →
        (((f + g).sum fun i a => a • B i).sum fun i a => a • A i) =
          (f + g).sum fun i a => a • (B i).sum fun i a => a • A i

Tactic:
intro f₁ f₂ h₁ h₂

Result:
case hadd
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
f₁ f₂ : β →₀ R
h₁ : ((f₁.sum fun i a => a • B i).sum fun i a => a • A i) = f₁.sum fun i a => a • (B i).sum fun i a => a • A i
h₂ : ((f₂.sum fun i a => a • B i).sum fun i a => a • A i) = f₂.sum fun i a => a • (B i).sum fun i a => a • A i
⊢ (((f₁ + f₂).sum fun i a => a • B i).sum fun i a => a • A i) =
    (f₁ + f₂).sum fun i a => a • (B i).sum fun i a => a • A i

Proof state:
case h0
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ ((sum 0 fun i a => a • B i).sum fun i a => a • A i) = sum 0 fun i a => a • (B i).sum fun i a => a • A i

Tactic:
simp only [sum_zero_index]

Result:
no goals

Proof state:
case hadd
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
f₁ f₂ : β →₀ R
h₁ : ((f₁.sum fun i a => a • B i).sum fun i a => a • A i) = f₁.sum fun i a => a • (B i).sum fun i a => a • A i
h₂ : ((f₂.sum fun i a => a • B i).sum fun i a => a • A i) = f₂.sum fun i a => a • (B i).sum fun i a => a • A i
⊢ (((f₁ + f₂).sum fun i a => a • B i).sum fun i a => a • A i) =
    (f₁ + f₂).sum fun i a => a • (B i).sum fun i a => a • A i

Tactic:
simp [sum_add_index, h₁, h₂, add_smul]

Result:
no goals