Theorem: Matroid.Minor.rk_le (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
have hle := h.erk_le
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
⊢ N.rk ≤ M.rk

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
⊢ N.rk ≤ M.rk
Tactic:
have := h.finiteRk
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
this : N.FiniteRk
⊢ N.rk ≤ M.rk

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
rw [← M.coe_rk_eq, ← N.coe_rk_eq] at hle
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : ↑N.rk ≤ ↑M.rk
this : N.FiniteRk
⊢ N.rk ≤ M.rk

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : ↑N.rk ≤ ↑M.rk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
exact WithTop.coe_le_coe.1 hle
State after:
no goals