simp_rw [deleteElem, eq_iff_indep_iff_indep_forall, addLoop_ground, addLoop_indep_iff,
  delete_ground, delete_indep_iff, disjoint_singleton_right, ← singleton_dep, dep_iff,
  singleton_subset_iff, and_iff_left he', subset_diff, disjoint_singleton_right, and_imp]
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ (M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I) ↔
    ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)