Theorem: Matroid.ModularFamily.map (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 : α → β
hf : InjOn f M.E
h : M.ModularFamily Xs
⊢ (M.map f hf).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 : α → β
hf : InjOn f M.E
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ (M.map f hf).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 : α → β
hf : InjOn f M.E
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ (M.map f hf).ModularFamily fun i => f '' Xs i
Tactic:
refine ⟨f '' B, hB.map hf, 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 : α → β
hf : InjOn f M.E
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (M.map f hf).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 : α → β
hf : InjOn f M.E
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (M.map f hf).Basis ((fun i => f '' Xs i) i ∩ f '' B) ((fun i => f '' Xs i) i)
Tactic:
convert (hBX i).map hf
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 : α → β
hf : InjOn f M.E
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 : α → β
hf : InjOn f M.E
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 [hf.image_inter (hBX i).subset_ground hB.subset_ground]
State after:
no goals