From 3de1122c81495b6f5303ba37ac3daa5452e7653b Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 13 Jun 2023 22:41:48 -0500
Subject: [PATCH 1/9] feat: port Data.Nat.Nth


From c55dc7cd16c10cdeae29d6625c58913a8a0354a2 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 13 Jun 2023 22:41:48 -0500
Subject: [PATCH 2/9] Initial file copy from mathport

---
 Mathlib/Data/Nat/Nth.lean | 434 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 434 insertions(+)
 create mode 100644 Mathlib/Data/Nat/Nth.lean

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
new file mode 100644
index 0000000000000..451cd46b03eae
--- /dev/null
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -0,0 +1,434 @@
+/-
+Copyright (c) 2021 Vladimir Goryachev. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Vladimir Goryachev, Kyle Miller, Scott Morrison, Eric Rodriguez
+
+! This file was ported from Lean 3 source module data.nat.nth
+! leanprover-community/mathlib commit 7fdd4f3746cb059edfdb5d52cba98f66fce418c0
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Data.Nat.Count
+import Mathbin.Data.Set.Intervals.Monotone
+import Mathbin.Order.OrderIsoNat
+
+/-!
+# The `n`th Number Satisfying a Predicate
+
+This file defines a function for "what is the `n`th number that satisifies a given predicate `p`",
+and provides lemmas that deal with this function and its connection to `nat.count`.
+
+## Main definitions
+
+* `nat.nth p n`: The `n`-th natural `k` (zero-indexed) such that `p k`. If there is no
+  such natural (that is, `p` is true for at most `n` naturals), then `nat.nth p n = 0`.
+
+## Main results
+
+* `nat.nth_set_card`: For a fintely-often true `p`, gives the cardinality of the set of numbers
+  satisfying `p` above particular values of `nth p`
+* `nat.count_nth_gc`: Establishes a Galois connection between `nat.nth p` and `nat.count p`.
+* `nat.nth_eq_order_iso_of_nat`: For an infinitely-ofter true predicate, `nth` agrees with the
+  order-isomorphism of the subtype to the natural numbers.
+
+There has been some discussion on the subject of whether both of `nth` and
+`nat.subtype.order_iso_of_nat` should exist. See discussion
+[here](https://github.com/leanprover-community/mathlib/pull/9457#pullrequestreview-767221180).
+Future work should address how lemmas that use these should be written.
+
+-/
+
+
+open Finset
+
+namespace Nat
+
+variable (p : ℕ → Prop)
+
+/-- Find the `n`-th natural number satisfying `p` (indexed from `0`, so `nth p 0` is the first
+natural number satisfying `p`), or `0` if there is no such number. See also
+`subtype.order_iso_of_nat` for the order isomorphism with ℕ when `p` is infinitely often true. -/
+noncomputable def nth (p : ℕ → Prop) (n : ℕ) : ℕ := by
+  classical exact
+    if h : Set.Finite (setOf p) then (h.to_finset.sort (· ≤ ·)).getD n 0
+    else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n
+#align nat.nth Nat.nth
+
+variable {p}
+
+/-!
+### Lemmas about `nat.nth` on a finite set
+-/
+
+
+theorem nth_of_card_le (hf : (setOf p).Finite) {n : ℕ} (hn : hf.toFinset.card ≤ n) : nth p n = 0 :=
+  by rw [nth, dif_pos hf, List.getD_eq_default]; rwa [Finset.length_sort]
+#align nat.nth_of_card_le Nat.nth_of_card_le
+
+theorem nth_eq_getD_sort (h : (setOf p).Finite) (n : ℕ) :
+    nth p n = (h.toFinset.sort (· ≤ ·)).getD n 0 :=
+  dif_pos h
+#align nat.nth_eq_nthd_sort Nat.nth_eq_getD_sort
+
+theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < hf.toFinset.card) :
+    nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩ := by
+  rw [nth_eq_nthd_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_nthLe]; rfl
+#align nat.nth_eq_order_emb_of_fin Nat.nth_eq_orderEmbOfFin
+
+theorem nth_strictMonoOn (hf : (setOf p).Finite) :
+    StrictMonoOn (nth p) (Set.Iio hf.toFinset.card) :=
+  by
+  rintro m (hm : m < _) n (hn : n < _) h
+  simp only [nth_eq_order_emb_of_fin, *]
+  exact OrderEmbedding.strictMono _ h
+#align nat.nth_strict_mono_on Nat.nth_strictMonoOn
+
+theorem nth_lt_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : m < n)
+    (hn : n < hf.toFinset.card) : nth p m < nth p n :=
+  nth_strictMonoOn hf (h.trans hn) hn h
+#align nat.nth_lt_nth_of_lt_card Nat.nth_lt_nth_of_lt_card
+
+theorem nth_le_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : m ≤ n)
+    (hn : n < hf.toFinset.card) : nth p m ≤ nth p n :=
+  (nth_strictMonoOn hf).MonotoneOn (h.trans_lt hn) hn h
+#align nat.nth_le_nth_of_lt_card Nat.nth_le_nth_of_lt_card
+
+theorem lt_of_nth_lt_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : nth p m < nth p n)
+    (hm : m < hf.toFinset.card) : m < n :=
+  not_le.1 fun hle => h.not_le <| nth_le_nth_of_lt_card hf hle hm
+#align nat.lt_of_nth_lt_nth_of_lt_card Nat.lt_of_nth_lt_nth_of_lt_card
+
+theorem le_of_nth_le_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : nth p m ≤ nth p n)
+    (hm : m < hf.toFinset.card) : m ≤ n :=
+  not_lt.1 fun hlt => h.not_lt <| nth_lt_nth_of_lt_card hf hlt hm
+#align nat.le_of_nth_le_nth_of_lt_card Nat.le_of_nth_le_nth_of_lt_card
+
+theorem nth_injOn (hf : (setOf p).Finite) : (Set.Iio hf.toFinset.card).InjOn (nth p) :=
+  (nth_strictMonoOn hf).InjOn
+#align nat.nth_inj_on Nat.nth_injOn
+
+theorem range_nth_of_finite (hf : (setOf p).Finite) : Set.range (nth p) = insert 0 (setOf p) := by
+  simpa only [← nth_eq_nthd_sort hf, mem_sort, Set.Finite.mem_toFinset] using
+    Set.range_list_getD (hf.to_finset.sort (· ≤ ·)) 0
+#align nat.range_nth_of_finite Nat.range_nth_of_finite
+
+@[simp]
+theorem image_nth_Iio_card (hf : (setOf p).Finite) : nth p '' Set.Iio hf.toFinset.card = setOf p :=
+  calc
+    nth p '' Set.Iio hf.toFinset.card = Set.range (hf.toFinset.orderEmbOfFin rfl) := by
+      ext x <;>
+        simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_order_emb_of_fin hf,
+          Set.mem_Iio, exists_prop]
+    _ = setOf p := by rw [range_order_emb_of_fin, Set.Finite.coe_toFinset]
+#align nat.image_nth_Iio_card Nat.image_nth_Iio_card
+
+theorem nth_mem_of_lt_card {n : ℕ} (hf : (setOf p).Finite) (hlt : n < hf.toFinset.card) :
+    p (nth p n) :=
+  (image_nth_Iio_card hf).Subset <| Set.mem_image_of_mem _ hlt
+#align nat.nth_mem_of_lt_card Nat.nth_mem_of_lt_card
+
+theorem exists_lt_card_finite_nth_eq (hf : (setOf p).Finite) {x} (h : p x) :
+    ∃ n, n < hf.toFinset.card ∧ nth p n = x := by
+  rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h 
+#align nat.exists_lt_card_finite_nth_eq Nat.exists_lt_card_finite_nth_eq
+
+/-!
+### Lemmas about `nat.nth` on an infinite set
+-/
+
+
+/-- When `s` is an infinite set, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
+theorem nth_apply_eq_orderIsoOfNat (hf : (setOf p).Infinite) (n : ℕ) :
+    nth p n = @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype n := by rw [nth, dif_neg hf]
+#align nat.nth_apply_eq_order_iso_of_nat Nat.nth_apply_eq_orderIsoOfNat
+
+/-- When `s` is an infinite set, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
+theorem nth_eq_orderIsoOfNat (hf : (setOf p).Infinite) :
+    nth p = coe ∘ @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype :=
+  funext <| nth_apply_eq_orderIsoOfNat hf
+#align nat.nth_eq_order_iso_of_nat Nat.nth_eq_orderIsoOfNat
+
+theorem nth_strictMono (hf : (setOf p).Infinite) : StrictMono (nth p) :=
+  by
+  rw [nth_eq_order_iso_of_nat hf]
+  exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
+#align nat.nth_strict_mono Nat.nth_strictMono
+
+theorem nth_injective (hf : (setOf p).Infinite) : Function.Injective (nth p) :=
+  (nth_strictMono hf).Injective
+#align nat.nth_injective Nat.nth_injective
+
+theorem nth_monotone (hf : (setOf p).Infinite) : Monotone (nth p) :=
+  (nth_strictMono hf).Monotone
+#align nat.nth_monotone Nat.nth_monotone
+
+theorem nth_lt_nth (hf : (setOf p).Infinite) {k n} : nth p k < nth p n ↔ k < n :=
+  (nth_strictMono hf).lt_iff_lt
+#align nat.nth_lt_nth Nat.nth_lt_nth
+
+theorem nth_le_nth (hf : (setOf p).Infinite) {k n} : nth p k ≤ nth p n ↔ k ≤ n :=
+  (nth_strictMono hf).le_iff_le
+#align nat.nth_le_nth Nat.nth_le_nth
+
+theorem range_nth_of_infinite (hf : (setOf p).Infinite) : Set.range (nth p) = setOf p :=
+  by
+  rw [nth_eq_order_iso_of_nat hf]
+  haveI := hf.to_subtype
+  exact Nat.Subtype.coe_comp_ofNat_range
+#align nat.range_nth_of_infinite Nat.range_nth_of_infinite
+
+theorem nth_mem_of_infinite (hf : (setOf p).Infinite) (n : ℕ) : p (nth p n) :=
+  Set.range_subset_iff.1 (range_nth_of_infinite hf).le n
+#align nat.nth_mem_of_infinite Nat.nth_mem_of_infinite
+
+/-!
+### Lemmas that work for finite and infinite sets
+-/
+
+
+theorem exists_lt_card_nth_eq {x} (h : p x) :
+    ∃ n, (∀ hf : (setOf p).Finite, n < hf.toFinset.card) ∧ nth p n = x :=
+  by
+  refine' (setOf p).finite_or_infinite.elim (fun hf => _) fun hf => _
+  · rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
+    exact ⟨n, fun hf' => hn, hx⟩
+  · rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h 
+    rcases h with ⟨n, hx⟩
+    exact ⟨n, fun hf' => absurd hf' hf, hx⟩
+#align nat.exists_lt_card_nth_eq Nat.exists_lt_card_nth_eq
+
+theorem subset_range_nth : setOf p ⊆ Set.range (nth p) := fun x (hx : p x) =>
+  let ⟨n, _, hn⟩ := exists_lt_card_nth_eq hx
+  ⟨n, hn⟩
+#align nat.subset_range_nth Nat.subset_range_nth
+
+theorem range_nth_subset : Set.range (nth p) ⊆ insert 0 (setOf p) :=
+  (setOf p).finite_or_infinite.elim (fun h => (range_nth_of_finite h).Subset) fun h =>
+    (range_nth_of_infinite h).trans_subset (Set.subset_insert _ _)
+#align nat.range_nth_subset Nat.range_nth_subset
+
+theorem nth_mem (n : ℕ) (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) : p (nth p n) :=
+  (setOf p).finite_or_infinite.elim (fun hf => nth_mem_of_lt_card hf (h hf)) fun h =>
+    nth_mem_of_infinite h n
+#align nat.nth_mem Nat.nth_mem
+
+theorem nth_lt_nth' {m n : ℕ} (hlt : m < n) (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
+    nth p m < nth p n :=
+  (setOf p).finite_or_infinite.elim (fun hf => nth_lt_nth_of_lt_card hf hlt (h _)) fun hf =>
+    (nth_lt_nth hf).2 hlt
+#align nat.nth_lt_nth' Nat.nth_lt_nth'
+
+theorem nth_le_nth' {m n : ℕ} (hle : m ≤ n) (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
+    nth p m ≤ nth p n :=
+  (setOf p).finite_or_infinite.elim (fun hf => nth_le_nth_of_lt_card hf hle (h _)) fun hf =>
+    (nth_le_nth hf).2 hle
+#align nat.nth_le_nth' Nat.nth_le_nth'
+
+theorem le_nth {n : ℕ} (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) : n ≤ nth p n :=
+  (setOf p).finite_or_infinite.elim
+    (fun hf => ((nth_strictMonoOn hf).mono <| Set.Iic_subset_Iio.2 (h _)).Iic_id_le _ le_rfl)
+    fun hf => (nth_strictMono hf).id_le _
+#align nat.le_nth Nat.le_nth
+
+theorem isLeast_nth {n} (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
+    IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
+  ⟨⟨nth_mem n h, fun k hk => nth_lt_nth' hk h⟩, fun x hx =>
+    let ⟨k, hk, hkx⟩ := exists_lt_card_nth_eq hx.1
+    (lt_or_le k n).elim (fun hlt => absurd hkx (hx.2 _ hlt).Ne) fun hle => hkx ▸ nth_le_nth' hle hk⟩
+#align nat.is_least_nth Nat.isLeast_nth
+
+theorem isLeast_nth_of_lt_card {n : ℕ} (hf : (setOf p).Finite) (hn : n < hf.toFinset.card) :
+    IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
+  isLeast_nth fun _ => hn
+#align nat.is_least_nth_of_lt_card Nat.isLeast_nth_of_lt_card
+
+theorem isLeast_nth_of_infinite (hf : (setOf p).Infinite) (n : ℕ) :
+    IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
+  isLeast_nth fun h => absurd h hf
+#align nat.is_least_nth_of_infinite Nat.isLeast_nth_of_infinite
+
+/-- An alternative recursive definition of `nat.nth`: `nat.nth s n` is the infimum of `x ∈ s` such
+that `nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
+nonempty because we use the same "garbage value" `0` both for `Inf` on `ℕ` and for `nat.nth s n` for
+`n ≥ card s`. -/
+theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} :=
+  by
+  by_cases hn : ∀ hf : (setOf p).Finite, n < hf.to_finset.card
+  · exact (is_least_nth hn).csInf_eq.symm
+  · push_neg at hn 
+    rcases hn with ⟨hf, hn⟩
+    rw [nth_of_card_le _ hn]
+    refine' ((congr_arg Inf <| Set.eq_empty_of_forall_not_mem fun k hk => _).trans sInf_empty).symm
+    rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
+    exact (hk.2 _ ((hlt hf).trans_le hn)).False
+#align nat.nth_eq_Inf Nat.nth_eq_sInf
+
+theorem nth_zero : nth p 0 = sInf (setOf p) := by rw [nth_eq_Inf]; simp
+#align nat.nth_zero Nat.nth_zero
+
+@[simp]
+theorem nth_zero_of_zero (h : p 0) : nth p 0 = 0 := by simp [nth_zero, h]
+#align nat.nth_zero_of_zero Nat.nth_zero_of_zero
+
+theorem nth_zero_of_exists [DecidablePred p] (h : ∃ n, p n) : nth p 0 = Nat.find h := by
+  rw [nth_zero]; convert Nat.sInf_def h
+#align nat.nth_zero_of_exists Nat.nth_zero_of_exists
+
+theorem nth_eq_zero {n} :
+    nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf : (setOf p).Finite, hf.toFinset.card ≤ n :=
+  by
+  refine' ⟨fun h => _, _⟩
+  · simp only [or_iff_not_imp_right, not_exists, not_le]
+    exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
+  · rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
+    exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]
+#align nat.nth_eq_zero Nat.nth_eq_zero
+
+theorem nth_eq_zero_mono (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p a = 0) : nth p b = 0 :=
+  by
+  simp only [nth_eq_zero, h₀, false_and_iff, false_or_iff] at ha ⊢
+  exact ha.imp fun hf hle => hle.trans hab
+#align nat.nth_eq_zero_mono Nat.nth_eq_zero_mono
+
+theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a ≤ nth p k :=
+  by
+  cases' (setOf p).finite_or_infinite with hf hf
+  · rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
+    cases' lt_or_le (k + 1) hf.to_finset.card with hk hk
+    ·
+      rwa [(nth_strict_mono_on hf).lt_iff_lt hn hk, lt_succ_iff, ←
+        (nth_strict_mono_on hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h 
+    · rw [nth_of_card_le _ hk] at h 
+      exact absurd h (zero_le _).not_lt
+  · rcases subset_range_nth ha with ⟨n, rfl⟩
+    rwa [nth_lt_nth hf, lt_succ_iff, ← nth_le_nth hf] at h 
+#align nat.le_nth_of_lt_nth_succ Nat.le_nth_of_lt_nth_succ
+
+section Count
+
+variable (p) [DecidablePred p]
+
+@[simp]
+theorem count_nth_zero : count p (nth p 0) = 0 :=
+  by
+  rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
+  exact fun n h₁ h₂ => (mem_range.1 h₁).not_le (Nat.sInf_le h₂)
+#align nat.count_nth_zero Nat.count_nth_zero
+
+theorem filter_range_nth_subset_insert (k : ℕ) :
+    (range (nth p (k + 1))).filterₓ p ⊆ insert (nth p k) ((range (nth p k)).filterₓ p) :=
+  by
+  intro a ha
+  simp only [mem_insert, mem_filter, mem_range] at ha ⊢
+  exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩
+#align nat.filter_range_nth_subset_insert Nat.filter_range_nth_subset_insert
+
+variable {p}
+
+theorem filter_range_nth_eq_insert {k : ℕ}
+    (hlt : ∀ hf : (setOf p).Finite, k + 1 < hf.toFinset.card) :
+    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) :=
+  by
+  refine' (filter_range_nth_subset_insert p k).antisymm fun a ha => _
+  simp only [mem_insert, mem_filter, mem_range] at ha ⊢
+  have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
+  rcases ha with (rfl | ⟨hlt, hpa⟩)
+  · exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩
+  · exact ⟨hlt.trans this, hpa⟩
+#align nat.filter_range_nth_eq_insert Nat.filter_range_nth_eq_insert
+
+theorem filter_range_nth_eq_insert_of_finite (hf : (setOf p).Finite) {k : ℕ}
+    (hlt : k + 1 < hf.toFinset.card) :
+    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) :=
+  filter_range_nth_eq_insert fun _ => hlt
+#align nat.filter_range_nth_eq_insert_of_finite Nat.filter_range_nth_eq_insert_of_finite
+
+theorem filter_range_nth_eq_insert_of_infinite (hp : (setOf p).Infinite) (k : ℕ) :
+    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) :=
+  filter_range_nth_eq_insert fun hf => absurd hf hp
+#align nat.filter_range_nth_eq_insert_of_infinite Nat.filter_range_nth_eq_insert_of_infinite
+
+theorem count_nth {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
+    count p (nth p n) = n := by
+  induction' n with k ihk
+  · exact count_nth_zero _
+  · rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_not_mem, ←
+      count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]
+    simp
+#align nat.count_nth Nat.count_nth
+
+theorem count_nth_of_lt_card_finite {n : ℕ} (hp : (setOf p).Finite) (hlt : n < hp.toFinset.card) :
+    count p (nth p n) = n :=
+  count_nth fun _ => hlt
+#align nat.count_nth_of_lt_card_finite Nat.count_nth_of_lt_card_finite
+
+theorem count_nth_of_infinite (hp : (setOf p).Infinite) (n : ℕ) : count p (nth p n) = n :=
+  count_nth fun hf => absurd hf hp
+#align nat.count_nth_of_infinite Nat.count_nth_of_infinite
+
+theorem count_nth_succ {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
+    count p (nth p n + 1) = n + 1 := by rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
+#align nat.count_nth_succ Nat.count_nth_succ
+
+@[simp]
+theorem nth_count {n : ℕ} (hpn : p n) : nth p (count p n) = n :=
+  have : ∀ hf : (setOf p).Finite, count p n < hf.toFinset.card := fun hf => count_lt_card hf hpn
+  count_injective (nth_mem _ this) hpn (count_nth this)
+#align nat.nth_count Nat.nth_count
+
+theorem nth_lt_of_lt_count {n k : ℕ} (h : k < count p n) : nth p k < n :=
+  by
+  refine' (count_monotone p).reflect_lt _
+  rwa [count_nth]
+  exact fun hf => h.trans_le (count_le_card hf n)
+#align nat.nth_lt_of_lt_count Nat.nth_lt_of_lt_count
+
+theorem le_nth_of_count_le {n k : ℕ} (h : n ≤ nth p k) : count p n ≤ k :=
+  not_lt.1 fun hlt => h.not_lt <| nth_lt_of_lt_count hlt
+#align nat.le_nth_of_count_le Nat.le_nth_of_count_le
+
+variable (p)
+
+theorem nth_count_eq_sInf (n : ℕ) : nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i} :=
+  by
+  refine' (nth_eq_Inf _ _).trans (congr_arg Inf _)
+  refine' Set.ext fun a => and_congr_right fun hpa => _
+  refine' ⟨fun h => not_lt.1 fun ha => _, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
+  have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
+  rwa [nth_count hpa, lt_self_iff_false] at hn 
+#align nat.nth_count_eq_Inf Nat.nth_count_eq_sInf
+
+variable {p}
+
+theorem le_nth_count' {n : ℕ} (hpn : ∃ k, p k ∧ n ≤ k) : n ≤ nth p (count p n) :=
+  (le_csInf hpn fun k => And.right).trans (nth_count_eq_sInf p n).ge
+#align nat.le_nth_count' Nat.le_nth_count'
+
+theorem le_nth_count (hp : (setOf p).Infinite) (n : ℕ) : n ≤ nth p (count p n) :=
+  let ⟨m, hp, hn⟩ := hp.exists_gt n
+  le_nth_count' ⟨m, hp, hn.le⟩
+#align nat.le_nth_count Nat.le_nth_count
+
+/-- If a predicate `p : ℕ → Prop` is true for infinitely many numbers, then `nat.count p` and
+`nat.nth p` form a Galois insertion. -/
+noncomputable def giCountNth (hp : (setOf p).Infinite) : GaloisInsertion (count p) (nth p) :=
+  GaloisInsertion.monotoneIntro (nth_monotone hp) (count_monotone p) (le_nth_count hp)
+    (count_nth_of_infinite hp)
+#align nat.gi_count_nth Nat.giCountNth
+
+theorem gc_count_nth (hp : (setOf p).Infinite) : GaloisConnection (count p) (nth p) :=
+  (giCountNth hp).gc
+#align nat.gc_count_nth Nat.gc_count_nth
+
+theorem count_le_iff_le_nth (hp : (setOf p).Infinite) {a b : ℕ} : count p a ≤ b ↔ a ≤ nth p b :=
+  gc_count_nth hp _ _
+#align nat.count_le_iff_le_nth Nat.count_le_iff_le_nth
+
+theorem lt_nth_iff_count_lt (hp : (setOf p).Infinite) {a b : ℕ} : a < count p b ↔ nth p a < b :=
+  (gc_count_nth hp).lt_iff_lt
+#align nat.lt_nth_iff_count_lt Nat.lt_nth_iff_count_lt
+
+end Count
+
+end Nat
+

From be491a4010c6f13e757905d133d1141b288db9d6 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 13 Jun 2023 22:41:48 -0500
Subject: [PATCH 3/9] automated fixes

Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
---
 Mathlib.lean              |  1 +
 Mathlib/Data/Nat/Nth.lean | 45 ++++++++++++++-------------------------
 2 files changed, 17 insertions(+), 29 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index e2ad3bd704738..d6d9d04bb4e8d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1486,6 +1486,7 @@ import Mathlib.Data.Nat.Lattice
 import Mathlib.Data.Nat.Log
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Nat.Multiplicity
+import Mathlib.Data.Nat.Nth
 import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Data.Nat.PSub
diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index 451cd46b03eae..f5ee964853c4f 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -8,9 +8,9 @@ Authors: Yaël Dillies, Vladimir Goryachev, Kyle Miller, Scott Morrison, Eric Ro
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Data.Nat.Count
-import Mathbin.Data.Set.Intervals.Monotone
-import Mathbin.Order.OrderIsoNat
+import Mathlib.Data.Nat.Count
+import Mathlib.Data.Set.Intervals.Monotone
+import Mathlib.Order.OrderIsoNat
 
 /-!
 # The `n`th Number Satisfying a Predicate
@@ -76,8 +76,7 @@ theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < hf.toFi
 #align nat.nth_eq_order_emb_of_fin Nat.nth_eq_orderEmbOfFin
 
 theorem nth_strictMonoOn (hf : (setOf p).Finite) :
-    StrictMonoOn (nth p) (Set.Iio hf.toFinset.card) :=
-  by
+    StrictMonoOn (nth p) (Set.Iio hf.toFinset.card) := by
   rintro m (hm : m < _) n (hn : n < _) h
   simp only [nth_eq_order_emb_of_fin, *]
   exact OrderEmbedding.strictMono _ h
@@ -148,8 +147,7 @@ theorem nth_eq_orderIsoOfNat (hf : (setOf p).Infinite) :
   funext <| nth_apply_eq_orderIsoOfNat hf
 #align nat.nth_eq_order_iso_of_nat Nat.nth_eq_orderIsoOfNat
 
-theorem nth_strictMono (hf : (setOf p).Infinite) : StrictMono (nth p) :=
-  by
+theorem nth_strictMono (hf : (setOf p).Infinite) : StrictMono (nth p) := by
   rw [nth_eq_order_iso_of_nat hf]
   exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
 #align nat.nth_strict_mono Nat.nth_strictMono
@@ -170,8 +168,7 @@ theorem nth_le_nth (hf : (setOf p).Infinite) {k n} : nth p k ≤ nth p n ↔ k 
   (nth_strictMono hf).le_iff_le
 #align nat.nth_le_nth Nat.nth_le_nth
 
-theorem range_nth_of_infinite (hf : (setOf p).Infinite) : Set.range (nth p) = setOf p :=
-  by
+theorem range_nth_of_infinite (hf : (setOf p).Infinite) : Set.range (nth p) = setOf p := by
   rw [nth_eq_order_iso_of_nat hf]
   haveI := hf.to_subtype
   exact Nat.Subtype.coe_comp_ofNat_range
@@ -187,8 +184,7 @@ theorem nth_mem_of_infinite (hf : (setOf p).Infinite) (n : ℕ) : p (nth p n) :=
 
 
 theorem exists_lt_card_nth_eq {x} (h : p x) :
-    ∃ n, (∀ hf : (setOf p).Finite, n < hf.toFinset.card) ∧ nth p n = x :=
-  by
+    ∃ n, (∀ hf : (setOf p).Finite, n < hf.toFinset.card) ∧ nth p n = x := by
   refine' (setOf p).finite_or_infinite.elim (fun hf => _) fun hf => _
   · rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
     exact ⟨n, fun hf' => hn, hx⟩
@@ -251,8 +247,7 @@ theorem isLeast_nth_of_infinite (hf : (setOf p).Infinite) (n : ℕ) :
 that `nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
 nonempty because we use the same "garbage value" `0` both for `Inf` on `ℕ` and for `nat.nth s n` for
 `n ≥ card s`. -/
-theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} :=
-  by
+theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} := by
   by_cases hn : ∀ hf : (setOf p).Finite, n < hf.to_finset.card
   · exact (is_least_nth hn).csInf_eq.symm
   · push_neg at hn 
