Theorem: Matroid.Indep.diff_indep_contract_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 C C₁ C₂ : Set α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ (M ／ I).Indep (J \ I)
Tactic:
rwa [← (hJ.subset hIJ).union_indep_iff_contract_indep, union_eq_self_of_subset_left hIJ]
State after:
no goals