Theorem: Matroid.Minor.erk_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
⊢ N.erk ≤ M.erk
Tactic:
obtain ⟨C, D, -, -, -, rfl⟩ := h
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C ＼ D).erk ≤ M.erk

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C ＼ D).erk ≤ M.erk
Tactic:
rw [← er_univ_eq, ← er_univ_eq, delete_er_eq']
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C).er (univ \ D) ≤ M.er univ

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C).er (univ \ D) ≤ M.er univ
Tactic:
exact (M.er_contract_le_er _ _).trans (M.er_mono diff_subset)
State after:
no goals