Theorem: Matroid.Basis'.relRank_eq_encard_diff (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 ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
Tactic:
rw [relRank_eq_relRank_union, relRank, ← er_cl_eq, contract_cl_eq, union_assoc, union_self,
  ← hI.cl_eq_cl, ← relRank_eq_er_diff_contract, relRank_cl_right,
  relRank_eq_er_diff_contract, Indep.er]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ (M ／ C).Indep (I \ C)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ (M ／ C).Indep (I \ C)
Tactic:
rw [hIC.contract_eq_contract_delete, delete_indep_iff, hIC.indep.contract_indep_iff,
  diff_union_inter, and_iff_left hI.indep, ← disjoint_union_right, union_diff_self,
  union_eq_self_of_subset_left inter_subset_right]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ Disjoint (I \ C) C

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ Disjoint (I \ C) C
Tactic:
exact disjoint_sdiff_left
State after:
no goals