obtain (h1 | h2) := hforall ⟨F, hF⟩ hF₀ hF₁
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 : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
⊢ F = F₀ ∨ F = F₁
case refine_1.inl
α : 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 : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
h1 : ⟨F, hF⟩ = ⋯.toFlatOf
⊢ F = F₀ ∨ F = F₁

case refine_1.inr
α : 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 : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
h2 : ⟨F, hF⟩ = ⋯.toFlatOf
⊢ F = F₀ ∨ F = F₁