fix: patch for std4#195 (more succ/pred lemmas for Nat) (#6203)

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -203,7 +203,7 @@ theorem sum_range_id_mul_two (n : ℕ) : (∑ i in range n, i) * 2 = n * (n - 1)
     by rw [sum_range_reflect (fun i => i) n, mul_two]
     _ = ∑ i in range n, (i + (n - 1 - i)) := sum_add_distrib.symm
     _ = ∑ i in range n, (n - 1) :=
-      sum_congr rfl fun i hi => add_tsub_cancel_of_le <| Nat.le_pred_of_lt <| mem_range.1 hi
+      sum_congr rfl fun i hi => add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| mem_range.1 hi
     _ = n * (n - 1) := by rw [sum_const, card_range, Nat.nsmul_eq_mul]
 #align finset.sum_range_id_mul_two Finset.sum_range_id_mul_two
 
@@ -275,7 +275,7 @@ theorem sum_Ico_by_parts (hmn : m < n) :
   have h₂ :
     (∑ i in Ico (m + 1) n, f i • G (i + 1)) =
       (∑ i in Ico m (n - 1), f i • G (i + 1)) + f (n - 1) • G n - f m • G (m + 1) := by
-    rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_pred_of_lt hmn),
+    rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_sub_one_of_lt hmn),
       Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
   rw [sum_eq_sum_Ico_succ_bot hmn]
   -- porting note: the following used to be done with `conv`

Mathlib/Algebra/CharP/Basic.lean

@@ -511,8 +511,6 @@ end CommRing
 
 section Semiring
 
-open Nat
-
 variable [NonAssocSemiring R]
 
 theorem char_ne_one [Nontrivial R] (p : ℕ) [hc : CharP R p] : p ≠ 1 := fun hp : p = 1 =>
@@ -529,7 +527,7 @@ theorem char_is_prime_of_two_le (p : ℕ) [hc : CharP R p] (hp : 2 ≤ p) : Nat.
   fun (d : ℕ) (hdvd : ∃ e, p = d * e) =>
   let ⟨e, hmul⟩ := hdvd
   have : (p : R) = 0 := (cast_eq_zero_iff R p p).mpr (dvd_refl p)
