Theorem: Matroid.circuitOn_ground_circuit (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
⊢ (circuitOn C).Circuit C
Tactic:
simp [circuit_iff_forall_ssubset, circuitOn_dep_iff hC, circuitOn_indep_iff hC]
State after:
no goals