by_cases hD : D ⊆ E
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
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

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