simpa using hwin
case refine_3
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
hwin : ⋂₀ range Fs ∈ U
⊢ ⋂ i, Fs i ∈ U
no goals