refine fun heCl ↦ ?_
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ e ∉ M.cl I
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
heCl : e ∈ M.cl I
⊢ False