rintro ⟨F, hF⟩ (h₀ : F₀ ⊆ F) (h₁ : 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 : α
x✝ : M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
hforall : ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
⊢ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
case refine_2.mk
α : 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✝ : M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
hforall : ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
F : Set α
hF : M.Flat F
h₀ : F₀ ⊆ F
h₁ : F ⊆ F₁
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf