Theorem: Matroid.Indep.union_indep_iff_contract_indep (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 α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)
Tactic:
rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]
State after:
no goals