have hsp' : M.Spanning = M'.Spanning := by
  ext S
  refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
    (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
    (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
α : 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
⊢ M = M'
α : 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
⊢ M = M'