Theorem: Matroid.restrict_contract_eq_contract_restrict (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 R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C
Tactic:
rw [contract_restrict_eq_restrict_contract _ _ _ disjoint_sdiff_right]
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 R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ 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 R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C
Tactic:
simp [union_eq_self_of_subset_right hCR]
State after:
no goals