have h' := h.2 hFE
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
⊢ F = H
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬M.Spanning F → H ⊆ F → H = F
⊢ F = H