-  have : (d : R) * e = 0 := @cast_mul R _ d e ▸ hmul ▸ this
+  have : (d : R) * e = 0 := @Nat.cast_mul R _ d e ▸ hmul ▸ this
   Or.elim (eq_zero_or_eq_zero_of_mul_eq_zero this)
     (fun hd : (d : R) = 0 =>
       have : p ∣ d := (cast_eq_zero_iff R p d).mp hd

Mathlib/Algebra/GeomSum.lean

@@ -147,7 +147,7 @@ theorem geom_sum₂_self {α : Type*} [CommRing α] (x : α) (n : ℕ) :
       by simp_rw [← pow_add]
     _ = ∑ i in Finset.range n, x ^ (n - 1) :=
       Finset.sum_congr rfl fun i hi =>
-        congr_arg _ <| add_tsub_cancel_of_le <| Nat.le_pred_of_lt <| Finset.mem_range.1 hi
+        congr_arg _ <| add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| Finset.mem_range.1 hi
     _ = (Finset.range n).card • x ^ (n - 1) := Finset.sum_const _
     _ = n * x ^ (n - 1) := by rw [Finset.card_range, nsmul_eq_mul]
 #align geom_sum₂_self geom_sum₂_self
@@ -309,7 +309,7 @@ protected theorem Commute.geom_sum₂_succ_eq {α : Type u} [Ring α] {x y : α}
   suffices n - 1 - i + 1 = n - i by rw [this]
   cases' n with n
   · exact absurd (List.mem_range.mp hi) i.not_lt_zero
-  · rw [tsub_add_eq_add_tsub (Nat.le_pred_of_lt (List.mem_range.mp hi)),
+  · rw [tsub_add_eq_add_tsub (Nat.le_sub_one_of_lt (List.mem_range.mp hi)),
       tsub_add_cancel_of_le (Nat.succ_le_iff.mpr n.succ_pos)]
 #align commute.geom_sum₂_succ_eq Commute.geom_sum₂_succ_eq
 

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -112,7 +112,7 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     · rintro rfl
       simp only [Fin.val_zero, not_lt_zero'] at hij'
     · simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter,
-        Fin.coe_castSucc, Fin.coe_pred, true_and] using Nat.le_pred_of_lt hij'
+        Fin.coe_castSucc, Fin.coe_pred, true_and] using Nat.le_sub_one_of_lt hij'
     · simp only [Fin.castLT_castSucc, Fin.succ_pred]
 #align algebraic_topology.alternating_face_map_complex.d_squared AlgebraicTopology.AlternatingFaceMapComplex.d_squared
 

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -696,7 +696,7 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
       conv_rhs => dsimp
       erw [Fin.succ_pred]
       simpa only [Fin.le_iff_val_le_val, Fin.coe_castSucc, Fin.coe_pred] using
-        Nat.le_pred_of_lt (Fin.lt_iff_val_lt_val.mp h')
+        Nat.le_sub_one_of_lt (Fin.lt_iff_val_lt_val.mp h')
   · obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)
     use θ ≫ σ (Fin.last _)
     ext x : 4

Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

@@ -333,7 +333,7 @@ theorem D_subset_differentiable_set {K : Set (E →L[𝕜] F)} (hK : IsComplete
       rw [pow_lt_pow_iff_of_lt_one (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num)] at this
       linarith
     set m := k - 1
-    have m_ge : n e ≤ m := Nat.le_pred_of_lt k_gt
+    have m_ge : n e ≤ m := Nat.le_sub_one_of_lt k_gt
     have km : k = m + 1 := (Nat.succ_pred_eq_of_pos (lt_of_le_of_lt (zero_le _) k_gt)).symm
     rw [km] at hk h'k
     -- `f` is well approximated by `L e (n e) k` at the relevant scale
@@ -701,7 +701,7 @@ theorem D_subset_differentiable_set {K : Set F} (hK : IsComplete K) :
       rw [pow_lt_pow_iff_of_lt_one (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num)] at this
       linarith
     set m := k - 1
-    have m_ge : n e ≤ m := Nat.le_pred_of_lt k_gt
+    have m_ge : n e ≤ m := Nat.le_sub_one_of_lt k_gt
     have km : k = m + 1 := (Nat.succ_pred_eq_of_pos (lt_of_le_of_lt (zero_le _) k_gt)).symm
     rw [km] at hk h'k
     -- `f` is well approximated by `L e (n e) k` at the relevant scale

Mathlib/Combinatorics/Additive/Behrend.lean

@@ -164,7 +164,7 @@ theorem map_injOn : {x : Fin n → ℕ | ∀ i, x i < d}.InjOn (map d) := by
 
 theorem map_le_of_mem_box (hx : x ∈ box n d) :
     map (2 * d - 1) x ≤ ∑ i : Fin n, (d - 1) * (2 * d - 1) ^ (i : ℕ) :=
-  map_monotone (2 * d - 1) fun _ => Nat.le_pred_of_lt <| mem_box.1 hx _
+  map_monotone (2 * d - 1) fun _ => Nat.le_sub_one_of_lt <| mem_box.1 hx _
 #align behrend.map_le_of_mem_box Behrend.map_le_of_mem_box
 
 nonrec theorem addSalemSpencer_sphere : AddSalemSpencer (sphere n d k : Set (Fin n → ℕ)) := by
@@ -196,7 +196,7 @@ theorem addSalemSpencer_image_sphere :
 theorem sum_sq_le_of_mem_box (hx : x ∈ box n d) : ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2 := by
   rw [mem_box] at hx
   have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i =>
-    Nat.pow_le_pow_of_le_left (Nat.le_pred_of_lt (hx i)) _
+    Nat.pow_le_pow_of_le_left (Nat.le_sub_one_of_lt (hx i)) _
   exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [card_fin, smul_eq_mul])
 #align behrend.sum_sq_le_of_mem_box Behrend.sum_sq_le_of_mem_box
 

Mathlib/Combinatorics/Hall/Finite.lean

@@ -62,7 +62,7 @@ theorem hall_cond_of_erase {x : ι} (a : α)
     rw [← erase_biUnion]
     by_cases hb : a ∈ s'.biUnion fun x => t x
     · rw [card_erase_of_mem hb]
-      exact Nat.le_pred_of_lt ha'
+      exact Nat.le_sub_one_of_lt ha'
     · rw [erase_eq_of_not_mem hb]
       exact Nat.le_of_lt ha'
   · rw [nonempty_iff_ne_empty, not_not] at he

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -148,7 +148,7 @@ theorem a_add_one_le_four_pow_parts_card : a + 1 ≤ 4 ^ P.parts.card := by
   rw [stepBound, ← Nat.div_div_eq_div_mul]
   conv_rhs => rw [← Nat.sub_add_cancel h]
   rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]
-  exact Nat.le_pred_of_lt (Nat.lt_div_mul_add h)
+  exact Nat.le_sub_one_of_lt (Nat.lt_div_mul_add h)
 #align szemeredi_regularity.a_add_one_le_four_pow_parts_card SzemerediRegularity.a_add_one_le_four_pow_parts_card
 
 theorem card_aux₁ (hucard : u.card = m * 4 ^ P.parts.card + a) :

Mathlib/Data/Fin/Basic.lean

@@ -1427,7 +1427,7 @@ theorem succAbove_castLT {x y : Fin (n + 1)} (h : x < y)
 theorem succAbove_pred {x y : Fin (n + 1)} (h : x < y)
     (hy : y ≠ 0 := (x.zero_le.trans_lt h).ne') : x.succAbove (y.pred hy) = y := by
   rw [succAbove_above, succ_pred]
-  simpa [le_iff_val_le_val] using Nat.le_pred_of_lt h
+  simpa [le_iff_val_le_val] using Nat.le_sub_one_of_lt h
 #align fin.succ_above_pred Fin.succAbove_pred
 
 theorem castLT_succAbove {x : Fin n} {y : Fin (n + 1)} (h : castSucc x < y)
@@ -1667,7 +1667,7 @@ theorem succAbove_predAbove {p : Fin n} {i : Fin (n + 1)} (h : i ≠ castSucc p)
     rw [if_neg]
     · simp
     · simp only [pred, Fin.mk_lt_mk, not_lt]
-      exact Nat.le_pred_of_lt (h.symm.lt_of_le H)
+      exact Nat.le_sub_one_of_lt (h.symm.lt_of_le H)
     · exact lt_of_le_of_ne H h.symm
 #align fin.succ_above_pred_above Fin.succAbove_predAbove
 

Mathlib/Data/Finset/Powerset.lean

@@ -312,7 +312,7 @@ theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.
     · intro x hx
       simp only [mem_biUnion, exists_prop, id.def]
       obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty
-        (le_trans (Nat.le_pred_of_lt hn) pred_card_le_card_erase)
+        (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)
       · refine' ⟨insert x t, _, mem_insert_self _ _⟩
         rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
         exact mem_union_right _ (mem_image_of_mem _ ht)

Mathlib/Data/Finset/Sort.lean

@@ -125,7 +125,7 @@ theorem sorted_last_eq_max'_aux (s : Finset α)
   · have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H)
     obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
     rw [← hi]
-    exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.le_pred_of_lt i.prop)
+    exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.le_sub_one_of_lt i.prop)
 #align finset.sorted_last_eq_max'_aux Finset.sorted_last_eq_max'_aux
 
 theorem sorted_last_eq_max' {s : Finset α}

