simp only [restrict_ground_eq, restrict_indep_iff, comap_indep_iff, ne_eq, image_update, id_eq,
  image_id', mem_diff, mem_singleton_iff, update_id_injOn_iff, delete_indep_iff,
  disjoint_singleton_right, and_congr_left_iff, iff_self_and, true_and]
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ (M.comap (update id f e) ↾ insert f M.E).E = ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).E ∧
    ∀ I ⊆ (M.comap (update id f e) ↾ insert f M.E).E,
      (M.comap (update id f e) ↾ insert f M.E).Indep I ↔ ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).Indep I
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ∀ I ⊆ insert f M.E,
    I ⊆ insert f M.E →
      (f ∈ I → e ∈ I → f = e) →
        M.Indep (if f ∈ I then insert e (I \ {f}) else I) → f ∉ if f ∈ I then insert e (I \ {f}) else I