rw [hF.cl] at heF
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat F
⊢ M.cl F = insert e F
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ F
hF : M.Flat F
⊢ M.cl F = insert e F