rw [and_comm, ← and_assoc, and_congr_left_iff, and_comm, and_congr_right_iff]
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ ((M.Dep C ∧ Disjoint C D) ∧ ∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔
    (M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C) ∧ Disjoint C D
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ Disjoint C D →
    M.Dep C → ((∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C)