Mathlib/Data/List/Cycle.lean

@@ -410,7 +410,7 @@ theorem prev_reverse_eq_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l)
       length_reverse, Nat.mod_eq_of_lt (tsub_lt_self lpos Nat.succ_pos'),
       tsub_tsub_cancel_of_le (Nat.succ_le_of_lt lpos)]
     rw [← nthLe_reverse]
-    · simp [tsub_tsub_cancel_of_le (Nat.le_pred_of_lt hk)]
+    · simp [tsub_tsub_cancel_of_le (Nat.le_sub_one_of_lt hk)]
     · simpa using (Nat.sub_le _ _).trans_lt (tsub_lt_self lpos Nat.succ_pos')
     · simpa
 #align list.prev_reverse_eq_next List.prev_reverse_eq_next

Mathlib/Data/Nat/Basic.lean

@@ -165,7 +165,6 @@ theorem eq_of_le_of_lt_succ {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n + 1) : m
 -- Moved to Std
 #align nat.one_add Nat.one_add
 
-@[simp]
 theorem succ_pos' {n : ℕ} : 0 < succ n :=
   succ_pos n
 #align nat.succ_pos' Nat.succ_pos'

Mathlib/Data/Nat/Digits.lean

@@ -555,7 +555,7 @@ theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits
         have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
         have ih := ih (w₂' h') w₁'
         simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
-          succ_eq_one_add] at ih
+          ←Nat.one_add] at ih
         have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
         rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
         have h₁ : 1 ≤ tl.length :=  List.length_pos.mpr h'

