by_contra hf
α : 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
⊢ f ∈ K
α : 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