obtain (rfl | hne₁) := eq_or_ne e₁ f
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₂
case inr.inl
α : Type u_1
M : Matroid α
C K : Set α
e g e₁ e₂ : α
hne : e₁ ≠ e₂
h₁ : M.ConnectedTo e₁ e₁
h₂ : M.ConnectedTo e₁ e₂
⊢ M.ConnectedTo e₁ e₂

case inr.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₂
hne₁ : e₁ ≠ f
⊢ M.ConnectedTo e₁ e₂