From 6f642abe7057f95ad364fab04d4a9778bda29c95 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 21 Oct 2024 17:51:23 +1100
Subject: [PATCH] feat: Nat.forall_lt_succ and variants (#5785)

---
 src/Init/Data/Nat/Lemmas.lean | 71 +++++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)

diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 76caf3f1b886..0aa6a9ae9e72 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -32,6 +32,77 @@ namespace Nat
 @[simp] theorem exists_add_one_eq : (∃ n, n + 1 = a) ↔ 0 < a :=
   ⟨fun ⟨n, h⟩ => by omega, fun h => ⟨a - 1, by omega⟩⟩
 
+/-- Dependent variant of `forall_lt_succ_right`. -/
+theorem forall_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega) := by
+  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
+  constructor
+  · intro w
+    constructor
+    · intro m h
+      exact w _ (.inl h)
+    · exact w _ (.inr rfl)
+  · rintro w m (h|rfl)
+    · exact w.1 _ h
+    · exact w.2
+
+/-- See `forall_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
+theorem forall_lt_succ_right {p : Nat → Prop} :
+    (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n := by
+  simpa using forall_lt_succ_right' (p := fun m _ => p m)
+
+/-- Dependent variant of `forall_lt_succ_left`. -/
+theorem forall_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∀ m (h : m < n + 1), p m h) ↔ p 0 (by omega) ∧ (∀ m (h : m < n), p (m + 1) (by omega)) := by
+  constructor
+  · intro w
+    constructor
+    · exact w 0 (by omega)
+    · intro m h
+      exact w (m + 1) (by omega)
+  · rintro ⟨h₀, h₁⟩ m h
+    cases m with
+    | zero => exact h₀
+    | succ m => exact h₁ m (by omega)
+
+/-- See `forall_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
+theorem forall_lt_succ_left {p : Nat → Prop} :
+    (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1)) := by
+  simpa using forall_lt_succ_left' (p := fun m _ => p m)
+
+/-- Dependent variant of `exists_lt_succ_right`. -/
+theorem exists_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega) := by
+  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
+  constructor
+  · rintro ⟨m, (h|rfl), w⟩
+    · exact .inl ⟨m, h, w⟩
+    · exact .inr w
+  · rintro (⟨m, h, w⟩ | w)
+    · exact ⟨m, by omega, w⟩
+    · exact ⟨n, by omega, w⟩
+
+/-- See `exists_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
+theorem exists_lt_succ_right {p : Nat → Prop} :
+    (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n := by
+  simpa using exists_lt_succ_right' (p := fun m _ => p m)
+
+/-- Dependent variant of `exists_lt_succ_left`. -/
+theorem exists_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega)) := by
+  constructor
+  · rintro ⟨_|m, h, w⟩
+    · exact .inl w
+    · exact .inr ⟨m, by omega, w⟩
+  · rintro (w|⟨m, h, w⟩)
+    · exact ⟨0, by omega, w⟩
+    · exact ⟨m + 1, by omega, w⟩
+
+/-- See `exists_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
+theorem exists_lt_succ_left {p : Nat → Prop} :
+    (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1)) := by
+  simpa using exists_lt_succ_left' (p := fun m _ => p m)
+
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by