@@ -275,8 +270,7 @@ theorem nth_zero_of_exists [DecidablePred p] (h : ∃ n, p n) : nth p 0 = Nat.fi
 #align nat.nth_zero_of_exists Nat.nth_zero_of_exists
 
 theorem nth_eq_zero {n} :
-    nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf : (setOf p).Finite, hf.toFinset.card ≤ n :=
-  by
+    nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf : (setOf p).Finite, hf.toFinset.card ≤ n := by
   refine' ⟨fun h => _, _⟩
   · simp only [or_iff_not_imp_right, not_exists, not_le]
     exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
@@ -284,14 +278,12 @@ theorem nth_eq_zero {n} :
     exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]
 #align nat.nth_eq_zero Nat.nth_eq_zero
 
-theorem nth_eq_zero_mono (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p a = 0) : nth p b = 0 :=
-  by
+theorem nth_eq_zero_mono (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p a = 0) : nth p b = 0 := by
   simp only [nth_eq_zero, h₀, false_and_iff, false_or_iff] at ha ⊢
   exact ha.imp fun hf hle => hle.trans hab
 #align nat.nth_eq_zero_mono Nat.nth_eq_zero_mono
 
-theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a ≤ nth p k :=
-  by
+theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a ≤ nth p k := by
   cases' (setOf p).finite_or_infinite with hf hf
   · rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
     cases' lt_or_le (k + 1) hf.to_finset.card with hk hk
