refine' ⟨fun h C hC heC ↦ by_contra fun hne ↦ _, fun h H hH hXE ↦ by_contra fun he' ↦ _⟩
α : 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 : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H) ↔ ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : ¬(X ∩ C).Nonempty
⊢ False

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