From 995c25cb9962967328d2ac33a0f46ebfe7a3d897 Mon Sep 17 00:00:00 2001
From: Joseph Myers <jsm@polyomino.org.uk>
Date: Wed, 20 Nov 2024 08:15:52 +0000
Subject: [PATCH] feat(Data/Nat/Nth): `nth_mem_anti` (#19169)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add another lemma for working with `Nat.nth`:

```lean
lemma nth_mem_anti {a b : ℕ} (hab : a ≤ b) (h : p (nth p b)) : p (nth p a) := by
```

Feel free to golf if you see a simpler way of proving this.
---
 Mathlib/Data/Nat/Nth.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index fe2658ba4d808..4cde210602f99 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -252,6 +252,18 @@ theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a
   · rcases subset_range_nth ha with ⟨n, rfl⟩
     rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h
 
+lemma nth_mem_anti {a b : ℕ} (hab : a ≤ b) (h : p (nth p b)) : p (nth p a) := by
+  by_cases h' : ∀ hf : (setOf p).Finite, a < #hf.toFinset
+  · exact nth_mem a h'
+  · simp only [not_forall, not_lt] at h'
+    have h'b : ∃ hf : (setOf p).Finite, #hf.toFinset ≤ b := by
+      rcases h' with ⟨hf, ha⟩
+      exact ⟨hf, ha.trans hab⟩
+    have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']
+    have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]
+    rw [ha0]
+    rwa [hb0] at h
+
 section Count
 
 variable (p) [DecidablePred p]