rintro rfl
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
C' : Set α
⊢ C' = C → (circuitOn C).Circuit C'
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C' : Set α
hC : C'.Nonempty
⊢ (circuitOn C').Circuit C'