case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] ⬝ ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) i j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]] i j
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ ↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] ⬝ ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]] =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
ext (i j)
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] ⬝ ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) i j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]] i j
fin_cases i <;> fin_cases j <;> simp [Matrix.mul, dotProduct, Fin.sum_univ_succ]