rw [← hef.mem_cl_iff_mem_cl, hK'] at hfK
α : 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
hfK : f ∈ M.cl (M.E \ 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
hfK : e ∈ M.E \ K
⊢ False