by_contra 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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert 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 : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
⊢ False