obtain (rfl | hne) := eq_or_ne e f
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
⊢ M.ConnectedTo e f
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e e
⊢ M.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
⊢ M.ConnectedTo e f