simp_rw [indep_iff, hI.contract_base_iff, union_subset_iff]
α : 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 ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)
α : 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
⊢ (∃ B, (M.Base (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B