Theorem: Matroid.ModularFamily.ofRestrict' (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 : α
R : Set α
h : (M ↾ R).ModularFamily Xs
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Tactic:
obtain ⟨B, hBb, hB⟩ := 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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ M.ModularFamily fun i => Xs i ∩ M.E

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 : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Tactic:
obtain ⟨B', hB'⟩ := hBb.indep.of_restrict.exists_base_superset
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'
⊢ M.ModularFamily fun i => Xs i ∩ M.E

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'
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Tactic:
refine' ⟨B', hB'.1, fun i ↦ _⟩
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 : ι
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)

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
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)

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
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)

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
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)

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
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)

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]
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)

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
State after:
no goals

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]
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

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⟩⟩
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

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
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

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
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)

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)]
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)

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
State after:
no goals