awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
j : Fin 3
a :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      α)
a₁ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      α)
a₂ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
j : Fin 3
a :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      α)
a₁ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      α)
a₂ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
j : Fin 3
a :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      α)
a₁ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      α)
a₂ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := Matrix (Fin 2) (Fin 2) α) (OfNat.ofNat n : Matrix (Fin 2) (Fin 2) α)
    (!![OfNat.ofNat n, 0; 0, OfNat.ofNat n] : Matrix (Fin 2) (Fin 2) α)

Tactic:
natCast_fin_two _

Premises used: Matrix.natCast_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := Matrix (Fin 3) (Fin 3) α) (OfNat.ofNat n : Matrix (Fin 3) (Fin 3) α)
    (!![OfNat.ofNat n, 0, 0; 0, OfNat.ofNat n, 0; 0, 0, OfNat.ofNat n] : Matrix (Fin 3) (Fin 3) α)

Tactic:
natCast_fin_three _

Premises used: Matrix.natCast_fin_three
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
a : ∀ (i j : Fin 2), A i j = !![A 0 0, A 0 1; A 1 0, A 1 1] i j
⊢ A = !![A 0 0, A 0 1; A 1 0, A 1 1]

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
a : A ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
a₁ : A ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ A i j = !![A 0 0, A 0 1; A 1 0, A 1 1] i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
a :
  A ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  A ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ A ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
a :
  A ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  A ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ A ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
a : ∀ (i j : Fin 3), A i j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] i j
⊢ A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2]

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
a :
  A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) j =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j
a₁ :
  A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) j =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j
a₂ :
  A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) j =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j
⊢ A i j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
a :
  A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
a₁ :
  A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
a₂ :
  A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
⊢ A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) j =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
a :
  A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
a₁ :
  A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
a₂ :
  A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
⊢ A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) j =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
a :
  A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
a₁ :
  A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
a₂ :
  A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
⊢ A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) j =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
a :
  ∀ (i j : Fin 2),
    HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
        (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α) i j =
      !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
a :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
a₁ :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
a :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
a :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply, Fin.sum_univ_succ]

Premises used: Matrix.mul_apply, Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.mul_apply, Fin.sum_univ_succ]

Premises used: Matrix.mul_apply, Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply, Fin.sum_univ_succ]

Premises used: Matrix.mul_apply, Fin.sum_univ_succ