@@ -309,15 +301,13 @@ section Count
 variable (p) [DecidablePred p]
 
 @[simp]
-theorem count_nth_zero : count p (nth p 0) = 0 :=
-  by
+theorem count_nth_zero : count p (nth p 0) = 0 := by
   rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
   exact fun n h₁ h₂ => (mem_range.1 h₁).not_le (Nat.sInf_le h₂)
 #align nat.count_nth_zero Nat.count_nth_zero
 
 theorem filter_range_nth_subset_insert (k : ℕ) :
-    (range (nth p (k + 1))).filterₓ p ⊆ insert (nth p k) ((range (nth p k)).filterₓ p) :=
-  by
+    (range (nth p (k + 1))).filterₓ p ⊆ insert (nth p k) ((range (nth p k)).filterₓ p) := by
   intro a ha
   simp only [mem_insert, mem_filter, mem_range] at ha ⊢
   exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩
@@ -327,8 +317,7 @@ variable {p}
 
 theorem filter_range_nth_eq_insert {k : ℕ}
     (hlt : ∀ hf : (setOf p).Finite, k + 1 < hf.toFinset.card) :
-    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) :=
-  by
+    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) := by
   refine' (filter_range_nth_subset_insert p k).antisymm fun a ha => _
   simp only [mem_insert, mem_filter, mem_range] at ha ⊢
   have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
