simp [det_fin_two, trace_fin_two]
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A).det = 1 + A.det + A.trace
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A 0 0) * (1 + A 1 1) - A 0 1 * A 1 0 = 1 + (A 0 0 * A 1 1 - A 0 1 * A 1 0) + (A 0 0 + A 1 1)