no goals
α : Type ?u.40762
β : Type ?u.40765
m : Type u_1
n : Type ?u.40771
o : Type ?u.40774
m' : α → Type ?u.40779
n' : α → Type ?u.40784
R : Type v
inst✝⁶ : CommRing R
M✝ N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
M : Matrix m m R
p q : m → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ det (toSquareBlockProp M p) = det (toSquareBlockProp M q)
convert Matrix.det_reindex_self (Equiv.subtypeEquivRight e) (toSquareBlockProp M q)