Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl (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 : α
h : e ∈ M.E \ M.cl X
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
State after:
case 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 : α
h : e ∈ M.E \ M.cl X
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H

State before:
case 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 : α
h : e ∈ M.E \ M.cl X
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
rw [← hI.cl_eq_cl, mem_diff, hI.indep.not_mem_cl_iff] at h
State after:
case 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H

State before:
case 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
obtain ⟨B, hB, heIB⟩ := h.2.1.exists_base_superset
State after:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : insert e I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H

State before:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : insert e I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
rw [insert_subset_iff] at heIB
State after:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H

State before:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
refine ⟨_, hB.hyperplane_of_cl_diff_singleton heIB.1, ?_, ?_⟩
State after:
case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ X ⊆ M.cl (B \ {e})

case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ e ∉ M.cl (B \ {e})

State before:
case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ e ∉ M.cl (B \ {e})
Tactic:
exact hB.indep.not_mem_cl_diff_of_mem heIB.1
State after:
no goals

State before:
case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ X ⊆ M.cl (B \ {e})
Tactic:
exact hI.subset_cl.trans (M.cl_subset_cl (subset_diff_singleton heIB.2 h.2.2))
State after:
no goals