have _ := hne.coe_sort
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
⊢ M.cl J ∈ U
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ M.cl J ∈ U