chore: bump to std4#261 (#7141)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Sep 22, 2023 · 5f13726 · 5f13726
1 parent f10b516
commit 5f13726
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 6 deletions.
diff --git a/Mathlib/Algebra/Hom/GroupInstances.lean b/Mathlib/Algebra/Hom/GroupInstances.lean
@@ -71,7 +71,7 @@ instance MonoidHom.commGroup {M G} [MulOneClass M] [CommGroup G] : CommGroup (M
       simp [zpow_ofNat, pow_succ],
     zpow_neg' := fun n f => by
       ext x
-      simp [Nat.succ_eq_add_one, zpow_ofNat] }
+      simp [Nat.succ_eq_add_one, zpow_ofNat, -Int.natCast_add] }
 
 instance [AddCommMonoid M] : AddCommMonoid (AddMonoid.End M) :=
   AddMonoidHom.addCommMonoid

diff --git a/Mathlib/Data/Int/Cast/Basic.lean b/Mathlib/Data/Int/Cast/Basic.lean
@@ -106,7 +106,7 @@ theorem cast_negOfNat (n : ℕ) : ((negOfNat n : ℤ) : R) = -n := by simp [Int.
 
 @[simp, norm_cast]
 theorem cast_add : ∀ m n, ((m + n : ℤ) : R) = m + n
-  | (m : ℕ), (n : ℕ) => by simp [← Int.ofNat_add, Nat.cast_add]
+  | (m : ℕ), (n : ℕ) => by simp [-Int.natCast_add, ← Int.ofNat_add]
   | (m : ℕ), -[n+1] => by erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_add_neg]
   | -[m+1], (n : ℕ) => by
     erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, add_assoc,

diff --git a/Mathlib/Data/Int/Order/Basic.lean b/Mathlib/Data/Int/Order/Basic.lean
@@ -89,7 +89,7 @@ theorem coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
 
 theorem sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign := by
   have : (1 : ℤ) ≠ -1 := by decide
-  rintro ((_ | m) | m) ((_ | n) | n) <;> simp [this, this.symm]
+  rintro ((_ | m) | m) ((_ | n) | n) <;> simp [this, this.symm, Int.negSucc_add_negSucc]
   rw [Int.sign_eq_one_iff_pos]
   apply Int.add_pos <;> · exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
 #align int.sign_add_eq_of_sign_eq Int.sign_add_eq_of_sign_eq

diff --git a/Mathlib/Init/Data/Int/CompLemmas.lean b/Mathlib/Init/Data/Int/CompLemmas.lean
@@ -122,15 +122,17 @@ theorem natAbs_of_negSucc (n : ℕ) : natAbs (negSucc n) = Nat.succ n :=
 protected theorem natAbs_add_nonneg :
     ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → natAbs (a + b) = natAbs a + natAbs b
   | ofNat n, ofNat m, _, _ => by
-    simp [natAbs_ofNat_core]
+    simp only [ofNat_eq_coe, natAbs_ofNat]
+    simp only [Int.ofNat_add_ofNat]
+    simp only [← ofNat_eq_coe, natAbs_ofNat_core]
   | _, negSucc m, _, h₂ => absurd (negSucc_lt_zero m) (not_lt_of_ge h₂)
   | negSucc n, _, h₁, _ => absurd (negSucc_lt_zero n) (not_lt_of_ge h₁)
 #align int.nat_abs_add_nonneg Int.natAbs_add_nonneg
 
 protected theorem natAbs_add_neg :
     ∀ {a b : Int}, a < 0 → b < 0 → natAbs (a + b) = natAbs a + natAbs b
   | negSucc n, negSucc m, _, _ => by
-    simp [natAbs_of_negSucc, Nat.succ_add, Nat.add_succ]
+    simp [negSucc_add_negSucc, natAbs_of_negSucc, Nat.succ_add, Nat.add_succ]
 #align int.nat_abs_add_neg Int.natAbs_add_neg
 
 set_option linter.deprecated false in

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -36,7 +36,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "32c1912a12dd38be9651ee70275e636ed4c34fc7",
+    "rev": "524aae5c8000f6e38433ee0ad95bdae3cfa88fee",
     "opts": {},
     "name": "std",
     "inputRev?": "main",