Theorem: Matroid.contract_minor_of_subset (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C' ≤m M ／ C
Tactic:
rw [← diff_union_of_subset hCC', union_comm, ← contract_contract]
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C ／ (C' \ C) ≤m M ／ C

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C ／ (C' \ C) ≤m M ／ C
Tactic:
apply contract_minor
State after:
no goals