have hef : e ≠ f := by rintro rfl; exact hf he.mem_ground
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))