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

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis (I ∩ J) J
Tactic:
rw [inter_eq_self_of_subset_right hJ]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis J J

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis J J
Tactic:
exact (hI.subset hJ).basis_self
State after:
no goals