Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane (Matroid/Constructions/Relax.lean)

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
⊢ ∃ f ∈ H \ B, M.Base (insert f (B \ {e})) ∨ insert f (B \ {e}) = H
Tactic:
by_contra! h
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ False

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ False
Tactic:
have h1 : H \ {e} ⊆ M.cl (B \ {e})
State after:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ H \ {e} ⊆ M.cl (B \ {e})

α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H \ {e} ⊆ M.cl (B \ {e})
⊢ False

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H \ {e} ⊆ M.cl (B \ {e})
⊢ False
Tactic:
rw [← cl_subset_cl_iff_subset_cl (diff_subset.trans hH.subset_ground),
  hHc.cl_diff_singleton_eq_cl, hH.flat.cl] at h1
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
⊢ False

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
⊢ False
Tactic:
obtain hBH := hH.eq_of_subset (hB.hyperplane_of_cl_diff_singleton he) h1
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ False

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ False
Tactic:
have hb : M.Basis (B \ {e}) H
State after:
case hb
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ M.Basis (B \ {e}) H

α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
⊢ False

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
⊢ False
Tactic:
obtain ⟨f, ⟨hfH, hfBe⟩, hfB⟩ := hHc.basis_iff_insert_eq.1 hb
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
⊢ False
Tactic:
refine (h _ ⟨hfH, fun hfB ↦ hfBe ⟨hfB, fun (hfe : f = e) ↦ ?_⟩⟩).2 hfB.symm
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ False
Tactic:
apply hB.indep.not_mem_cl_diff_of_mem he
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ e ∈ M.cl (B \ {e})

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ e ∈ M.cl (B \ {e})
Tactic:
rwa [← hBH, ← hfe]
State after:
no goals

State before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ H \ {e} ⊆ M.cl (B \ {e})
Tactic:
refine fun x hx ↦ by_contra fun hcl ↦ ?_
State after:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ False

State before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ False
Tactic:
have hxB : x ∉ B
State after:
case hxB
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ x ∉ B

case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ False

State before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ False
Tactic:
refine (h x ⟨hx.1, hxB⟩).1 (hB.exchange_base_of_indep hxB ?_)
State after:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ M.Indep (insert x (B \ {e}))

State before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ M.Indep (insert x (B \ {e}))
Tactic:
rwa [← (hB.indep.diff {e}).not_mem_cl_iff_of_not_mem (not_mem_subset diff_subset hxB)
  (hH.subset_ground hx.1)]
State after:
no goals

State before:
case hxB
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ x ∉ B
Tactic:
exact fun hxB' ↦ hcl (M.mem_cl_of_mem' ⟨hxB', hx.2⟩ (hH.subset_ground hx.1))
State after:
no goals

State before:
case hb
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ M.Basis (B \ {e}) H
Tactic:
exact (hB.indep.diff _).basis_of_subset_of_subset_cl
  ((M.subset_cl (B \ {e}) (diff_subset.trans hB.subset_ground)).trans hBH.symm.subset) h1
State after:
no goals