simp only [Dep, circuitOn_indep_iff hC, ssubset_iff_subset_ne, ne_eq, not_and, not_not,
  circuitOn_ground]
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (circuitOn C).Dep D ↔ D = C
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (D ⊆ C → D = C) ∧ D ⊆ C ↔ D = C