rintro ⟨C, hC, rfl⟩
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) → M.Circuit (⇑f.symm '' C)
case intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α ≃ β
C : Set α
hC : M.Circuit C
⊢ M.Circuit (⇑f.symm '' (⇑f '' C))