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