simp (config := {contextual := true}) [← not_indep_iff (M := uniqueBaseOn I E) hD, hD,
  nonempty_iff_ne_empty, not_imp_not]
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
no goals