Theorem: Matroid.Basis.relRank_eq_encard_diff_of_subset_basis (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.relRank X Y = (J \ I).encard
Tactic:
rw [← relRank_cl_left, ← hI.cl_eq_cl, relRank_cl_left, ← relRank_cl_right, ← hJ.cl_eq_cl,
  relRank_cl_right, hJ.indep.relRank_of_subset hIJ]
State after:
no goals