Theorem: Matroid.Flat.subset_hyperplane_of_ne_ground (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 : α
hF : M.Flat F
h : F ≠ M.E
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
obtain ⟨e, heE, heF⟩ := exists_of_ssubset (hF.subset_ground.ssubset_of_ne h)
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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H

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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
rw [← hF.cl] at heF
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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H

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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
obtain ⟨H, hH, hFH, -⟩ := exists_hyperplane_sep_of_not_mem_cl ⟨heE, heF⟩
State after:
case intro.intro.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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
H : Set α
hH : M.Hyperplane H
hFH : F ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H

State before:
case intro.intro.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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
H : Set α
hH : M.Hyperplane H
hFH : F ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
exact ⟨H, hH, hFH⟩
State after:
no goals