Theorem: Matroid.Nonloop.relRank_eq_sub_one (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X = M.er (insert e X) - 1
Tactic:
apply WithTop.add_right_cancel (show (1 : ℕ∞) ≠ ⊤ from ENat.coe_toNat_eq_self.mp rfl)
State after:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X) - 1 + 1

State before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X) - 1 + 1
Tactic:
rw [← he.relRank_add_one_eq, 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 : α
he : M.Nonloop e
X : Set α
⊢ 1 ≤ M.relRank {e} X + 1

State before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ 1 ≤ M.relRank {e} X + 1
Tactic:
exact le_add_self
State after:
no goals