fix: patch for std4#197 (More add lemmas for Nat) (#6202)

leanprover-community · Dec 19, 2023 · e3d665e · e3d665e
1 parent 1ec5ce1
commit e3d665e
Show file tree

Hide file tree

Showing 19 changed files with 24 additions and 26 deletions.
diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean
@@ -490,7 +490,7 @@ theorem ceil_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n
     · obtain ⟨d, rfl⟩ := exists_add_of_le hb
       rw [Nat.cast_add, add_comm n, add_comm (n : α), add_lt_add_iff_right, add_lt_add_iff_right,
         lt_ceil]
-    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (lt_add_left _ _ _ hb)
+    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)
 #align nat.ceil_add_nat Nat.ceil_add_nat
 
 theorem ceil_add_one (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1 := by

diff --git a/Mathlib/Control/Fix.lean b/Mathlib/Control/Fix.lean
@@ -101,10 +101,10 @@ protected theorem fix_def {x : α} (h' : ∃ i, (Fix.approx f i x).Dom) :
     ext : 1
     have hh : ¬(Fix.approx f z.val x).Dom := by
       apply Nat.find_min h'
-      rw [hk, Nat.succ_add, ← Nat.add_succ]
+      rw [hk, Nat.succ_add_eq_add_succ]
       apply Nat.lt_of_succ_le
       apply Nat.le_add_left
-    rw [succ_add_eq_succ_add] at _this hk
+    rw [succ_add_eq_add_succ] at _this hk
     rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
 #align part.fix_def Part.fix_def
 

diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -653,12 +653,12 @@ theorem snoc_eq_append {α : Type*} (xs : Fin n → α) (x : α) :
 
 theorem append_left_snoc {n m} {α : Type*} (xs : Fin n → α) (x : α) (ys : Fin m → α) :
     Fin.append (Fin.snoc xs x) ys =
-      Fin.append xs (Fin.cons x ys) ∘ Fin.cast (Nat.succ_add_eq_succ_add ..) := by
+      Fin.append xs (Fin.cons x ys) ∘ Fin.cast (Nat.succ_add_eq_add_succ ..) := by
   rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]; rfl
 
 theorem append_right_cons {n m} {α : Type*} (xs : Fin n → α) (y : α) (ys : Fin m → α) :
     Fin.append xs (Fin.cons y ys) =
-      Fin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_succ_add ..).symm := by
+      Fin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_add_succ ..).symm := by
   rw [append_left_snoc]; rfl
 
 theorem comp_init {α : Type*} {β : Type*} (g : α → β) (q : Fin n.succ → α) :

diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean
@@ -154,7 +154,7 @@ theorem Sorted.rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) {
   obtain ⟨⟨ix, hix⟩, rfl⟩ := get_of_mem hx
   rw [get_take', get_drop']
   rw [length_take] at hix
-  exact h.rel_nthLe_of_lt _ _ (ix.lt_add_right _ _ (lt_min_iff.mp hix).left)
+  exact h.rel_nthLe_of_lt _ _ (Nat.lt_add_right _ (lt_min_iff.mp hix).left)
 #align list.sorted.rel_of_mem_take_of_mem_drop List.Sorted.rel_of_mem_take_of_mem_drop
 
 end Sorted

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
@@ -263,7 +263,7 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
     cases b <;> cases b'
     <;> simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
     · exact this'
-    · exact Nat.lt_add_right (2 * n) (2 * m) 1 this'
+    · exact Nat.lt_add_right 1 this'
     · calc
         2 * n + 1 < 2 * n + 2 := lt.base _
         _ ≤ 2 * m := mul_le_mul_left 2 this

diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean
@@ -128,7 +128,7 @@ theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) :
   simp only [binomial_eq_choose, Function.update_apply,
     h, Ne.def, ite_true, ite_false, not_false_eq_true]
   rw [if_neg h.symm]
-  rw [add_succ, choose_succ_succ, succ_add_eq_succ_add]
+  rw [add_succ, choose_succ_succ, succ_add_eq_add_succ]
   ring
 #align nat.binomial_succ_succ Nat.binomial_succ_succ
 

diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean
@@ -173,8 +173,8 @@ theorem add_pos_iff_pos_or_pos (m n : ℕ) : 0 < m + n ↔ 0 < m ∨ 0 < n :=
       exact Or.inl (succ_pos _))
     (by
       intro h; cases' h with mpos npos
-      · apply add_pos_left mpos
-      apply add_pos_right _ npos)
+      · apply Nat.add_pos_left mpos
+      apply Nat.add_pos_right _ npos)
 #align nat.add_pos_iff_pos_or_pos Nat.add_pos_iff_pos_or_pos
 
 theorem add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 := by

diff --git a/Mathlib/Data/Nat/Pairing.lean b/Mathlib/Data/Nat/Pairing.lean
@@ -130,7 +130,7 @@ theorem pair_lt_pair_left {a₁ a₂} (b) (h : a₁ < a₂) : pair a₁ b < pair
     simp at h₂
     apply add_lt_add_of_le_of_lt
     exact mul_self_le_mul_self h₂
-    exact Nat.lt_add_right _ _ _ h
+    exact Nat.lt_add_right _ h
   · simp at h₁
     simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
     apply add_lt_add

diff --git a/Mathlib/Data/Polynomial/Derivative.lean b/Mathlib/Data/Polynomial/Derivative.lean
@@ -407,7 +407,7 @@ theorem coeff_iterate_derivative {k} (p : R[X]) (m : ℕ) :
         _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
           rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
         _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
-          rw [Nat.succ_add_eq_succ_add]
+          rw [Nat.succ_add_eq_add_succ]
 
 theorem iterate_derivative_mul {n} (p q : R[X]) :
     derivative^[n] (p * q) =

diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean
@@ -63,7 +63,7 @@ namespace Nat
 
 #align nat.one_mul Nat.one_mul
 
-#align nat.succ_add_eq_succ_add Nat.succ_add_eq_succ_add
+#align nat.succ_add_eq_succ_add Nat.succ_add_eq_add_succ
 
 theorem eq_zero_of_mul_eq_zero : ∀ {n m : ℕ}, n * m = 0 → n = 0 ∨ m = 0
   | 0, m => fun _ => Or.inl rfl

diff --git a/Mathlib/Init/Meta/WellFoundedTactics.lean b/Mathlib/Init/Meta/WellFoundedTactics.lean
@@ -21,8 +21,6 @@ theorem Nat.zero_lt_one_add (a : Nat) : 0 < 1 + a := by simp [Nat.one_add]
 
 #align nat.lt_add_right Nat.lt_add_right
 
-theorem Nat.lt_add_left (a b c : Nat) : a < b → a < c + b := fun h =>
-  lt_of_lt_of_le h (Nat.le_add_left _ _)
 #align nat.lt_add_left Nat.lt_add_left
 
 /-

diff --git a/Mathlib/Logic/Equiv/Fin.lean b/Mathlib/Logic/Equiv/Fin.lean
@@ -368,7 +368,7 @@ theorem finAddFlip_apply_natAdd (k : Fin n) (m : ℕ) :
 #align fin_add_flip_apply_nat_add finAddFlip_apply_natAdd
 
 @[simp]
-theorem finAddFlip_apply_mk_left {k : ℕ} (h : k < m) (hk : k < m + n := Nat.lt_add_right k m n h)
+theorem finAddFlip_apply_mk_left {k : ℕ} (h : k < m) (hk : k < m + n := Nat.lt_add_right n h)
     (hnk : n + k < n + m := add_lt_add_left h n) :
     finAddFlip (⟨k, hk⟩ : Fin (m + n)) = ⟨n + k, hnk⟩ := by
   convert finAddFlip_apply_castAdd ⟨k, h⟩ n

diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean
@@ -65,7 +65,7 @@ variable (A : Type*) [CommRing A] [Algebra ℚ A]
 the $n$-th Bernoulli number $B_n$ is defined recursively via
 $$B_n = 1 - \sum_{k < n} \binom{n}{k}\frac{B_k}{n+1-k}$$ -/
 def bernoulli' : ℕ → ℚ :=
-  WellFounded.fix lt_wfRel.wf fun n bernoulli' =>
+  WellFounded.fix Nat.lt_wfRel.wf fun n bernoulli' =>
     1 - ∑ k : Fin n, n.choose k / (n - k + 1) * bernoulli' k k.2
 #align bernoulli' bernoulli'
 

diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean
@@ -412,7 +412,7 @@ theorem pow_add_pow (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : Odd n)
   · exact multiplicity.Nat.pow_add_pow hp.out hp1 hxy hx hn
   · exact Odd.pos hn
   · simp only [add_pos_iff, Nat.succ_pos', or_true_iff]
-  · exact Nat.lt_add_left _ _ _ (pow_pos y.succ_pos _)
+  · exact Nat.lt_add_left _ (pow_pos y.succ_pos _)
 #align padic_val_nat.pow_add_pow padicValNat.pow_add_pow
 
 end padicValNat
diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
@@ -135,10 +135,10 @@ theorem coeff_hermite_of_odd_add {n k : ℕ} (hnk : Odd (n + k)) : coeff (hermit
   · rw [Nat.zero_eq, zero_add k] at hnk
     exact coeff_hermite_of_lt hnk.pos
   · cases' k with k
-    · rw [Nat.succ_add_eq_succ_add] at hnk
+    · rw [Nat.succ_add_eq_add_succ] at hnk
       rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
     · rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
-      · rwa [Nat.succ_add_eq_succ_add] at hnk
+      · rwa [Nat.succ_add_eq_add_succ] at hnk
       · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
         exact (Nat.odd_add.mp hnk).mpr even_two
 #align polynomial.coeff_hermite_of_odd_add Polynomial.coeff_hermite_of_odd_add

diff --git a/Mathlib/RingTheory/PowerSeries/Derivative.lean b/Mathlib/RingTheory/PowerSeries/Derivative.lean
@@ -76,7 +76,7 @@ theorem derivativeFun_mul (f g : R⟦X⟧) :
     derivativeFun (f * g) = f • g.derivativeFun + g • f.derivativeFun := by
   ext n
   have h₁ : n < n + 1 := lt_succ_self n
-  have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ _ _ h₁
+  have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ h₁
   rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
     smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
     coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
@@ -68,7 +68,7 @@ theorem minFacHelper_0 (n : ℕ)
 theorem minFacHelper_1 {n k k' : ℕ} (e : k + 2 = k') (h : MinFacHelper n k)
     (np : minFac n ≠ k) : MinFacHelper n k' := by
   rw [← e]
-  refine ⟨Nat.lt_add_right _ _ _ h.1, ?_, ?_⟩
+  refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
   · rw [add_mod, mod_self, add_zero, mod_mod]
     exact h.2.1
   rcases h.2.2.eq_or_lt with rfl|h2

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,13 +1,13 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/fgdorais/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ddcb08633f442f1af91cad299d6ed114434b54b2",
+   "rev": "89eab993f49a933f981ce078a17118c1f94a3247",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nat-add",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",

diff --git a/lakefile.lean b/lakefile.lean
@@ -26,7 +26,7 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/fgdorais/std4" @ "nat-add"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23"