Theorem: Matroid.ModularFamily.mapEmbedding (Matroid/Modular.lean)

State before:
ι : 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 : α ↪ β
h : M.ModularFamily Xs
⊢ (M.mapEmbedding f).ModularFamily fun i => ⇑f '' Xs i
Tactic:
obtain ⟨B, hB, hBX⟩ := h
State after:
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

State before:
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
Tactic:
refine ⟨f '' B, hB.mapEmbedding f, fun i ↦ ?_⟩
State after:
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)

State before:
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)
Tactic:
convert (hBX i).mapEmbedding f
State after:
case h.e'_3
ι : 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 : ι
⊢ (fun i => ⇑f '' Xs i) i ∩ ⇑f '' B = ⇑f '' (Xs i ∩ B)

State before:
case h.e'_3
ι : 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 : ι
⊢ (fun i => ⇑f '' Xs i) i ∩ ⇑f '' B = ⇑f '' (Xs i ∩ B)
Tactic:
rw [image_inter f.injective]
State after:
no goals