refine' ⟨B, hB.subset hsub⟩
case intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Y : Set (Set α)
hsub : Y ⊆ X
B : Set α
hB : M.ModularBase B fun x => ↑x
⊢ M.ModularFamily fun y => ↑y
no goals