rw [mapEquiv_eq_map, map_circuit_iff]
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (M.mapEquiv f).Circuit C ↔ M.Circuit (⇑f.symm '' C)
α : 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)