-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁_1 a₂_1 : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ j_1 : n,
      HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
a₁ :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A) i x) *
        HSMul.hSMul (β := A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A) x j)
a₂ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HSMul.hSMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
a₃ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
a₄ :
  Eq.{u_7 + 1} (α := A)
    (∑ i_1 : n,
      a₁_1 * a₂_1 *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i i_1) : A)
          ((algebraMap R A : (a : R) → A) (b₂ i_1 j) : A))
    (∑ x : n,
      HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A))
a₅ :
  Eq.{u_7 + 1} (α := A)
    (∑ x : n,
      a₁_1 *
        (a₂_1 *
          HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
            ((algebraMap R A : (a : R) → A) (b₂ x j) : A)))
    (∑ x : n,
      a₁_1 *
        HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          (HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)))
⊢ a₁_1 * a₂_1 *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j

Tactic:
simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]

Premises used: Finset.mul_sum, mul_assoc, Matrix.map_apply, Matrix.mul_apply, Matrix.smul_apply, Algebra.left_comm, smul_eq_mul