refine ⟨f '' B, hB.mapEmbedding f, fun i ↦ ?_⟩
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ (M.mapEmbedding f).ModularFamily fun i => ⇑f '' Xs i
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (M.mapEmbedding f).Basis ((fun i => ⇑f '' Xs i) i ∩ ⇑f '' B) ((fun i => ⇑f '' Xs i) i)