have hmod : M.ModularFamily Is := hI.modularFamily_of_subsets (by simp [hIs])
α : 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}
⊢ 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
⊢ M.cl J ∈ U