Theorem: Matroid.Hyperplane.basis_hyperplane_delete (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ (M ＼ (H \ I)).Hyperplane I
Tactic:
obtain ⟨e, he, heH⟩ := exists_of_ssubset hH.ssubset_ground
State after:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ (M ＼ (H \ I)).Hyperplane I

State before:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ (M ＼ (H \ I)).Hyperplane I
Tactic:
convert Base.hyperplane_of_cl_diff_singleton (B := insert e I) (e := e) ?_ (.inl rfl)
State after:
case h.e'_3
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = (M ＼ (H \ I)).cl (insert e I \ {e})

case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ (M ＼ (H \ I)).Base (insert e I)

State before:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ (M ＼ (H \ I)).Base (insert e I)
Tactic:
simp only [delete_base_iff]
State after:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ M.Basis (insert e I) (M.E \ (H \ I))

State before:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ M.Basis (insert e I) (M.E \ (H \ I))
Tactic:
refine hB.indep.basis_of_forall_insert ?_ fun x ⟨⟨hxE, _⟩, hx⟩ ↦ hB.insert_dep ⟨hxE, hx⟩
State after:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ⊆ M.E \ (H \ I)

State before:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ⊆ M.E \ (H \ I)
Tactic:
suffices insert e I ∩ (H \ I) = ∅ by simpa [insert_subset_iff, he, heH, subset_diff,
  hI.indep.subset_ground, disjoint_iff_inter_eq_empty]
State after:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ∩ (H \ I) = ∅

State before:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ∩ (H \ I) = ∅
Tactic:
rw [insert_inter_of_not_mem (by simp [heH])]
State after:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ∩ (H \ I) = ∅

State before:
case intro.intro.convert_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ∩ (H \ I) = ∅
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Base (insert e I)
Tactic:
refine Indep.base_of_spanning ?_ ?_
State after:
case refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Indep (insert e I)

case refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Spanning (insert e I)

State before:
case refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Spanning (insert e I)
Tactic:
rw [spanning_iff_cl, ← cl_insert_cl_eq_cl_insert, hI.cl_eq_cl, hH.flat.cl,
  hH.cl_eq_ground_of_ssuperset (ssubset_insert heH)]
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Indep (insert e I)
Tactic:
rwa [hI.indep.insert_indep_iff_of_not_mem (not_mem_subset hI.subset heH), hI.cl_eq_cl,
  hH.flat.cl, mem_diff, and_iff_left heH]
State after:
no goals

State before:
case h.e'_3
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = (M ＼ (H \ I)).cl (insert e I \ {e})
Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem, not_mem_subset hI.subset heH,
not_false_eq_true, diff_singleton_eq_self, delete_cl_eq]
State after:
case h.e'_3
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = M.cl (I \ (H \ I)) \ (H \ I)

State before:
case h.e'_3
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = M.cl (I \ (H \ I)) \ (H \ I)
Tactic:
rw [disjoint_sdiff_right.sdiff_eq_left, hI.cl_eq_cl, hH.flat.cl, diff_diff_cancel_left]
State after:
case h.e'_3
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ⊆ H

State before:
case h.e'_3
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ⊆ H
Tactic:
exact hI.subset
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
this : insert e I ∩ (H \ I) = ∅
⊢ insert e I ⊆ M.E \ (H \ I)
Tactic:
simpa [insert_subset_iff, he, heH, subset_diff,
hI.indep.subset_ground, disjoint_iff_inter_eq_empty]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ e ∉ H \ I
Tactic:
simp [heH]
State after:
no goals