rw [hJ.relRank_eq_encard_diff_of_subset hXY hI, hK.relRank_eq_encard_diff_of_subset hYZ hJ,
  hK.relRank_eq_encard_diff_of_subset (hXY.trans hYZ)
  (by rwa [inter_assoc, inter_eq_self_of_subset_right hXY] at hI),
  ← encard_union_eq, diff_eq, diff_eq, inter_assoc, ← inter_union_distrib_left,
  inter_union_distrib_right, union_compl_self, univ_inter, ← compl_inter,
  inter_eq_self_of_subset_left hXY, diff_eq]
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ Disjoint ((K ∩ Y) \ X) (K \ Y)