Theorem: MatrixCookbook.eq_477 (MatrixCookbook/9SpecialMatrices.lean)

State before:
R : Type u_1
l : Type ?u.198937
m : Type ?u.198940
n : Type ?u.198943
p : Type ?u.198946
q : Type ?u.198949
r : Type ?u.198952
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
⊢ of ![![0, 1, 0], ![1, 0, 0], ![0, 0, 1]] = of ![Pi.single 1 1, Pi.single 0 1, Pi.single 2 1]
Tactic:
ext i j
State after:
case a
R : Type u_1
l : Type ?u.198937
m : Type ?u.198940
n : Type ?u.198943
p : Type ?u.198946
q : Type ?u.198949
r : Type ?u.198952
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
i j : Fin 3
⊢ of ![![0, 1, 0], ![1, 0, 0], ![0, 0, 1]] i j = of ![Pi.single 1 1, Pi.single 0 1, Pi.single 2 1] i j

State before:
case a
R : Type u_1
l : Type ?u.198937
m : Type ?u.198940
n : Type ?u.198943
p : Type ?u.198946
q : Type ?u.198949
r : Type ?u.198952
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
i j : Fin 3
⊢ of ![![0, 1, 0], ![1, 0, 0], ![0, 0, 1]] i j = of ![Pi.single 1 1, Pi.single 0 1, Pi.single 2 1] i j
Tactic:
fin_cases i <;> fin_cases j <;> rfl
State after:
no goals