Theorem: Matroid.IsoMinor.erk_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
⊢ N.erk ≤ M.erk
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
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.erk ≤ M.erk

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
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.erk ≤ M.erk
Tactic:
exact i.erk_eq.trans_le hM₀.erk_le
State after:
no goals