Theorem: Matroid.IsoMinor.rk_le (Matroid/Minor/Iso.lean)

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
inst✝ : M.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
obtain ⟨M₀, hM₀, i, -⟩ := e.exists_iso
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
inst✝ : M.FiniteRk
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.rk ≤ M.rk

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
inst✝ : M.FiniteRk
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.rk ≤ M.rk
Tactic:
exact i.rk_eq.trans_le hM₀.rk_le
State after:
no goals