rw [diff_empty]
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl (C \ ∅)
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl C