Theorem: Matroid.Basis'.relRank_eq_encard_diff_of_subset (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
hCX : C ⊆ X
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
Tactic:
rw [← union_eq_self_of_subset_right hCX] at hI
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hCX : C ⊆ X
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard

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