replace hFU := U.cl_mem_of_mem hFU
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : insert e (M.cl F) ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e (M.cl F)) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)