Mathlib/Data/Nat/Totient.lean

@@ -245,7 +245,7 @@ theorem card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [Fintype (ZMod p)ˣ] :
     Fintype.card (ZMod p)ˣ ≤ p - 1 := by
   haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩
   rw [ZMod.card_units_eq_totient p]
-  exact Nat.le_pred_of_lt (Nat.totient_lt p hp)
+  exact Nat.le_sub_one_of_lt (Nat.totient_lt p hp)
 #align nat.card_units_zmod_lt_sub_one Nat.card_units_zmod_lt_sub_one
 
 theorem prime_iff_card_units (p : ℕ) [Fintype (ZMod p)ˣ] :

Mathlib/Data/Polynomial/Derivative.lean

@@ -216,7 +216,7 @@ theorem natDegree_derivative_lt {p : R[X]} (hp : p.natDegree ≠ 0) :
 theorem natDegree_derivative_le (p : R[X]) : p.derivative.natDegree ≤ p.natDegree - 1 := by
   by_cases p0 : p.natDegree = 0
   · simp [p0, derivative_of_natDegree_zero]
-  · exact Nat.le_pred_of_lt (natDegree_derivative_lt p0)
+  · exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)
 #align polynomial.nat_degree_derivative_le Polynomial.natDegree_derivative_le
 
 theorem natDegree_iterate_derivative (p : R[X]) (k : ℕ) :

Mathlib/Data/Polynomial/EraseLead.lean

@@ -204,7 +204,7 @@ theorem eraseLead_natDegree_lt_or_eraseLead_eq_zero (f : R[X]) :
 
 theorem eraseLead_natDegree_le (f : R[X]) : (eraseLead f).natDegree ≤ f.natDegree - 1 := by
   rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
-  · exact Nat.le_pred_of_lt h
+  · exact Nat.le_sub_one_of_lt h
   · simp only [h, natDegree_zero, zero_le]
 #align polynomial.erase_lead_nat_degree_le Polynomial.eraseLead_natDegree_le
 

Mathlib/Data/Polynomial/Module.lean

@@ -230,7 +230,7 @@ theorem monomial_smul_single (i : ℕ) (r : R) (j : ℕ) (m : M) :
   | succ n hn =>
     rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
     congr 2
-    rw [← Nat.succ_eq_one_add]
+    rw [Nat.one_add]
     exact Finsupp.mapDomain_single
 #align polynomial_module.monomial_smul_single PolynomialModule.monomial_smul_single
 

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -784,7 +784,7 @@ lemma to_digits_core_length (b : Nat) (h : 2 <= b) (f n e : Nat)
             to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
           exact Nat.succ_le_succ ih
       case neg =>
