simp
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ True ∧ True
no goals