obtain ⟨f, ⟨rfl, -⟩, hfe⟩ := (he'.cocircuit_inter_nontrivial hK ⟨e, by simp [he]⟩).exists_ne e
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ False
case intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
f✝ : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
f : α
he : f ∈ K
he' : M.Circuit {f}
hfe : f ≠ f
⊢ False