rw [hsp _ hSE]
α : 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
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S
no goals