feat(Data/Finset/Card): iterating a function's image on a finite set stabilises (leanprover-community#38488)

...and does so in a bounded number of steps (which is why this is Finset-specific).
In a later PR, I'll add this for endofunctions on a fintype, as well as add a Set.Finite version.

Author: b-mehta

Mathlib/Data/Finset/Card.lean

@@ -932,4 +932,38 @@ theorem eraseInduction [DecidableEq α] {p : Finset α → Prop}
     (H : (S : Finset α) → (∀ s ∈ S, p (S.erase s)) → p S) (S : Finset α) : p S :=
   S.strongInduction fun S ih => H S fun _ hs => ih _ (erase_ssubset hs)
 
+/--
+Given a function `f` which sends the finite set `s` to itself, the sequence of images of `s` under
+iterates of `f` is eventually constant. Furthermore, the sequence of images stabilises in fewer
+than `#s` steps.
+-/
+theorem image_iterate_stabilises_lt_card [DecidableEq α] {f : α → α} {s : Finset α}
+    (hs : Set.MapsTo f s s) (hs₀ : s.Nonempty) :
+    ∃ n < #s, ∀ m, n ≤ m → s.image f^[m] = s.image f^[n] := by
+  let g (i : ℕ) : Finset α := s.image f^[i]
+  have (i : ℕ) : 0 < #(g i) := (hs₀.image _).card_pos
+  have hg : Antitone g := antitone_nat_of_succ_le <| fun i ↦ by
+    simp_rw [g, Function.iterate_succ, ← image_image]
+    grw [hs.finsetImage_subset]
+  have eq_iff (i j : ℕ) : #(g i) - 1 = #(g j) - 1 ↔ g i = g j := by
+    wlog hij : j ≤ i generalizing i j
+    · grind
+    exact ⟨fun h ↦ eq_of_subset_of_card_le (hg hij) (by grind), by grind⟩
+  have hG : Antitone (fun i ↦ #(g i) - 1) := fun i j h ↦ by dsimp; gcongr #?_ - 1; exact hg h
+  rcases Nat.stabilises_of_antitone hG (by grind [=_ image_image, iterate_succ']) with ⟨n, hn, hn'⟩
+  exact ⟨n, by grind⟩
+
+/--
+Given a function `f` which sends the finite set `s` to itself, the sequence of images of `s` under
+iterates of `f` is eventually constant. Furthermore, the sequence of images stabilises in at most
+`#s` steps.
+-/
+theorem image_iterate_stabilises_le_card [DecidableEq α] {f : α → α} {s : Finset α}
+    (hs : Set.MapsTo f s s) :
+    ∃ n ≤ #s, ∀ m, n ≤ m → s.image f^[m] = s.image f^[n] := by
+  obtain rfl | hs₀ := s.eq_empty_or_nonempty
+  · simp
+  obtain ⟨n, hn', hn⟩ := image_iterate_stabilises_lt_card hs hs₀
+  exact ⟨n, hn'.le, hn⟩
+
 end Finset

Mathlib/Data/Finset/Image.lean

@@ -403,6 +403,7 @@ theorem _root_.Function.Commute.finset_image [DecidableEq α] {f g : α → α}
     (h : Function.Commute f g) : Function.Commute (image f) (image g) :=
   Function.Semiconj.finset_image h
 
+@[gcongr]
 theorem image_subset_image {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f := by
   simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]