Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «0».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

pp: case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

pp: case «2».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «2».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «0».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

case «2».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «2».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «2».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)