chore: update to 2023-01-10 nightly (#1447)

- [x] depends on: leanprover-community/batteries#83
- [x] depends on: leanprover-community/aesop#38

Mathlib/Algebra/Group/Pi.lean

@@ -623,7 +623,7 @@ section Piecewise
 theorem Set.piecewise_mul [∀ i, Mul (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)]
     (f₁ f₂ g₁ g₂ : ∀ i, f i) :
     s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂ :=
-  s.piecewise_op₂ _ _ _ _ fun _ => (· * ·)
+  s.piecewise_op₂ f₁ _ _ _ fun _ => (· * ·)
 #align set.piecewise_mul Set.piecewise_mul
 #align set.piecewise_add Set.piecewise_add
 
@@ -638,7 +638,7 @@ theorem Set.piecewise_inv [∀ i, Inv (f i)] (s : Set I) [∀ i, Decidable (i 
 theorem Set.piecewise_div [∀ i, Div (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)]
     (f₁ f₂ g₁ g₂ : ∀ i, f i) :
     s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂ :=
-  s.piecewise_op₂ _ _ _ _ fun _ => (· / ·)
+  s.piecewise_op₂ f₁ _ _ _ fun _ => (· / ·)
 #align set.piecewise_div Set.piecewise_div
 #align set.piecewise_sub Set.piecewise_sub
 

Mathlib/Data/Int/Cast/Defs.lean

@@ -37,11 +37,8 @@ protected def Int.castDef {R : Type u} [NatCast R] [Neg R] : ℤ → R
   | Int.negSucc n => -(n + 1 : ℕ)
 #align int.cast_def Int.castDef
 
-/-- Type class for the canonical homomorphism `ℤ → R`. -/
-class IntCast (R : Type u) where
-  /-- The canonical map `ℤ → R`. -/
-  intCast : ℤ → R
 #align has_int_cast IntCast
+#align int.cast Int.cast
 
 /-! ### Additive groups with one -/
 
@@ -62,17 +59,6 @@ class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGro
 #align add_group_with_one.int_cast_of_nat AddGroupWithOne.intCast_ofNat
 #align add_group_with_one.int_cast_neg_succ_of_nat AddGroupWithOne.intCast_negSucc
 
-namespace Int
-
-/-- Canonical homomorphism from the integers to any ring(-like) structure `R` -/
-@[coe] def cast [IntCast R] : ℤ → R := IntCast.intCast
-#align int.cast Int.cast
-
-instance [IntCast R] : CoeTail ℤ R where coe := cast
-instance [IntCast R] : CoeHTCT ℤ R where coe := cast
-
-end Int
-
 /-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/
 class AddCommGroupWithOne (R : Type u) extends AddCommGroup R, AddGroupWithOne R
 #align add_comm_group_with_one AddCommGroupWithOne

Mathlib/Data/List/Defs.lean

@@ -105,7 +105,7 @@ def alternatingProd {G : Type _} [One G] [Mul G] [Inv G] : List G → G
 
 /-- `findM tac l` returns the first element of `l` on which `tac` succeeds, and
 fails otherwise. -/
-def findM {α} {m : Type u → Type v} [Monad m] [Alternative m] (tac : α → m PUnit) : List α → m α :=
+def findM {α} {m : Type u → Type v} [Alternative m] (tac : α → m PUnit) : List α → m α :=
   List.firstM <| fun a => (tac a) $> a
 #align list.mfind List.findM
 

Mathlib/GroupTheory/GroupAction/Pi.lean

@@ -256,7 +256,7 @@ namespace Set
 @[to_additive]
 theorem piecewise_smul {α : Type _} [∀ i, SMul α (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)]
     (c : α) (f₁ g₁ : ∀ i, f i) : s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁ :=
-  s.piecewise_op (δ' := f) _ _ fun _ => (· • ·) c
+  s.piecewise_op (δ' := f) f₁ _ fun _ => (· • ·) c
 #align set.piecewise_smul Set.piecewise_smul
 
 end Set

lake-manifest.json

@@ -34,7 +34,7 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "72610cec1cd686884a08704f5fa91b45262136f9",
+    "rev": "645e92db52499582bb31984396a5e41772241012",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
@@ -52,6 +52,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "570141abe5886d697b2544630e8e0e3aec9df240",
+    "rev": "fde95b16907bf38ea3f310af406868fc6bcf48d1",
     "name": "std",
     "inputRev?": "main"}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-01-06
+leanprover/lean4:nightly-2023-01-10