refine' (M.subset_cl F hF).antisymm' (fun e heF ↦ by_contra fun 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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
⊢ M.cl F = F
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
⊢ False