refine'
  ⟨fun e he ↦ _, h.1.1.ssubset_of_ne (by rintro rfl; exact h.1.2 M.ground_spanning),
    fun F hF hHF hFE ↦ or_iff_not_imp_right.mpr fun hFE' ↦ _⟩
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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ (∀ e ∈ M.E \ H, M.cl H ⊂ M.cl (insert e H)) ∧ H ⊂ M.E ∧ ∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
⊢ M.cl H ⊂ M.cl (insert e 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
⊢ F = H