simp [restrictSubtype, Subtype.val_injective.injOn]
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝¹ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I✝ : Set α
M N : Matroid α
I : Set ↑X
⊢ (M.restrictSubtype X).Indep I ↔ M.Indep ↑I
no goals