rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I
no goals