simp only [mem_singleton_iff, hne.symm, not_false_eq_true, diff_singleton_eq_self, ite_false,
  indep_singleton, hne, false_or, or_false, and_iff_left_iff_imp]
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hne : x ≠ f
⊢ M.Indep (if f ∈ {x} then insert e ({x} \ {f}) else {x}) ∧ (x = f ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = f
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hne : x ≠ f
⊢ M.Nonloop x → x ∈ M.E