rintro rfl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : ¬(f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f})
hfX : f ∉ X
⊢ e ≠ f
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
X : Set α
hf : e ∉ M.E
heX : ¬(e ∈ (M.parallelExtend e e).cl (X \ {e}) ∧ e ∉ {e})
hfX : e ∉ X
⊢ False