rw [h, and_iff_left (.inl rfl), ← h]
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
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 (M.cl F)