Theorem: Matroid.rFin.relRank_eq_sub (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.er Y - M.er X
Tactic:
rw [← relRank_add_er_of_subset _ hXY]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.relRank X Y + M.er X - M.er X

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.relRank X Y + M.er X - M.er X
Tactic:
apply WithTop.add_right_cancel <| ne_top_of_lt hY
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.relRank X Y + M.er X - M.er X + M.er X

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.relRank X Y + M.er X - M.er X + M.er X
Tactic:
rw [eq_comm, tsub_add_cancel_iff_le]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.er X ≤ M.relRank X Y + M.er X

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.er X ≤ M.relRank X Y + M.er X
Tactic:
exact le_add_self
State after:
no goals