Theorem: Matroid.modularFamily_map_iff (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
Xs : ι → Set β
⊢ (M.map f hf).ModularFamily Xs ↔ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨Ys, hYs, h_eq⟩ ↦ ?_⟩
State after:
case refine_1
ι : 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
Xs : ι → Set β
h : (M.map f hf).ModularFamily Xs
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

case refine_2
ι : 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
Xs : ι → Set β
x✝ : ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Ys : ι → Set α
hYs : M.ModularFamily Ys
h_eq : ∀ (i : ι), Xs i = f '' Ys i
⊢ (M.map f hf).ModularFamily Xs

State before:
case refine_2
ι : 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
Xs : ι → Set β
x✝ : ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Ys : ι → Set α
hYs : M.ModularFamily Ys
h_eq : ∀ (i : ι), Xs i = f '' Ys i
⊢ (M.map f hf).ModularFamily Xs
Tactic:
convert hYs.map f hf with i
State after:
case h.e'_4.h
ι : 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
Xs : ι → Set β
x✝ : ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Ys : ι → Set α
hYs : M.ModularFamily Ys
h_eq : ∀ (i : ι), Xs i = f '' Ys i
i : ι
⊢ Xs i = f '' Ys i

State before:
case h.e'_4.h
ι : 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
Xs : ι → Set β
x✝ : ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Ys : ι → Set α
hYs : M.ModularFamily Ys
h_eq : ∀ (i : ι), Xs i = f '' Ys i
i : ι
⊢ Xs i = f '' Ys i
Tactic:
apply h_eq
State after:
no goals

State before:
case refine_1
ι : 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
Xs : ι → Set β
h : (M.map f hf).ModularFamily Xs
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
obtain ⟨B, hB, h⟩ := h
State after:
case refine_1.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
Xs : ι → Set β
B : Set β
hB : (M.map f hf).Base B
h : ∀ (i : ι), (M.map f hf).Basis (Xs i ∩ B) (Xs i)
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

State before:
case refine_1.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
Xs : ι → Set β
B : Set β
hB : (M.map f hf).Base B
h : ∀ (i : ι), (M.map f hf).Basis (Xs i ∩ B) (Xs i)
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
simp_rw [map_basis_iff'] at h
State after:
case refine_1.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
Xs : ι → Set β
B : Set β
hB : (M.map f hf).Base B
h : ∀ (i : ι), ∃ I₀ X₀, M.Basis I₀ X₀ ∧ Xs i ∩ B = f '' I₀ ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

State before:
case refine_1.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
Xs : ι → Set β
B : Set β
hB : (M.map f hf).Base B
h : ∀ (i : ι), ∃ I₀ X₀, M.Basis I₀ X₀ ∧ Xs i ∩ B = f '' I₀ ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
rw [map_base_iff] at hB
State after:
case refine_1.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
Xs : ι → Set β
B : Set β
hB : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
h : ∀ (i : ι), ∃ I₀ X₀, M.Basis I₀ X₀ ∧ Xs i ∩ B = f '' I₀ ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

State before:
case refine_1.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
Xs : ι → Set β
B : Set β
hB : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
h : ∀ (i : ι), ∃ I₀ X₀, M.Basis I₀ X₀ ∧ Xs i ∩ B = f '' I₀ ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
obtain ⟨B, hB, rfl⟩ := hB
State after:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
h : ∀ (i : ι), ∃ I₀ X₀, M.Basis I₀ X₀ ∧ Xs i ∩ f '' B = f '' I₀ ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

State before:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
h : ∀ (i : ι), ∃ I₀ X₀, M.Basis I₀ X₀ ∧ Xs i ∩ f '' B = f '' I₀ ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
choose Is hIs using h
State after:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is : ι → Set α
hIs : ∀ (i : ι), ∃ X₀, M.Basis (Is i) X₀ ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

State before:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is : ι → Set α
hIs : ∀ (i : ι), ∃ X₀, M.Basis (Is i) X₀ ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' X₀
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
choose Ys hYs using hIs
State after:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

State before:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
⊢ ∃ Ys, M.ModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i
Tactic:
refine ⟨Ys, ⟨B, hB, fun i ↦ ?_⟩, fun i ↦ (hYs i).2.2⟩
State after:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ M.Basis (Ys i ∩ B) (Ys i)

State before:
case refine_1.intro.intro.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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ M.Basis (Ys i ∩ B) (Ys i)
Tactic:
convert (hYs i).1
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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ∩ B = Is i

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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ∩ B = Is i
Tactic:
rw [← hf.image_eq_image_iff (inter_subset_right.trans hB.subset_ground)
  (hYs i).1.indep.subset_ground, ← (hYs i).2.1, (hYs i).2.2, hf.image_inter]
State after:
case h.e'_3.hs
ι : 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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ⊆ M.E

case h.e'_3.ht
ι : 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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ B ⊆ M.E

State before:
case h.e'_3.ht
ι : 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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ B ⊆ M.E
Tactic:
exact hB.subset_ground
State after:
no goals

State before:
case h.e'_3.hs
ι : 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
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ⊆ M.E
Tactic:
exact (hYs i).1.subset_ground
State after:
no goals