refine' ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_cl_of_mem heI)),
  fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h e heI _,fun e heI hin ↦ h e heI
    (by rw [cl_diff_singleton_eq_cl hin])⟩⟩
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.cl (I \ {e}) = M.cl I