feat(Data/Finset/Card): add image_iterate_stabilises_{lt,le}_card

Author: b-mehta

Mathlib/Data/Finset/Card.lean

@@ -910,4 +910,45 @@ 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 : g 0 = s := by simp [g]
+  have (i : ℕ) : #(g i) ≠ 0 := by simp [g, hs₀.ne_empty]
+  let G (i : ℕ) : ℕ := #(g i) - 1
+  have hg (i : ℕ) : g (i + 1) ⊆ g i := by
+    simp only [g]
+    rw [Function.iterate_succ, ← image_image]
+    exact image_subset_image hs.finsetImage_subset
+  replace hg : Antitone g := antitone_nat_of_succ_le hg
+  have G_eq (i j : ℕ) : G i = G j ↔ 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 G := fun i j h ↦ by simp only [G]; gcongr #?_ - 1; exact hg h
+  have hG₁ (m : ℕ) : G m = G (m + 1) → G (m + 1) = G (m + 2) := by
+    simp only [G_eq, g, Function.iterate_succ', ← image_image]
+    grind
+  obtain ⟨n, hn, hn'⟩ := Nat.stabilises_of_antitone hG hG₁
+  exact ⟨n, by grind, 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