obtain (rfl | hne) := eq_or_ne e₁ e₂
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
⊢ M.ConnectedTo e₁ e₂
case inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₁
⊢ M.ConnectedTo e₁ e₁

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
⊢ M.ConnectedTo e₁ e₂