obtain (rfl | hne) := eq_or_ne e f
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he hf : M.Nonloop e
⊢ M.cl {e} = M.cl {e} ↔ e = e ∨ ¬M.Indep {e, e}

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}