obtain ⟨K₁, hK₁, he₁K₁, hfK₁⟩ := h₁.exists_cocircuit_of_ne hne₁
case inr.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
hne₂ : f ≠ e₂
⊢ M.ConnectedTo e₁ e₂
case inr.inr.inr.intro.intro.intro
α : 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
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
⊢ M.ConnectedTo e₁ e₂