exact ⟨by rintro ⟨C, hC, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
α : 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)
no goals