obtain ⟨f, hf⟩ := h _ hH.compl_cocircuit ⟨he, he'⟩
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
⊢ False
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✝ : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
f : α
hf : f ∈ X ∩ (M✶.E \ H)
⊢ False