feat: @[simp] Nat.count / Nat.nth of fun _ ↦ True, False (#13378)

Co-authored-by: L Lllvvuu <git@llllvvuu.dev>

Author: llllvvuu

Mathlib/Data/Nat/Count.lean

@@ -146,6 +146,19 @@ theorem count_lt_card {n : ℕ} (hp : (setOf p).Finite) (hpn : p n) : count p n
   (count_lt_count_succ_iff.2 hpn).trans_le (count_le_card hp _)
 #align nat.count_lt_card Nat.count_lt_card
 
+theorem count_of_forall {n : ℕ} (hp : ∀ n' < n, p n') : count p n = n := by
+  rw [count_eq_card_filter_range, filter_true_of_mem, card_range]
+  · simpa only [Finset.mem_range]
+
+@[simp] theorem count_true (n : ℕ) : count (fun _ ↦ True) n = n := count_of_forall fun _ _ ↦ trivial
+
+theorem count_of_forall_not {n : ℕ} (hp : ∀ n' < n, ¬p n') : count p n = 0 := by
+  rw [count_eq_card_filter_range, filter_false_of_mem, card_empty]
+  · simpa only [Finset.mem_range]
+
+@[simp] theorem count_false (n : ℕ) : count (fun _ ↦ False) n = 0 :=
+  count_of_forall_not fun _ _ ↦ id
+
 variable {q : ℕ → Prop}
 variable [DecidablePred q]
 

Mathlib/Data/Nat/Nth.lean

@@ -413,4 +413,20 @@ theorem lt_nth_iff_count_lt (hp : (setOf p).Infinite) {a b : ℕ} : a < count p
 
 end Count
 
+theorem nth_of_forall {n : ℕ} (hp : ∀ n' ≤ n, p n') : nth p n = n := by
+  classical nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]
+
+@[simp] theorem nth_true (n : ℕ) : nth (fun _ ↦ True) n = n := nth_of_forall fun _ _ ↦ trivial
+
+theorem nth_of_forall_not {n : ℕ} (hp : ∀ n' ≥ n, ¬p n') : nth p n = 0 := by
+  have : setOf p ⊆ Finset.range n := by
+    intro n' hn'
+    contrapose! hp
+    exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩
+  rw [nth_of_card_le ((finite_toSet _).subset this)]
+  · refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)
+    exact Set.Finite.toFinset_subset.mpr this
+
+@[simp] theorem nth_false (n : ℕ) : nth (fun _ ↦ False) n = 0 := nth_of_forall_not fun _ _ ↦ id
+
 end Nat