feat: f '' s = f ⁻¹' s for an involution f (#27746)

Author: j-loreaux

Mathlib/Data/Set/Image.lean

@@ -351,6 +351,10 @@ theorem image_eq_preimage_of_inverse {f : α → β} {g : β → α} (h₁ : Lef
   funext fun s =>
     Subset.antisymm (image_subset_preimage_of_inverse h₁ s) (preimage_subset_image_of_inverse h₂ s)
 
+theorem _root_.Function.Involutive.image_eq_preimage {f : α → α} (hf : f.Involutive) :
+    image f = preimage f :=
+  image_eq_preimage_of_inverse hf.leftInverse hf.rightInverse
+
 theorem mem_image_iff_of_inverse {f : α → β} {g : β → α} {b : β} {s : Set α} (h₁ : LeftInverse g f)
     (h₂ : RightInverse g f) : b ∈ f '' s ↔ g b ∈ s := by
   rw [image_eq_preimage_of_inverse h₁ h₂]; rfl