rw [circuit_iff_forall_ssubset, hCi.contract_dep_iff, and_iff_right (disjoint_sdiff_left),
  diff_union_self, union_eq_self_of_subset_right hC.subset, and_iff_right hK.dep]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ (M ／ C).Circuit (K \ C)
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ ∀ ⦃I : Set α⦄, I ⊂ K \ C → (M ／ C).Indep I