chore: bump Std to leanprover-community/batteries#541 (#9828)

Notable changes: lemmas were added in leanprover-community/batteries#538 about `gcd` and `lcm`, that now have implicit arguments. Mostly this is a positive change in Mathlib, we can just delete the arguments. The one to consider in review is in [`ModEq`](https://github.com/leanprover-community/mathlib4/pull/9828/files#diff-bf7908935cfca2e7d7959ec20d701fcda99586d0b7620b05b0a803988fdbd4fc).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Data/Int/GCD.lean

@@ -231,9 +231,6 @@ theorem dvd_of_mul_dvd_mul_right {i j k : ℤ} (k_non_zero : k ≠ 0) (H : i * k
   rw [mul_comm i k, mul_comm j k] at H; exact dvd_of_mul_dvd_mul_left k_non_zero H
 #align int.dvd_of_mul_dvd_mul_right Int.dvd_of_mul_dvd_mul_right
 
-/-- ℤ specific version of least common multiple. -/
-def lcm (i j : ℤ) : ℕ :=
-  Nat.lcm (natAbs i) (natAbs j)
 #align int.lcm Int.lcm
 
 theorem lcm_def (i j : ℤ) : lcm i j = Nat.lcm (natAbs i) (natAbs j) :=
@@ -244,12 +241,7 @@ protected theorem coe_nat_lcm (m n : ℕ) : Int.lcm ↑m ↑n = Nat.lcm m n :=
   rfl
 #align int.coe_nat_lcm Int.coe_nat_lcm
 
-theorem gcd_dvd_left (i j : ℤ) : (gcd i j : ℤ) ∣ i :=
-  dvd_natAbs.mp <| coe_nat_dvd.mpr <| Nat.gcd_dvd_left _ _
 #align int.gcd_dvd_left Int.gcd_dvd_left
-
-theorem gcd_dvd_right (i j : ℤ) : (gcd i j : ℤ) ∣ j :=
-  dvd_natAbs.mp <| coe_nat_dvd.mpr <| Nat.gcd_dvd_right _ _
 #align int.gcd_dvd_right Int.gcd_dvd_right
 
 theorem dvd_gcd {i j k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) : k ∣ gcd i j :=
@@ -281,23 +273,10 @@ theorem gcd_zero_left (i : ℤ) : gcd 0 i = natAbs i := by simp [gcd]
 theorem gcd_zero_right (i : ℤ) : gcd i 0 = natAbs i := by simp [gcd]
 #align int.gcd_zero_right Int.gcd_zero_right
 
-@[simp]
-theorem gcd_one_left (i : ℤ) : gcd 1 i = 1 :=
-  Nat.gcd_one_left _
-#align int.gcd_one_left Int.gcd_one_left
-
-@[simp]
-theorem gcd_one_right (i : ℤ) : gcd i 1 = 1 :=
-  Nat.gcd_one_right _
-#align int.gcd_one_right Int.gcd_one_right
-
-@[simp]
-theorem gcd_neg_right {x y : ℤ} : gcd x (-y) = gcd x y := by rw [Int.gcd, Int.gcd, natAbs_neg]
-#align int.gcd_neg_right Int.gcd_neg_right
-
-@[simp]
-theorem gcd_neg_left {x y : ℤ} : gcd (-x) y = gcd x y := by rw [Int.gcd, Int.gcd, natAbs_neg]
-#align int.gcd_neg_left Int.gcd_neg_left
+#align int.gcd_one_left Int.one_gcd
+#align int.gcd_one_right Int.gcd_one
+#align int.gcd_neg_right Int.gcd_neg
+#align int.gcd_neg_left Int.neg_gcd
 
 theorem gcd_mul_left (i j k : ℤ) : gcd (i * j) (i * k) = natAbs i * gcd j k := by
   rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]
@@ -332,15 +311,15 @@ theorem gcd_div {i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) :
 #align int.gcd_div Int.gcd_div
 
 theorem gcd_div_gcd_div_gcd {i j : ℤ} (H : 0 < gcd i j) : gcd (i / gcd i j) (j / gcd i j) = 1 := by
