obtain (rfl | hne) := eq_or_ne e f
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C