rw [← hfl.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem hFU.2, cl_cl] at hFU
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : M.cl F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U