rintro ⟨⟨heF, (hF | hF)⟩, hFU⟩
case mp
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U → e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

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

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

case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U