rw [← Base.encard_compl_eq hB.restrict_base]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I (I ∪ X)
hdj : Disjoint I X
⊢ (M ↾ (I ∪ X))✶.erk = X.encard
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I (I ∪ X)
hdj : Disjoint I X
⊢ ((M ↾ (I ∪ X)).E \ I).encard = X.encard