simp only [heI, not_true_eq_false, mem_diff, mem_singleton_iff, true_and, false_and,
  iff_false, parallelExtend_ground]
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∈ I
⊢ ¬(M.parallelExtend e f).Indep I