exact hf he.mem_ground
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
hdel : ∀ (J : Set α), e ∉ J → ((M.parallelExtend e e).Indep J ↔ M.Indep J)
⊢ False
no goals