Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

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

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

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

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

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

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

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

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

Tactic:
<;>

Goal state after:
case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

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

case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

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

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

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

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