exact circuitOn_ground_circuit M.ground_nonempty
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ (circuitOn M.E).Circuit (circuitOn M.E).E
no goals