have h' := hK.contract_circuit (C := C ∩ K) (inter_subset_right.ssubset_of_ne (by simpa))
α : 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
C : Set α
hKC : ¬K ⊆ C
⊢ (M ／ C).Dep (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
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ (C ∩ K))
⊢ (M ／ C).Dep (K \ C)