have hcon := (h _ (hef.circuit_of_ne hne)).trans_eq (encard_pair hne)
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
⊢ False
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
hcon : 3 ≤ 2
⊢ False