@@ -376,8 +365,7 @@ theorem nth_count {n : ℕ} (hpn : p n) : nth p (count p n) = n :=
   count_injective (nth_mem _ this) hpn (count_nth this)
 #align nat.nth_count Nat.nth_count
 
-theorem nth_lt_of_lt_count {n k : ℕ} (h : k < count p n) : nth p k < n :=
-  by
+theorem nth_lt_of_lt_count {n k : ℕ} (h : k < count p n) : nth p k < n := by
   refine' (count_monotone p).reflect_lt _
   rwa [count_nth]
   exact fun hf => h.trans_le (count_le_card hf n)
@@ -389,8 +377,7 @@ theorem le_nth_of_count_le {n k : ℕ} (h : n ≤ nth p k) : count p n ≤ k :=
 
 variable (p)
 
-theorem nth_count_eq_sInf (n : ℕ) : nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i} :=
-  by
+theorem nth_count_eq_sInf (n : ℕ) : nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i} := by
   refine' (nth_eq_Inf _ _).trans (congr_arg Inf _)
   refine' Set.ext fun a => and_congr_right fun hpa => _
   refine' ⟨fun h => not_lt.1 fun ha => _, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩

From eddb3b248a7a4fad8f0daf3ceb827d43a2560f9a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 14 Jun 2023 08:27:18 -0500
Subject: [PATCH 4/9] Fix compile