-        have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
+        have _ : e = 0 := Nat.eq_zero_of_not_pos h_pred_pos
         rw [‹e = 0›]
         have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
         have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)

Mathlib/Init/Meta/WellFoundedTactics.lean

@@ -16,11 +16,7 @@ theorem Nat.lt_add_of_zero_lt_left (a b : Nat) (h : 0 < b) : a < a + b :=
     assumption
 #align nat.lt_add_of_zero_lt_left Nat.lt_add_of_zero_lt_left
 
-theorem Nat.zero_lt_one_add (a : Nat) : 0 < 1 + a :=
-  suffices 0 < a + 1 by
-    simp only [Nat.add_comm]
-    assumption
-  Nat.zero_lt_succ _
+theorem Nat.zero_lt_one_add (a : Nat) : 0 < 1 + a := by simp [Nat.one_add]
 #align nat.zero_lt_one_add Nat.zero_lt_one_add
 
 #align nat.lt_add_right Nat.lt_add_right

Mathlib/NumberTheory/Multiplicity.lean

@@ -114,7 +114,7 @@ theorem odd_sq_dvd_geom_sum₂_sub (hp : Odd p) :
       have : ∀ (x : ℕ), (hx : x ∈ range p) → a ^ (x + (p - 1 - x)) = a ^ (p - 1) := by
         intro x hx
         rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]
-        exact Nat.le_pred_of_lt (Finset.mem_range.mp hx)
+        exact Nat.le_sub_one_of_lt (Finset.mem_range.mp hx)
       rw [Finset.sum_congr rfl this]
     _ =
         mk (span {s})
@@ -129,7 +129,7 @@ theorem odd_sq_dvd_geom_sum₂_sub (hp : Odd p) :
       rintro (⟨⟩ | ⟨x⟩) hx
       · rw [Nat.cast_zero, mul_zero, mul_zero]
       · have : x.succ - 1 + (p - 1 - x.succ) = p - 2 := by
-          rw [← Nat.add_sub_assoc (Nat.le_pred_of_lt (Finset.mem_range.mp hx))]
+          rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]
           exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
         rw [this]
         ring1

Mathlib/Probability/Martingale/Upcrossing.lean

@@ -321,7 +321,7 @@ theorem upperCrossingTime_bound_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω)
       refine' strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab _
       rw [Nat.lt_pred_iff] at hm
       convert Nat.find_min _ hm
-    convert StrictMonoOn.Iic_id_le hmono N (Nat.le_pred_of_lt hN')
+    convert StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')
   · rw [not_lt] at hN'
     exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))
 #align measure_theory.upper_crossing_time_bound_eq MeasureTheory.upperCrossingTime_bound_eq

Mathlib/Probability/StrongLaw.lean

@@ -465,7 +465,7 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
         · rintro ⟨i, j⟩ hij
           simp only [mem_sigma, mem_range] at hij
           simp only [hij.1, hij.2, mem_sigma, mem_range, mem_filter, and_true_iff]
-          exact hij.2.trans_le (u_mono (Nat.le_pred_of_lt hij.1))
+          exact hij.2.trans_le (u_mono (Nat.le_sub_one_of_lt hij.1))
         · rintro ⟨i, j⟩ hij
           simp only [mem_sigma, mem_range, mem_filter] at hij
           simp only [hij.2.1, hij.2.2, mem_sigma, mem_range, and_self_iff]

Mathlib/RingTheory/IntegralClosure.lean

@@ -728,7 +728,7 @@ theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ nat
   · simp [h₁]
   · rw [h₂, leadingCoeff, ← pow_succ, tsub_add_cancel_of_le hp]
   · rw [mul_assoc, ← pow_add, tsub_add_cancel_of_le]
-    apply Nat.le_pred_of_lt
+    apply Nat.le_sub_one_of_lt
     rw [lt_iff_le_and_ne]
     exact ⟨le_natDegree_of_ne_zero h₁, h₂⟩
 #align normalize_scale_roots_coeff_mul_leading_coeff_pow normalizeScaleRoots_coeff_mul_leadingCoeff_pow

Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean

@@ -280,7 +280,7 @@ theorem psum_eq_mul_esymm_sub_sum (k : ℕ) (h : 0 < k) : psum σ R k =
     rw [mem_filter, mem_antidiagonal, mem_singleton]
     refine' ⟨_, fun ha ↦ by aesop⟩
     rintro ⟨ha, ⟨_, ha0⟩⟩
-    rw [← ha, Nat.eq_zero_of_nonpos a.fst ha0, zero_add, ← Nat.eq_zero_of_nonpos a.fst ha0]
+    rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
   rw [this, sum_singleton] at sub_both_sides
   simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides
   exact sub_both_sides.symm

Mathlib/RingTheory/Polynomial/Bernstein.lean

@@ -189,7 +189,7 @@ theorem iterate_derivative_at_0 (n ν : ℕ) :
         rw [this, ascPochhammer_eval_succ]
         rw_mod_cast [tsub_add_cancel_of_le (h'.trans n.pred_le)]
   · simp only [not_le] at h
-    rw [tsub_eq_zero_iff_le.mpr (Nat.le_pred_of_lt h), eq_zero_of_lt R h]
+    rw [tsub_eq_zero_iff_le.mpr (Nat.le_sub_one_of_lt h), eq_zero_of_lt R h]
     simp [pos_iff_ne_zero.mp (pos_of_gt h)]
 #align bernstein_polynomial.iterate_derivative_at_0 bernsteinPolynomial.iterate_derivative_at_0
 

Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

@@ -133,7 +133,8 @@ theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S}
           tsub_add_cancel_of_le one_le_deg]
         exact degree_eq_natDegree hp
       · have : i.1 ≤ p.natDegree - 1 :=
-          Nat.le_pred_of_lt (lt_of_le_of_ne (le_natDegree_of_ne_zero (mem_support_iff.mp i.2)) hi)
+          Nat.le_sub_one_of_lt
+            (lt_of_le_of_ne (le_natDegree_of_ne_zero (mem_support_iff.mp i.2)) hi)
         rw [integralNormalization_coeff_ne_natDegree hi, mul_assoc, ← pow_add,
           tsub_add_cancel_of_le this]
     _ = f p.leadingCoeff ^ (natDegree p - 1) * eval₂ f z p := by

Mathlib/Testing/SlimCheck/Gen.lean

@@ -55,7 +55,7 @@ def choose (α : Type u) [Preorder α] [BoundedRandom α] (lo hi : α) (h : lo 
 
 lemma chooseNatLt_aux {lo hi : Nat} (a : Nat) (h : Nat.succ lo ≤ a ∧ a ≤ hi) :
     lo ≤ Nat.pred a ∧ Nat.pred a < hi :=
-  And.intro (Nat.le_pred_of_lt (Nat.lt_of_succ_le h.left)) <|
+  And.intro (Nat.le_sub_one_of_lt (Nat.lt_of_succ_le h.left)) <|
     show a.pred.succ ≤ hi by
        rw [Nat.succ_pred_eq_of_pos]
        exact h.right

Mathlib/Util/DischargerAsTactic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 Alex J. Best. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Simp.Main
 import Std.Tactic.Exact
 
 /-!

lake-manifest.json

@@ -2,14 +2,6 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
     "rev": "396201245bf244f9d78e9007a02dd1c388193d27",
@@ -40,5 +32,13 @@
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "8bedddc3883cf58c1ae443a48bfa430e932a80b0",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
     "inherited": false}}],
  "name": "mathlib"}

test/lift.lean

@@ -206,7 +206,7 @@ example (n : ℕ) : n = 0 ∨ ∃ p : ℕ+, n = p := by
     right
     exact ⟨n, rfl⟩
   · left
-    exact Nat.eq_zero_of_nonpos _ hn
+    exact Nat.eq_zero_of_not_pos hn
 
 example (n : ℤ) (hn : 0 < n) : True := by
   lift n to ℕ+