refine fun he ↦ ⟨?_, fun h ↦ ?_⟩
α : 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)) ∧ e ∈ M.cl F ↔ M.cl F = insert e F)
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F → M.cl F = insert e F

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