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

State before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X : Set α
⊢ (M ／ C).er X ≤ M.er X
Tactic:
obtain ⟨I, hI⟩ := (M ／ C).exists_basis (X ∩ (M ／ C).E)
State after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ (M ／ C).er X ≤ M.er X

State before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ (M ／ C).er X ≤ M.er X
Tactic:
rw [← er_inter_ground_eq, ← hI.encard, ← hI.indep.of_contract.er]
State after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ M.er I ≤ M.er X

State before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ M.er I ≤ M.er X
Tactic:
exact M.er_mono (hI.subset.trans inter_subset_left)
State after:
no goals