refine' ⟨fun h ↦ _, _⟩
α : 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
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