Theorem: Matroid.cl_eq_sInter_hyperplanes (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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E
Tactic:
refine' subset_antisymm (subset_inter _ (M.cl_subset_ground _)) _
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X ⊆ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}

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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E ⊆ M.cl X

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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E ⊆ M.cl X
Tactic:
rintro e ⟨heH, heE⟩
State after:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
⊢ e ∈ M.cl X

State before:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
⊢ e ∈ M.cl X
Tactic:
refine' by_contra fun hx ↦ _
State after:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
⊢ False

State before:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
⊢ False
Tactic:
obtain ⟨H, hH, hXH, heH'⟩ := exists_hyperplane_sep_of_not_mem_cl ⟨heE, hx⟩
State after:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
heH' : e ∉ H
⊢ False

State before:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
heH' : e ∉ H
⊢ False
Tactic:
exact heH' (heH H ⟨hH, hXH⟩)
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X ⊆ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
Tactic:
rw [subset_sInter_iff]
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ t' ∈ {H | M.Hyperplane H ∧ X ⊆ H}, M.cl X ⊆ t'

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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ t' ∈ {H | M.Hyperplane H ∧ X ⊆ H}, M.cl X ⊆ t'
Tactic:
rintro H ⟨hH, hXH⟩
State after:
case refine'_1.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
⊢ M.cl X ⊆ H

State before:
case refine'_1.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
⊢ M.cl X ⊆ H
Tactic:
exact hH.flat.cl_subset_of_subset hXH
State after:
no goals