English
If p and q agree up to a point x, then Nat.find hp equals Nat.find hq.
Русский
Если предикаты p и q совпадают до некоторого x, то Nat.find(h_p) = Nat.find(h_q).
LaTeX
$$$\\mathrm{Nat.find}(hp) = \\mathrm{Nat.find}(hq).$$$
Lean4
/-- If a predicate `p` holds at some `x` and agrees with `q` up to that `x`, then
their `Nat.find` agree. The stronger version of `Nat.find_congr'`, since this one needs
agreement only up to `Nat.find _` while the other requires `p = q`.
Usage of this lemma will likely be via `obtain ⟨x, hx⟩ := hp; apply Nat.find_congr hx` to unify `q`,
or provide it explicitly with `rw [Nat.find_congr (q := q) hx]`.
-/
theorem find_congr [DecidablePred q] {x : ℕ} (hx : p x) (hpq : ∀ n ≤ x, p n ↔ q n) :
Nat.find ⟨x, hx⟩ = Nat.find ⟨x, show q x from hpq _ le_rfl |>.1 hx⟩ :=
le_antisymm (find_mono_of_le (hpq _ le_rfl |>.1 hx) fun _ h ↦ (hpq _ h).mpr)
(find_mono_of_le hx fun _ h ↦ (hpq _ h).mp)
