Theorem: Matroid.truncate_base_iff (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.truncate.Base B ↔ ∃ e ∉ B, M.Base (insert e B)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e, he, hBe⟩ ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Base B

State before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Base B
Tactic:
refine Indep.base_of_forall_insert ?_ ?_
State after:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Indep B

case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.truncate.E \ B, ¬M.truncate.Indep (insert e B)

State before:
case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.truncate.E \ B, ¬M.truncate.Indep (insert e B)
Tactic:
simp only [truncate_ground_eq, mem_diff, truncate_indep_iff, not_and, not_not, and_imp]
State after:
case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.E, e ∉ B → M.Indep (insert e B) → M.Base (insert e B)

State before:
case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.E, e ∉ B → M.Indep (insert e B) → M.Base (insert e B)
Tactic:
exact fun f _ hfB hfBi ↦ insert_base_of_insert_indep he hfB hBe hfBi
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
obtain ⟨hB, hBb⟩ := truncate_indep_iff.1 h.indep
State after:
case refine_1.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)

State before:
case refine_1.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
obtain ⟨B', hB', hBB'⟩ := hB.exists_base_superset
State after:
case refine_1.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
⊢ ∃ e ∉ B, M.Base (insert e B)

State before:
case refine_1.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
obtain ⟨e, heB', heB⟩ := exists_of_ssubset (hBB'.ssubset_of_ne (by rintro rfl; contradiction))
State after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ ∃ e ∉ B, M.Base (insert e B)

State before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
refine ⟨e, heB, ?_⟩
State after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Base (insert e B)

State before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Base (insert e B)
Tactic:
rwa [h.eq_of_subset_indep ?_ (subset_diff_singleton hBB' heB), insert_diff_singleton,
  insert_eq_of_mem heB']
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.truncate.Indep (B' \ {e})

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.truncate.Indep (B' \ {e})
Tactic:
rw [truncate_indep_iff]
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Indep (B' \ {e}) ∧ ¬M.Base (B' \ {e})

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Indep (B' \ {e}) ∧ ¬M.Base (B' \ {e})
Tactic:
exact ⟨hB'.indep.subset diff_subset, hB'.not_base_of_ssubset <| diff_singleton_sSubset.mpr heB'⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
⊢ B ≠ B'
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
hB' : M.Base B
hBB' : B ⊆ B
⊢ False

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
hB' : M.Base B
hBB' : B ⊆ B
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Indep B
Tactic:
rw [truncate_indep_iff]
State after:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.Indep B ∧ ¬M.Base B

State before:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.Indep B ∧ ¬M.Base B
Tactic:
exact ⟨hBe.indep.subset (subset_insert _ _), hBe.not_base_of_ssubset (ssubset_insert he)⟩
State after:
no goals