exact iff_of_false (fun h ↦ hD h.subset_ground) (by simp [hD])
case neg
α : 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