exact fun hei ↦ he (singleton_subset_iff.1 hei.subset_ground)
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M.Indep {e}
no goals