awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 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
have a₂ : A ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : 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, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ 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
have a : A ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 ((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
have a₁ : A ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 ((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
have a₂ : A ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ 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
have a : A ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 ((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
have a₁ : A ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 ((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
have a₂ : A ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ 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
have a : A ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 ((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
have a₁ : A ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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 ((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
have a₂ : A ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : 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, sorry⟩)
    ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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) α) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
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
have 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, sorry⟩ : 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, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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
⊢ 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
have 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, sorry⟩ : 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, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
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) α)
      ((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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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, ⋯⟩)
⊢ 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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
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) α)
      ((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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
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, ⋯⟩)
⊢ 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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
have a : ∀ (i j : Fin 3),
  HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
⊢ HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j
have a : HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
    (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
    (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α)
    ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) j =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
    ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
a :
  HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j
⊢ HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j
have a₁ : HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
    (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
    (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α)
    ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) j =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
    ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
a :
  HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j
a₁ :
  HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α)
      ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j
⊢ HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
      (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
      (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j
have a₂ : HMul.hMul (α := Matrix (Fin 3) (Fin 3) α) (β := Matrix (Fin 3) (Fin 3) α)
    (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] : Matrix (Fin 3) (Fin 3) α)
    (!![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] : Matrix (Fin 3) (Fin 3) α)
    ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) j =
  !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
    ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i