---
 Mathlib/Data/Nat/Nth.lean | 88 +++++++++++++++++++--------------------
 1 file changed, 44 insertions(+), 44 deletions(-)

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index f5ee964853c4f..a209461f5d80d 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -50,7 +50,7 @@ natural number satisfying `p`), or `0` if there is no such number. See also
 `subtype.order_iso_of_nat` for the order isomorphism with ℕ when `p` is infinitely often true. -/
 noncomputable def nth (p : ℕ → Prop) (n : ℕ) : ℕ := by
   classical exact
-    if h : Set.Finite (setOf p) then (h.to_finset.sort (· ≤ ·)).getD n 0
+    if h : Set.Finite (setOf p) then (h.toFinset.sort (· ≤ ·)).getD n 0
     else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n
 #align nat.nth Nat.nth
 
@@ -72,13 +72,13 @@ theorem nth_eq_getD_sort (h : (setOf p).Finite) (n : ℕ) :
 
 theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < hf.toFinset.card) :
     nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩ := by
-  rw [nth_eq_nthd_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_nthLe]; rfl
+  rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_get]; rfl
 #align nat.nth_eq_order_emb_of_fin Nat.nth_eq_orderEmbOfFin
 
 theorem nth_strictMonoOn (hf : (setOf p).Finite) :
     StrictMonoOn (nth p) (Set.Iio hf.toFinset.card) := by
   rintro m (hm : m < _) n (hn : n < _) h
-  simp only [nth_eq_order_emb_of_fin, *]
+  simp only [nth_eq_orderEmbOfFin, *]
   exact OrderEmbedding.strictMono _ h
 #align nat.nth_strict_mono_on Nat.nth_strictMonoOn
 
@@ -89,7 +89,7 @@ theorem nth_lt_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : m < n)
 
 theorem nth_le_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : m ≤ n)
     (hn : n < hf.toFinset.card) : nth p m ≤ nth p n :=
-  (nth_strictMonoOn hf).MonotoneOn (h.trans_lt hn) hn h
+  (nth_strictMonoOn hf).monotoneOn (h.trans_lt hn) hn h
 #align nat.nth_le_nth_of_lt_card Nat.nth_le_nth_of_lt_card
 
 theorem lt_of_nth_lt_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : nth p m < nth p n)
@@ -103,39 +103,38 @@ theorem le_of_nth_le_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : nth
 #align nat.le_of_nth_le_nth_of_lt_card Nat.le_of_nth_le_nth_of_lt_card
 
 theorem nth_injOn (hf : (setOf p).Finite) : (Set.Iio hf.toFinset.card).InjOn (nth p) :=
-  (nth_strictMonoOn hf).InjOn
+  (nth_strictMonoOn hf).injOn
 #align nat.nth_inj_on Nat.nth_injOn
 
 theorem range_nth_of_finite (hf : (setOf p).Finite) : Set.range (nth p) = insert 0 (setOf p) := by
-  simpa only [← nth_eq_nthd_sort hf, mem_sort, Set.Finite.mem_toFinset] using
-    Set.range_list_getD (hf.to_finset.sort (· ≤ ·)) 0
+  simpa only [← nth_eq_getD_sort hf, mem_sort, Set.Finite.mem_toFinset]
+    using Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0
 #align nat.range_nth_of_finite Nat.range_nth_of_finite
 
 @[simp]
 theorem image_nth_Iio_card (hf : (setOf p).Finite) : nth p '' Set.Iio hf.toFinset.card = setOf p :=
   calc
     nth p '' Set.Iio hf.toFinset.card = Set.range (hf.toFinset.orderEmbOfFin rfl) := by
-      ext x <;>
-        simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_order_emb_of_fin hf,
-          Set.mem_Iio, exists_prop]
-    _ = setOf p := by rw [range_order_emb_of_fin, Set.Finite.coe_toFinset]
+      ext x
+      simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf,
+        Set.mem_Iio, exists_prop]
+    _ = setOf p := by rw [range_orderEmbOfFin, Set.Finite.coe_toFinset]
 #align nat.image_nth_Iio_card Nat.image_nth_Iio_card
 
 theorem nth_mem_of_lt_card {n : ℕ} (hf : (setOf p).Finite) (hlt : n < hf.toFinset.card) :
     p (nth p n) :=
-  (image_nth_Iio_card hf).Subset <| Set.mem_image_of_mem _ hlt
+  (image_nth_Iio_card hf).subset <| Set.mem_image_of_mem _ hlt
 #align nat.nth_mem_of_lt_card Nat.nth_mem_of_lt_card
 
 theorem exists_lt_card_finite_nth_eq (hf : (setOf p).Finite) {x} (h : p x) :
     ∃ n, n < hf.toFinset.card ∧ nth p n = x := by
-  rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h 
+  rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h
 #align nat.exists_lt_card_finite_nth_eq Nat.exists_lt_card_finite_nth_eq
 
 /-!
 ### Lemmas about `nat.nth` on an infinite set
 -/
 
-
 /-- When `s` is an infinite set, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
 theorem nth_apply_eq_orderIsoOfNat (hf : (setOf p).Infinite) (n : ℕ) :
     nth p n = @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype n := by rw [nth, dif_neg hf]
@@ -143,21 +142,21 @@ theorem nth_apply_eq_orderIsoOfNat (hf : (setOf p).Infinite) (n : ℕ) :
 
 /-- When `s` is an infinite set, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
 theorem nth_eq_orderIsoOfNat (hf : (setOf p).Infinite) :
-    nth p = coe ∘ @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype :=
+    nth p = (↑) ∘ @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype :=
   funext <| nth_apply_eq_orderIsoOfNat hf
 #align nat.nth_eq_order_iso_of_nat Nat.nth_eq_orderIsoOfNat
 
 theorem nth_strictMono (hf : (setOf p).Infinite) : StrictMono (nth p) := by
