simpa [inter_eq_self_of_subset_right hKC] using hC.contract_circuit (diff_ssubset hKC hK)
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hC : M.Circuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ (M ／ (C \ K)).Circuit K
no goals