rw [restrict_circuit_iff h.subset_ground, circuitOn_circuit_iff h.nonempty,
  and_iff_left (show C' ⊆ C from hC')]
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ (M ↾ C).Circuit C' ↔ (circuitOn C).Circuit C'
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ M.Circuit C' ↔ C' = C