rwa [h, freeOn_indep_iff, iff_true_intro Subset.rfl, and_true, true_iff] at h'
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
h' : (M ↾ I).Indep I ↔ M.Indep I ∧ I ⊆ I
⊢ M.Indep I
no goals