Theorem: Matroid.Circuit.contract_diff_circuit (Matroid/Minor/Basic.lean)

State before:
α : 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
Tactic:
simpa [inter_eq_self_of_subset_right hKC] using hC.contract_circuit (diff_ssubset hKC hK)
State after:
no goals