simp only [diff_inter_self_eq_diff] at h'
α : 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)
α : 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)
⊢ (M ／ C).Dep (K \ C)