rwa [and_iff_left Subset.rfl, h, iff_true_intro (circuitOn_ground_circuit hCne), true_iff] at h'
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
h' : (M ↾ C).Circuit C ↔ M.Circuit C ∧ C ⊆ C
⊢ M.Circuit C
no goals