suffices e ∈ M.cl (M.cl I) from h.not_mem_cl_diff_of_mem (.inl rfl) <| by simpa [heI']
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ False
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ e ∈ M.cl (M.cl I)