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

State before:
α : 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
Tactic:
rw [← Base.encard_compl_eq hB.restrict_base]
State after:
α : 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

State before:
α : 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
Tactic:
simp [hdj.sdiff_eq_right]
State after:
no goals