-  rw [nth_eq_order_iso_of_nat hf]
+  rw [nth_eq_orderIsoOfNat hf]
   exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
 #align nat.nth_strict_mono Nat.nth_strictMono
 
 theorem nth_injective (hf : (setOf p).Infinite) : Function.Injective (nth p) :=
-  (nth_strictMono hf).Injective
+  (nth_strictMono hf).injective
 #align nat.nth_injective Nat.nth_injective
 
 theorem nth_monotone (hf : (setOf p).Infinite) : Monotone (nth p) :=
-  (nth_strictMono hf).Monotone
+  (nth_strictMono hf).monotone
 #align nat.nth_monotone Nat.nth_monotone
 
 theorem nth_lt_nth (hf : (setOf p).Infinite) {k n} : nth p k < nth p n ↔ k < n :=
@@ -169,9 +168,10 @@ theorem nth_le_nth (hf : (setOf p).Infinite) {k n} : nth p k ≤ nth p n ↔ k 
 #align nat.nth_le_nth Nat.nth_le_nth
 
 theorem range_nth_of_infinite (hf : (setOf p).Infinite) : Set.range (nth p) = setOf p := by
-  rw [nth_eq_order_iso_of_nat hf]
+  rw [nth_eq_orderIsoOfNat hf]
   haveI := hf.to_subtype
-  exact Nat.Subtype.coe_comp_ofNat_range
+  -- porting note: added `classical`; probably, Lean 3 found instance by unification
+  classical exact Nat.Subtype.coe_comp_ofNat_range
 #align nat.range_nth_of_infinite Nat.range_nth_of_infinite
 
 theorem nth_mem_of_infinite (hf : (setOf p).Infinite) (n : ℕ) : p (nth p n) :=
@@ -187,8 +187,8 @@ theorem exists_lt_card_nth_eq {x} (h : p x) :
     ∃ n, (∀ hf : (setOf p).Finite, n < hf.toFinset.card) ∧ nth p n = x := by
   refine' (setOf p).finite_or_infinite.elim (fun hf => _) fun hf => _
   · rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
-    exact ⟨n, fun hf' => hn, hx⟩
-  · rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h 
+    exact ⟨n, fun _ => hn, hx⟩
+  · rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h
     rcases h with ⟨n, hx⟩
     exact ⟨n, fun hf' => absurd hf' hf, hx⟩
 #align nat.exists_lt_card_nth_eq Nat.exists_lt_card_nth_eq
@@ -199,7 +199,7 @@ theorem subset_range_nth : setOf p ⊆ Set.range (nth p) := fun x (hx : p x) =>
 #align nat.subset_range_nth Nat.subset_range_nth
 
 theorem range_nth_subset : Set.range (nth p) ⊆ insert 0 (setOf p) :=
-  (setOf p).finite_or_infinite.elim (fun h => (range_nth_of_finite h).Subset) fun h =>
+  (setOf p).finite_or_infinite.elim (fun h => (range_nth_of_finite h).subset) fun h =>
     (range_nth_of_infinite h).trans_subset (Set.subset_insert _ _)
 #align nat.range_nth_subset Nat.range_nth_subset
 
