have hK' := (hK.compl_hyperplane).flat.cl
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
⊢ False
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
⊢ False