rw [inter_eq_iInter]
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ F ∩ F' ∈ U
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ (⋂ b, bif b then F else F') ∈ U