@@ -228,9 +228,9 @@ theorem le_nth {n : ℕ} (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
 
 theorem isLeast_nth {n} (h : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
     IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
-  ⟨⟨nth_mem n h, fun k hk => nth_lt_nth' hk h⟩, fun x hx =>
+  ⟨⟨nth_mem n h, fun _k hk => nth_lt_nth' hk h⟩, fun _x hx =>
     let ⟨k, hk, hkx⟩ := exists_lt_card_nth_eq hx.1
-    (lt_or_le k n).elim (fun hlt => absurd hkx (hx.2 _ hlt).Ne) fun hle => hkx ▸ nth_le_nth' hle hk⟩
+    (lt_or_le k n).elim (fun hlt => absurd hkx (hx.2 _ hlt).ne) fun hle => hkx ▸ nth_le_nth' hle hk⟩
 #align nat.is_least_nth Nat.isLeast_nth
 
 theorem isLeast_nth_of_lt_card {n : ℕ} (hf : (setOf p).Finite) (hn : n < hf.toFinset.card) :
@@ -248,17 +248,18 @@ that `nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assum
 nonempty because we use the same "garbage value" `0` both for `Inf` on `ℕ` and for `nat.nth s n` for
 `n ≥ card s`. -/
 theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} := by
-  by_cases hn : ∀ hf : (setOf p).Finite, n < hf.to_finset.card
-  · exact (is_least_nth hn).csInf_eq.symm
-  · push_neg at hn 
+  by_cases hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card
+  · exact (isLeast_nth hn).csInf_eq.symm
+  · -- porting note: TODO: was push_neg at hn
+    simp only [not_forall, not_lt] at hn
     rcases hn with ⟨hf, hn⟩
     rw [nth_of_card_le _ hn]
-    refine' ((congr_arg Inf <| Set.eq_empty_of_forall_not_mem fun k hk => _).trans sInf_empty).symm
+    refine' ((congr_arg sInf <| Set.eq_empty_of_forall_not_mem fun k hk => _).trans sInf_empty).symm
     rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
-    exact (hk.2 _ ((hlt hf).trans_le hn)).False
+    exact (hk.2 _ ((hlt hf).trans_le hn)).false
 #align nat.nth_eq_Inf Nat.nth_eq_sInf
 
-theorem nth_zero : nth p 0 = sInf (setOf p) := by rw [nth_eq_Inf]; simp
+theorem nth_zero : nth p 0 = sInf (setOf p) := by rw [nth_eq_sInf]; simp
 #align nat.nth_zero Nat.nth_zero
 
 @[simp]
@@ -286,14 +287,13 @@ theorem nth_eq_zero_mono (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p
 theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a ≤ nth p k := by
   cases' (setOf p).finite_or_infinite with hf hf
   · rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
-    cases' lt_or_le (k + 1) hf.to_finset.card with hk hk
-    ·
-      rwa [(nth_strict_mono_on hf).lt_iff_lt hn hk, lt_succ_iff, ←
-        (nth_strict_mono_on hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h 
-    · rw [nth_of_card_le _ hk] at h 
+    cases' lt_or_le (k + 1) hf.toFinset.card with hk hk
+    · rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, lt_succ_iff,
+        ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
+    · rw [nth_of_card_le _ hk] at h
       exact absurd h (zero_le _).not_lt
   · rcases subset_range_nth ha with ⟨n, rfl⟩
-    rwa [nth_lt_nth hf, lt_succ_iff, ← nth_le_nth hf] at h 
+    rwa [nth_lt_nth hf, lt_succ_iff, ← nth_le_nth hf] at h
 #align nat.le_nth_of_lt_nth_succ Nat.le_nth_of_lt_nth_succ
 
 section Count
@@ -307,7 +307,7 @@ theorem count_nth_zero : count p (nth p 0) = 0 := by
 #align nat.count_nth_zero Nat.count_nth_zero
 
 theorem filter_range_nth_subset_insert (k : ℕ) :
-    (range (nth p (k + 1))).filterₓ p ⊆ insert (nth p k) ((range (nth p k)).filterₓ p) := by
+    (range (nth p (k + 1))).filter p ⊆ insert (nth p k) ((range (nth p k)).filter p) := by
   intro a ha
   simp only [mem_insert, mem_filter, mem_range] at ha ⊢
   exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩
@@ -317,7 +317,7 @@ variable {p}
 
 theorem filter_range_nth_eq_insert {k : ℕ}
     (hlt : ∀ hf : (setOf p).Finite, k + 1 < hf.toFinset.card) :
-    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) := by
+    (range (nth p (k + 1))).filter p = insert (nth p k) ((range (nth p k)).filter p) := by
   refine' (filter_range_nth_subset_insert p k).antisymm fun a ha => _
   simp only [mem_insert, mem_filter, mem_range] at ha ⊢
   have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
@@ -328,12 +328,12 @@ theorem filter_range_nth_eq_insert {k : ℕ}
 
 theorem filter_range_nth_eq_insert_of_finite (hf : (setOf p).Finite) {k : ℕ}
     (hlt : k + 1 < hf.toFinset.card) :
-    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) :=
+    (range (nth p (k + 1))).filter p = insert (nth p k) ((range (nth p k)).filter p) :=
   filter_range_nth_eq_insert fun _ => hlt
 #align nat.filter_range_nth_eq_insert_of_finite Nat.filter_range_nth_eq_insert_of_finite
 
 theorem filter_range_nth_eq_insert_of_infinite (hp : (setOf p).Infinite) (k : ℕ) :
-    (range (nth p (k + 1))).filterₓ p = insert (nth p k) ((range (nth p k)).filterₓ p) :=
+    (range (nth p (k + 1))).filter p = insert (nth p k) ((range (nth p k)).filter p) :=
   filter_range_nth_eq_insert fun hf => absurd hf hp
 #align nat.filter_range_nth_eq_insert_of_infinite Nat.filter_range_nth_eq_insert_of_infinite
 
@@ -378,17 +378,17 @@ theorem le_nth_of_count_le {n k : ℕ} (h : n ≤ nth p k) : count p n ≤ k :=
 variable (p)
 
 theorem nth_count_eq_sInf (n : ℕ) : nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i} := by
-  refine' (nth_eq_Inf _ _).trans (congr_arg Inf _)
+  refine' (nth_eq_sInf _ _).trans (congr_arg sInf _)
   refine' Set.ext fun a => and_congr_right fun hpa => _
   refine' ⟨fun h => not_lt.1 fun ha => _, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
   have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
-  rwa [nth_count hpa, lt_self_iff_false] at hn 
+  rwa [nth_count hpa, lt_self_iff_false] at hn
 #align nat.nth_count_eq_Inf Nat.nth_count_eq_sInf
 
 variable {p}
 
 theorem le_nth_count' {n : ℕ} (hpn : ∃ k, p k ∧ n ≤ k) : n ≤ nth p (count p n) :=
-  (le_csInf hpn fun k => And.right).trans (nth_count_eq_sInf p n).ge
+  (le_csInf hpn fun _ => And.right).trans (nth_count_eq_sInf p n).ge
 #align nat.le_nth_count' Nat.le_nth_count'
 
 theorem le_nth_count (hp : (setOf p).Infinite) (n : ℕ) : n ≤ nth p (count p n) :=

From b0fa77dbbc28b70d956e23e9d29591f3383e879a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 14 Jun 2023 08:28:00 -0500
Subject: [PATCH 5/9] auto: naming

---
 Mathlib/Data/Nat/Nth.lean | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index a209461f5d80d..9a708c1e96702 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -16,23 +16,23 @@ import Mathlib.Order.OrderIsoNat
 # The `n`th Number Satisfying a Predicate
 
 This file defines a function for "what is the `n`th number that satisifies a given predicate `p`",
-and provides lemmas that deal with this function and its connection to `nat.count`.
+and provides lemmas that deal with this function and its connection to `Nat.count`.
 
 ## Main definitions
 
-* `nat.nth p n`: The `n`-th natural `k` (zero-indexed) such that `p k`. If there is no
-  such natural (that is, `p` is true for at most `n` naturals), then `nat.nth p n = 0`.
+* `Nat.nth p n`: The `n`-th natural `k` (zero-indexed) such that `p k`. If there is no
+  such natural (that is, `p` is true for at most `n` naturals), then `Nat.nth p n = 0`.
 
 ## Main results
 
 * `nat.nth_set_card`: For a fintely-often true `p`, gives the cardinality of the set of numbers
   satisfying `p` above particular values of `nth p`
-* `nat.count_nth_gc`: Establishes a Galois connection between `nat.nth p` and `nat.count p`.
-* `nat.nth_eq_order_iso_of_nat`: For an infinitely-ofter true predicate, `nth` agrees with the
+* `nat.count_nth_gc`: Establishes a Galois connection between `Nat.nth p` and `Nat.count p`.
+* `Nat.nth_eq_orderIsoOfNat`: For an infinitely-ofter true predicate, `nth` agrees with the
   order-isomorphism of the subtype to the natural numbers.
 
 There has been some discussion on the subject of whether both of `nth` and
-`nat.subtype.order_iso_of_nat` should exist. See discussion
+`Nat.Subtype.orderIsoOfNat` should exist. See discussion
 [here](https://github.com/leanprover-community/mathlib/pull/9457#pullrequestreview-767221180).
 Future work should address how lemmas that use these should be written.
 
@@ -57,7 +57,7 @@ noncomputable def nth (p : ℕ → Prop) (n : ℕ) : ℕ := by
 variable {p}
 
 /-!
-### Lemmas about `nat.nth` on a finite set
+### Lemmas about `Nat.nth` on a finite set
 -/
 
 
@@ -132,15 +132,15 @@ theorem exists_lt_card_finite_nth_eq (hf : (setOf p).Finite) {x} (h : p x) :
 #align nat.exists_lt_card_finite_nth_eq Nat.exists_lt_card_finite_nth_eq
 
 /-!
-### Lemmas about `nat.nth` on an infinite set
+### Lemmas about `Nat.nth` on an infinite set
 -/
 
-/-- When `s` is an infinite set, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
+/-- When `s` is an infinite set, `nth` agrees with `Nat.Subtype.orderIsoOfNat`. -/
 theorem nth_apply_eq_orderIsoOfNat (hf : (setOf p).Infinite) (n : ℕ) :
     nth p n = @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype n := by rw [nth, dif_neg hf]
 #align nat.nth_apply_eq_order_iso_of_nat Nat.nth_apply_eq_orderIsoOfNat
 
-/-- When `s` is an infinite set, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
+/-- When `s` is an infinite set, `nth` agrees with `Nat.Subtype.orderIsoOfNat`. -/
 theorem nth_eq_orderIsoOfNat (hf : (setOf p).Infinite) :
     nth p = (↑) ∘ @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype :=
   funext <| nth_apply_eq_orderIsoOfNat hf
@@ -243,9 +243,9 @@ theorem isLeast_nth_of_infinite (hf : (setOf p).Infinite) (n : ℕ) :
   isLeast_nth fun h => absurd h hf
 #align nat.is_least_nth_of_infinite Nat.isLeast_nth_of_infinite
 
-/-- An alternative recursive definition of `nat.nth`: `nat.nth s n` is the infimum of `x ∈ s` such
-that `nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
-nonempty because we use the same "garbage value" `0` both for `Inf` on `ℕ` and for `nat.nth s n` for
+/-- An alternative recursive definition of `Nat.nth`: `Nat.nth s n` is the infimum of `x ∈ s` such
+that `Nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
+nonempty because we use the same "garbage value" `0` both for `Inf` on `ℕ` and for `Nat.nth s n` for
 `n ≥ card s`. -/
 theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} := by
   by_cases hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card
@@ -396,8 +396,8 @@ theorem le_nth_count (hp : (setOf p).Infinite) (n : ℕ) : n ≤ nth p (count p
   le_nth_count' ⟨m, hp, hn.le⟩
 #align nat.le_nth_count Nat.le_nth_count
 
-/-- If a predicate `p : ℕ → Prop` is true for infinitely many numbers, then `nat.count p` and
-`nat.nth p` form a Galois insertion. -/
+/-- If a predicate `p : ℕ → Prop` is true for infinitely many numbers, then `Nat.count p` and
+`Nat.nth p` form a Galois insertion. -/
 noncomputable def giCountNth (hp : (setOf p).Infinite) : GaloisInsertion (count p) (nth p) :=
   GaloisInsertion.monotoneIntro (nth_monotone hp) (count_monotone p) (le_nth_count hp)
     (count_nth_of_infinite hp)

From bc6e2900bafc0ab42ce45623e34cb6c2c2c23d8e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 15 Jun 2023 14:15:07 -0500
Subject: [PATCH 6/9] Fix 1 name

---
 Mathlib/Data/Nat/Nth.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index 9a708c1e96702..5747a42976a80 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -27,7 +27,7 @@ and provides lemmas that deal with this function and its connection to `Nat.coun
 
 * `nat.nth_set_card`: For a fintely-often true `p`, gives the cardinality of the set of numbers
   satisfying `p` above particular values of `nth p`
-* `nat.count_nth_gc`: Establishes a Galois connection between `Nat.nth p` and `Nat.count p`.
+* `Nat.gc_count_nth`: Establishes a Galois connection between `Nat.nth p` and `Nat.count p`.
 * `Nat.nth_eq_orderIsoOfNat`: For an infinitely-ofter true predicate, `nth` agrees with the
   order-isomorphism of the subtype to the natural numbers.
 
@@ -182,7 +182,6 @@ theorem nth_mem_of_infinite (hf : (setOf p).Infinite) (n : ℕ) : p (nth p n) :=
 ### Lemmas that work for finite and infinite sets
 -/
 
-
 theorem exists_lt_card_nth_eq {x} (h : p x) :
     ∃ n, (∀ hf : (setOf p).Finite, n < hf.toFinset.card) ∧ nth p n = x := by
   refine' (setOf p).finite_or_infinite.elim (fun hf => _) fun hf => _

From 7dd1530038bd76ae6e3dd2b46f4b7ff9e71042c0 Mon Sep 17 00:00:00 2001
From: Komyyy <pol_tta@outlook.jp>
Date: Mon, 19 Jun 2023 19:12:36 +0900
Subject: [PATCH 7/9] doc

---
 Mathlib/Data/Nat/Nth.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index 5747a42976a80..1394e7e9e0335 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -25,8 +25,8 @@ and provides lemmas that deal with this function and its connection to `Nat.coun
 
 ## Main results
 
-* `nat.nth_set_card`: For a fintely-often true `p`, gives the cardinality of the set of numbers
-  satisfying `p` above particular values of `nth p`
+* `Nat.nth_eq_orderEmbOfFin`: For a fintely-often true `p`, gives the cardinality of the set of
+  numbers satisfying `p` above particular values of `nth p`
 * `Nat.gc_count_nth`: Establishes a Galois connection between `Nat.nth p` and `Nat.count p`.
 * `Nat.nth_eq_orderIsoOfNat`: For an infinitely-ofter true predicate, `nth` agrees with the
   order-isomorphism of the subtype to the natural numbers.
@@ -47,7 +47,7 @@ variable (p : ℕ → Prop)
 
 /-- Find the `n`-th natural number satisfying `p` (indexed from `0`, so `nth p 0` is the first
 natural number satisfying `p`), or `0` if there is no such number. See also
-`subtype.order_iso_of_nat` for the order isomorphism with ℕ when `p` is infinitely often true. -/
+`Subtype.orderIsoOfNat` for the order isomorphism with ℕ when `p` is infinitely often true. -/
 noncomputable def nth (p : ℕ → Prop) (n : ℕ) : ℕ := by
   classical exact
     if h : Set.Finite (setOf p) then (h.toFinset.sort (· ≤ ·)).getD n 0
@@ -244,8 +244,8 @@ theorem isLeast_nth_of_infinite (hf : (setOf p).Infinite) (n : ℕ) :
 
 /-- An alternative recursive definition of `Nat.nth`: `Nat.nth s n` is the infimum of `x ∈ s` such
 that `Nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
-nonempty because we use the same "garbage value" `0` both for `Inf` on `ℕ` and for `Nat.nth s n` for
-`n ≥ card s`. -/
+nonempty because we use the same "garbage value" `0` both for `sInf` on `ℕ` and for `Nat.nth s n`
+for `n ≥ card s`. -/
 theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} := by
   by_cases hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card
   · exact (isLeast_nth hn).csInf_eq.symm
@@ -417,4 +417,3 @@ theorem lt_nth_iff_count_lt (hp : (setOf p).Infinite) {a b : ℕ} : a < count p
 end Count
 
 end Nat
-

From bfa097ef8c91e9775b019df02939786810e5273b Mon Sep 17 00:00:00 2001
From: Komyyy <pol_tta@outlook.jp>
Date: Mon, 19 Jun 2023 19:51:25 +0900
Subject: [PATCH 8/9] fix

---
 Mathlib/Tactic/PushNeg.lean | 2 +-
 test/push_neg.lean          | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/PushNeg.lean b/Mathlib/Tactic/PushNeg.lean
index 1bdac021a7ec7..3bb9fe7d2b21f 100644
--- a/Mathlib/Tactic/PushNeg.lean
+++ b/Mathlib/Tactic/PushNeg.lean
@@ -84,7 +84,7 @@ def transformNegationStep (e : Expr) : SimpM (Option Simp.Step) := do
       return none
   | _ => match ex with
           | .forallE name ty body binfo => do
-              if (← isProp ty) then
+              if (← isProp ty) && !body.hasLooseBVars then
                 return mkSimpStep (← mkAppM ``And #[ty, mkNot body])
                   (← mkAppM ``not_implies_eq #[ty, body])
               else
diff --git a/test/push_neg.lean b/test/push_neg.lean
index 8b90905bac03c..38d353ad76543 100644
--- a/test/push_neg.lean
+++ b/test/push_neg.lean
@@ -141,3 +141,7 @@ example (h : x = 0 ∧ y ≠ 0) : ¬(x = 0 → y = 0) := by
   exact h
 
 end use_distrib
+
+example (a : α) (o : Option α) (h : ¬∀ hs, o.get hs ≠ a) : ∃ hs, o.get hs = a := by
+  push_neg at h
+  exact h

From 3433ddf2d78523f9cb109d1e581e0950cf5d9ff6 Mon Sep 17 00:00:00 2001
From: Komyyy <pol_tta@outlook.jp>
Date: Mon, 19 Jun 2023 20:00:26 +0900
Subject: [PATCH 9/9] push_neg

---
 Mathlib/Data/Nat/Nth.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
index 1394e7e9e0335..d99d577676e69 100644
--- a/Mathlib/Data/Nat/Nth.lean
+++ b/Mathlib/Data/Nat/Nth.lean
@@ -249,8 +249,7 @@ for `n ≥ card s`. -/
 theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} := by
   by_cases hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card
   · exact (isLeast_nth hn).csInf_eq.symm
-  · -- porting note: TODO: was push_neg at hn
-    simp only [not_forall, not_lt] at hn
+  · push_neg at hn
     rcases hn with ⟨hf, hn⟩
     rw [nth_of_card_le _ hn]
     refine' ((congr_arg sInf <| Set.eq_empty_of_forall_not_mem fun k hk => _).trans sInf_empty).symm