internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)
Tactic:
obtain Basis := hB i
Proof state after:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)
Tactic:
have R_B'_inter_eq : R ∩ B' = B := by
  rw [ext_iff]
  refine' fun x ↦ ⟨fun x_mem ↦ _, fun x_mem ↦ ⟨hBb.subset_ground x_mem, hB'.2 x_mem⟩⟩
  by_contra x_nB
  apply (hB'.1.indep.subset (insert_subset x_mem.2 hB'.2)).not_dep
  rw [Dep, and_iff_left ((insert_subset x_mem.2 hB'.2).trans hB'.1.subset_ground)]
  exact (restrict_dep_iff.1 (hBb.insert_dep ⟨x_mem.1, x_nB⟩)).1
Proof state after:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)
Tactic:
simp only
Proof state after:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis (Xs i ∩ M.E ∩ B') (Xs i ∩ M.E)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis (Xs i ∩ M.E ∩ B') (Xs i ∩ M.E)
Tactic:
rw [basis_restrict_iff'] at Basis
Proof state after:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : M.Basis (Xs i ∩ B) (Xs i ∩ M.E) ∧ Xs i ⊆ R
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis (Xs i ∩ M.E ∩ B') (Xs i ∩ M.E)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : M.Basis (Xs i ∩ B) (Xs i ∩ M.E) ∧ Xs i ⊆ R
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis (Xs i ∩ M.E ∩ B') (Xs i ∩ M.E)
Tactic:
rw [ ← inter_eq_self_of_subset_left Basis.2, inter_right_comm _ R, inter_assoc, R_B'_inter_eq,
  inter_assoc, inter_eq_self_of_subset_right (hB'.2.trans hB'.1.subset_ground),
  inter_right_comm, inter_eq_self_of_subset_left Basis.2]
Proof state after:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : M.Basis (Xs i ∩ B) (Xs i ∩ M.E) ∧ Xs i ⊆ R
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis (Xs i ∩ B) (Xs i ∩ M.E)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : M.Basis (Xs i ∩ B) (Xs i ∩ M.E) ∧ Xs i ⊆ R
R_B'_inter_eq : R ∩ B' = B
⊢ M.Basis (Xs i ∩ B) (Xs i ∩ M.E)
Tactic:
exact Basis.1
Proof state after:
no goals
Theorem: Matroid.ModularFamily.ofRestrict'
Proof 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ R ∩ B' = B
Tactic:
rw [ext_iff]
Proof state after:
ι : 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ ∀ (x : α), x ∈ R ∩ B' ↔ x ∈ B
Theorem: Matroid.ModularFamily.ofRestrict'
Proof 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ ∀ (x : α), x ∈ R ∩ B' ↔ x ∈ B
Tactic:
refine' fun x ↦ ⟨fun x_mem ↦ _, fun x_mem ↦ ⟨hBb.subset_ground x_mem, hB'.2 x_mem⟩⟩
Proof state after:
ι : 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
⊢ x ∈ B
Theorem: Matroid.ModularFamily.ofRestrict'
Proof 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
⊢ x ∈ B
Tactic:
by_contra x_nB
Proof state after:
ι : 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
x_nB : x ∉ B
⊢ False
Theorem: Matroid.ModularFamily.ofRestrict'
Proof 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
x_nB : x ∉ B
⊢ False
Tactic:
apply (hB'.1.indep.subset (insert_subset x_mem.2 hB'.2)).not_dep
Proof state after:
ι : 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
x_nB : x ∉ B
⊢ M.Dep (insert x B)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
x_nB : x ∉ B
⊢ M.Dep (insert x B)
Tactic:
rw [Dep, and_iff_left ((insert_subset x_mem.2 hB'.2).trans hB'.1.subset_ground)]
Proof state after:
ι : 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
x_nB : x ∉ B
⊢ ¬M.Indep (insert x B)
Theorem: Matroid.ModularFamily.ofRestrict'
Proof 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
Basis : (M ↾ R).Basis (Xs i ∩ B) (Xs i)
x : α
x_mem : x ∈ R ∩ B'
x_nB : x ∉ B
⊢ ¬M.Indep (insert x B)
Tactic:
exact (restrict_dep_iff.1 (hBb.insert_dep ⟨x_mem.1, x_nB⟩)).1
Proof state after:
no goals
Theorem: Matroid.ModularFamily.ofRestrict
Proof 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 : α
M : Matroid α
R : Set α
hR : R ⊆ M.E
h : (M ↾ R).ModularFamily Xs
⊢ M.ModularFamily Xs
Tactic:
convert h.ofRestrict' with i
Proof 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 : α
M : Matroid α
R : Set α
hR : R ⊆ M.E
h : (M ↾ R).ModularFamily Xs
i : ι
⊢ Xs i = Xs i ∩ M.E
Theorem: Matroid.ModularFamily.ofRestrict
Proof 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 : α
M : Matroid α
R : Set α
hR : R ⊆ M.E
h : (M ↾ R).ModularFamily Xs
i : ι
⊢ Xs i = Xs i ∩ M.E
Tactic:
rw [inter_eq_self_of_subset_left <| (h.subset_ground_of_mem i).trans hR]
Proof state after:
no goals
Theorem: Matroid.ModularFamily.comp
Proof 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
h : M.ModularFamily Xs
t : η → ι
⊢ M.ModularFamily (Xs ∘ t)
Tactic:
obtain ⟨B, hB, hBXs⟩ := h
Proof 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
t : η → ι
B : Set α
hB : M.Base B
hBXs : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ M.ModularFamily (Xs ∘ t)
Theorem: Matroid.ModularFamily.comp
Proof 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
t : η → ι
B : Set α
hB : M.Base B
hBXs : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ M.ModularFamily (Xs ∘ t)
Tactic:
exact ⟨B, hB, fun i ↦ (by simpa using hBXs (t i))⟩
Proof state after:
no goals
Theorem: Matroid.ModularFamily.comp
Proof 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
t : η → ι
B : Set α
hB : M.Base B
hBXs : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : η
⊢ M.Basis ((Xs ∘ t) i ∩ B) ((Xs ∘ t) i)
Tactic:
simpa using hBXs (t i)
Proof state after:
no goals
Theorem: Matroid.ModularFamily.set_biInter_comp
Proof 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
h : M.ModularFamily Xs
t : η → Set ι
ht : ∀ (j : η), (t j).Nonempty
⊢ M.ModularFamily fun j => ⋂ i ∈ t j, Xs i
Tactic:
obtain ⟨B, hB⟩ := h
Proof state after:
case 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
t : η → Set ι
ht : ∀ (j : η), (t j).Nonempty
B : Set α
hB : M.ModularBase B Xs
⊢ M.ModularFamily fun j => ⋂ i ∈ t j, Xs i
Theorem: Matroid.ModularFamily.set_biInter_comp
Proof state before:
case 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
t : η → Set ι
ht : ∀ (j : η), (t j).Nonempty
B : Set α
hB : M.ModularBase B Xs
⊢ M.ModularFamily fun j => ⋂ i ∈ t j, Xs i
Tactic:
exact ⟨B, hB.base, fun j ↦ hB.basis_biInter (ht j)⟩
Proof state after:
no goals
Theorem: Matroid.ModularFamily.map
Proof 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
Proof 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
Theorem: Matroid.ModularFamily.map
Proof 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 ↦ ?_⟩
Proof 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)
Theorem: Matroid.ModularFamily.map
Proof 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
Proof 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)
Theorem: Matroid.ModularFamily.map
Proof 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]
Proof state after:
no goals
Theorem: Matroid.modularFamily_map_iff
Proof 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⟩ ↦ ?_⟩
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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
Theorem: Matroid.modularFamily_map_iff
Proof 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⟩
Proof 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)
Theorem: Matroid.modularFamily_map_iff
Proof 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
Proof 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