-  rw [gcd_div (gcd_dvd_left i j) (gcd_dvd_right i j), natAbs_ofNat, Nat.div_self H]
+  rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_ofNat, Nat.div_self H]
 #align int.gcd_div_gcd_div_gcd Int.gcd_div_gcd_div_gcd
 
 theorem gcd_dvd_gcd_of_dvd_left {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd i j ∣ gcd k j :=
-  Int.coe_nat_dvd.1 <| dvd_gcd ((gcd_dvd_left i j).trans H) (gcd_dvd_right i j)
+  Int.coe_nat_dvd.1 <| dvd_gcd (gcd_dvd_left.trans H) gcd_dvd_right
 #align int.gcd_dvd_gcd_of_dvd_left Int.gcd_dvd_gcd_of_dvd_left
 
 theorem gcd_dvd_gcd_of_dvd_right {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd j i ∣ gcd j k :=
-  Int.coe_nat_dvd.1 <| dvd_gcd (gcd_dvd_left j i) ((gcd_dvd_right j i).trans H)
+  Int.coe_nat_dvd.1 <| dvd_gcd gcd_dvd_left (gcd_dvd_right.trans H)
 #align int.gcd_dvd_gcd_of_dvd_right Int.gcd_dvd_gcd_of_dvd_right
 
 theorem gcd_dvd_gcd_mul_left (i j k : ℤ) : gcd i j ∣ gcd (k * i) j :=
@@ -373,8 +352,8 @@ theorem ne_zero_of_gcd {x y : ℤ} (hc : gcd x y ≠ 0) : x ≠ 0 ∨ y ≠ 0 :=
 
 theorem exists_gcd_one {m n : ℤ} (H : 0 < gcd m n) :
     ∃ m' n' : ℤ, gcd m' n' = 1 ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
-  ⟨_, _, gcd_div_gcd_div_gcd H, (Int.ediv_mul_cancel (gcd_dvd_left m n)).symm,
-    (Int.ediv_mul_cancel (gcd_dvd_right m n)).symm⟩
+  ⟨_, _, gcd_div_gcd_div_gcd H, (Int.ediv_mul_cancel gcd_dvd_left).symm,
+    (Int.ediv_mul_cancel gcd_dvd_right).symm⟩
 #align int.exists_gcd_one Int.exists_gcd_one
 
 theorem exists_gcd_one' {m n : ℤ} (H : 0 < gcd m n) :
@@ -397,13 +376,13 @@ theorem gcd_dvd_iff {a b : ℤ} {n : ℕ} : gcd a b ∣ n ↔ ∃ x y : ℤ, ↑
   · rintro ⟨x, y, h⟩
     rw [← Int.coe_nat_dvd, h]
     exact
-      dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left a b) _) (dvd_mul_of_dvd_left (gcd_dvd_right a b) y)
+      dvd_add (dvd_mul_of_dvd_left gcd_dvd_left _) (dvd_mul_of_dvd_left gcd_dvd_right y)
 #align int.gcd_dvd_iff Int.gcd_dvd_iff
 
 theorem gcd_greatest {a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b)
     (hd : ∀ e : ℤ, e ∣ a → e ∣ b → e ∣ d) : d = gcd a b :=
   dvd_antisymm hd_pos (ofNat_zero_le (gcd a b)) (dvd_gcd hda hdb)
-    (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b))
+    (hd _ gcd_dvd_left gcd_dvd_right)
 #align int.gcd_greatest Int.gcd_greatest
 
 /-- Euclid's lemma: if `a ∣ b * c` and `gcd a c = 1` then `a ∣ b`.
@@ -475,22 +454,8 @@ theorem lcm_one_right (i : ℤ) : lcm i 1 = natAbs i := by
   apply Nat.lcm_one_right
 #align int.lcm_one_right Int.lcm_one_right
 
-@[simp]
-theorem lcm_self (i : ℤ) : lcm i i = natAbs i := by
-  rw [Int.lcm]
-  apply Nat.lcm_self
 #align int.lcm_self Int.lcm_self
-
-theorem dvd_lcm_left (i j : ℤ) : i ∣ lcm i j := by
-  rw [Int.lcm]
-  apply coe_nat_dvd_right.mpr
-  apply Nat.dvd_lcm_left
 #align int.dvd_lcm_left Int.dvd_lcm_left
-
-theorem dvd_lcm_right (i j : ℤ) : j ∣ lcm i j := by
-  rw [Int.lcm]
-  apply coe_nat_dvd_right.mpr
-  apply Nat.dvd_lcm_right
 #align int.dvd_lcm_right Int.dvd_lcm_right
 
 theorem lcm_dvd {i j k : ℤ} : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k := by

Mathlib/Data/Int/ModEq.lean

@@ -223,14 +223,13 @@ lemma of_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
 theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) :
     a ≡ b [ZMOD m / gcd m c] := by
   letI d := gcd m c
-  have hmd := gcd_dvd_left m c
-  have hcd := gcd_dvd_right m c
   rw [modEq_iff_dvd] at h ⊢
   -- porting note: removed `show` due to leanprover-community/mathlib4#3305
   refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
-  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
-    exact Int.ediv_dvd_ediv hmd h
-  · rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
+  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) gcd_dvd_right, sub_mul]
+    exact Int.ediv_dvd_ediv gcd_dvd_left h
+  · rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_ofNat,
+      Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
 #align int.modeq.cancel_right_div_gcd Int.ModEq.cancel_right_div_gcd
 
 /-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/

