rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_diff, disjoint_comm,
  union_subset_iff, and_iff_left hI.subset_ground]
α : 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).Dep J ↔ Disjoint J I ∧ M.Dep (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
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E