Theorem: Matrix.one_fin_four (MatrixCookbook/ForMathlib/Data/Matrix.lean)

State before:
R : Type u_1
inst✝ : CommRing R
⊢ 1 = of ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 1]]
Tactic:
ext i j
State after:
case a
R : Type u_1
inst✝ : CommRing R
i j : Fin 4
⊢ 1 i j = of ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 1]] i j

State before:
case a
R : Type u_1
inst✝ : CommRing R
i j : Fin 4
⊢ 1 i j = of ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 1]] i j
Tactic:
fin_cases i <;> fin_cases j <;> rfl
State after:
no goals