Theorem: Matroid.subset_hyperplane_iff_cl_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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.cl Y ≠ M.E ↔ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Tactic:
refine' ⟨fun h ↦ _, _⟩
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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ 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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ H, M.Hyperplane H ∧ Y ⊆ H) → M.cl Y ≠ M.E

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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ H, M.Hyperplane H ∧ Y ⊆ H) → M.cl Y ≠ M.E
Tactic:
rintro ⟨H, hH, hYH⟩ hY
State after:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ False

State before:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ False
Tactic:
refine' hH.ssubset_ground.not_subset _
State after:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ H

State before:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ H
Tactic:
rw [← hH.flat.cl]
State after:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ M.cl H

State before:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ M.cl H
Tactic:
exact hY.symm.trans_subset (M.cl_mono hYH)
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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Tactic:
obtain ⟨H, hH, hYH⟩ := (M.cl_flat Y).subset_hyperplane_of_ne_ground h
State after:
case refine'_1.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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
H : Set α
hH : M.Hyperplane H
hYH : M.cl Y ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H

State before:
case refine'_1.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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
H : Set α
hH : M.Hyperplane H
hYH : M.cl Y ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Tactic:
exact ⟨H, hH, (M.subset_cl Y).trans hYH⟩
State after:
no goals