rw [hF₀.covBy_iff_relRank_eq_one hF, hF.covBy_iff_relRank_eq_one hF₁,
  and_iff_right h₀.subset, and_iff_right h₁.subset]
α : 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₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
α : 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₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ M.relRank F₀ F = 1 ∧ M.relRank F F₁ = 1