rw [← M.relRank_add_of_subset_of_subset hF₀F'.subset hF'F₁.subset, hF'F₁.relRank_eq_one,
  hF₀F'.relRank_eq_one]
α : 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₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ M.relRank F₀ F₁ = 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 : α
hF₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ 1 + 1 = 2