Mathlib/Init/Data/Bool/Lemmas.lean

@@ -107,10 +107,10 @@ theorem coe_false : ↑false = False := by simp
 theorem coe_true : ↑true = True := by simp
 #align coe_tt Bool.coe_true
 
-theorem coe_sort_false : (↥false : Prop) = False := by simp
+theorem coe_sort_false : (false : Prop) = False := by simp
 #align coe_sort_ff Bool.coe_sort_false
 
-theorem coe_sort_true : (↥true : Prop) = True := by simp
+theorem coe_sort_true : (true : Prop) = True := by simp
 #align coe_sort_tt Bool.coe_sort_true
 
 theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p := by simp

Mathlib/Lean/Expr/Basic.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lewis,
 Floris van Doorn, E.W.Ayers, Arthur Paulino
 -/
+import Lean.Meta.Tactic.Rewrite
 import Std.Lean.Expr
+import Std.Data.Rat.Basic
 import Std.Data.List.Basic
 
 /-!

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -219,8 +219,8 @@ theorem isClassified_of_normalize_isPrimitiveClassified (hc : h.normalize.IsPrim
   convert h.normalize.mul_isClassified (Int.gcd x y)
         (isClassified_of_isPrimitiveClassified h.normalize hc) <;>
     rw [Int.mul_ediv_cancel']
-  · exact Int.gcd_dvd_left x y
-  · exact Int.gcd_dvd_right x y
+  · exact Int.gcd_dvd_left
+  · exact Int.gcd_dvd_right
   · exact h.gcd_dvd
 #align pythagorean_triple.is_classified_of_normalize_is_primitive_classified PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassified
 

Mathlib/RingTheory/Int/Basic.lean

@@ -136,8 +136,8 @@ section GCDMonoid
 instance : GCDMonoid ℤ where
   gcd a b := Int.gcd a b
   lcm a b := Int.lcm a b
-  gcd_dvd_left a b := Int.gcd_dvd_left _ _
-  gcd_dvd_right a b := Int.gcd_dvd_right _ _
+  gcd_dvd_left a b := Int.gcd_dvd_left
+  gcd_dvd_right a b := Int.gcd_dvd_right
   dvd_gcd := dvd_gcd
   gcd_mul_lcm a b := by
     rw [← Int.ofNat_mul, gcd_mul_lcm, coe_natAbs, abs_eq_normalize]
@@ -246,7 +246,7 @@ theorem natAbs_euclideanDomain_gcd (a b : ℤ) :
   · rw [Int.natAbs_dvd]
     exact Int.dvd_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)
   · rw [Int.dvd_natAbs]
-    exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left _ _) (Int.gcd_dvd_right _ _)
+    exact EuclideanDomain.dvd_gcd Int.gcd_dvd_left Int.gcd_dvd_right
 #align int.nat_abs_euclidean_domain_gcd Int.natAbs_euclideanDomain_gcd
 
 end Int

Mathlib/Tactic/ExtractGoal.lean

@@ -3,6 +3,8 @@ Copyright (c) 2017 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Kyle Miller, Damiano Testa
 -/
+import Lean.Elab.Tactic
+import Lean.Meta.Tactic.Cleanup
 import Std.Lean.Meta.Inaccessible
 
 /-!

Mathlib/Tactic/GeneralizeProofs.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Alex J. Best. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
+import Lean.Meta.AbstractNestedProofs
 import Mathlib.Lean.Expr.Basic
 
 /-!

Mathlib/Tactic/NormNum/GCD.lean

@@ -24,8 +24,8 @@ theorem int_gcd_helper' {d : ℕ} {x y : ℤ} (a b : ℤ) (h₁ : (d : ℤ) ∣
   refine Nat.dvd_antisymm ?_ (Int.coe_nat_dvd.1 (Int.dvd_gcd h₁ h₂))
   rw [← Int.coe_nat_dvd, ← h₃]
   apply dvd_add
-  · exact (Int.gcd_dvd_left _ _).mul_right _
-  · exact (Int.gcd_dvd_right _ _).mul_right _
+  · exact Int.gcd_dvd_left.mul_right _
+  · exact Int.gcd_dvd_right.mul_right _
 
 theorem nat_gcd_helper_dvd_left (x y : ℕ) (h : y % x = 0) : Nat.gcd x y = x :=
   Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero h)

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "1d85fd7db28700b28043d6370dd1ebc426de4d5d",
+   "rev": "1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70",
+   "rev": "1c638703ed1c0c42aed2687acbeda67cec801454",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",