Theorem: Matroid.ModularFamily.subset (Matroid/Old/_ModularCut.lean)

State before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Y : Set (Set α)
hmod : M.ModularFamily fun x => ↑x
hsub : Y ⊆ X
⊢ M.ModularFamily fun y => ↑y
Tactic:
obtain ⟨B, hB⟩ := hmod
State after:
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

State before:
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
Tactic:
refine' ⟨B, hB.subset hsub⟩
State after:
no goals