exact fun hcon ↦ hef <| hcon.1.2 (by simp) (by simp) (by simp [update_noteq hef e id])
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ ¬((M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E)
no goals