chore: bump to leanprover/lean4:nightly-2023-02-10 (#2188)

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -439,24 +439,25 @@ def liftAddHom [AddZeroClass M] [AddCommMonoid N] : (α → M →+ N) ≃+ ((α
 
 @[simp]
 theorem liftAddHom_apply [AddCommMonoid M] [AddCommMonoid N] (F : α → M →+ N) (f : α →₀ M) :
-    liftAddHom F f = f.sum fun x => F x :=
+    (liftAddHom (α := α) (M := M) (N := N)) F f = f.sum fun x => F x :=
   rfl
 #align finsupp.lift_add_hom_apply Finsupp.liftAddHom_apply
 
 @[simp]
 theorem liftAddHom_symm_apply [AddCommMonoid M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) :
-    liftAddHom.symm F x = F.comp (singleAddHom x) :=
+    (liftAddHom (α := α) (M := M) (N := N)).symm F x = F.comp (singleAddHom x) :=
   rfl
 #align finsupp.lift_add_hom_symm_apply Finsupp.liftAddHom_symm_apply
 
 theorem liftAddHom_symm_apply_apply [AddCommMonoid M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α)
-    (y : M) : liftAddHom.symm F x y = F (single x y) :=
+    (y : M) : (liftAddHom (α := α) (M := M) (N := N)).symm F x y = F (single x y) :=
   rfl
 #align finsupp.lift_add_hom_symm_apply_apply Finsupp.liftAddHom_symm_apply_apply
 
 @[simp]
 theorem liftAddHom_singleAddHom [AddCommMonoid M] :
-    liftAddHom (singleAddHom : α → M →+ α →₀ M) = AddMonoidHom.id _ :=
+    (liftAddHom (α := α) (M := M) (N := α →₀ M)) (singleAddHom : α → M →+ α →₀ M) =
+      AddMonoidHom.id _ :=
   liftAddHom.toEquiv.apply_eq_iff_eq_symm_apply.2 rfl
 #align finsupp.lift_add_hom_single_add_hom Finsupp.liftAddHom_singleAddHom
 
@@ -485,26 +486,29 @@ theorem sum_univ_single' [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
 -- Porting note: simp can prove this
 -- @[simp]
 theorem liftAddHom_apply_single [AddCommMonoid M] [AddCommMonoid N] (f : α → M →+ N) (a : α)
-    (b : M) : liftAddHom f (single a b) = f a b :=
+    (b : M) : (liftAddHom (α := α) (M := M) (N := N)) f (single a b) = f a b :=
   sum_single_index (f a).map_zero
 #align finsupp.lift_add_hom_apply_single Finsupp.liftAddHom_apply_single
 
 @[simp]
 theorem liftAddHom_comp_single [AddCommMonoid M] [AddCommMonoid N] (f : α → M →+ N) (a : α) :
-    (liftAddHom f).comp (singleAddHom a) = f a :=
+    ((liftAddHom (α := α) (M := M) (N := N)) f).comp (singleAddHom a) = f a :=
   AddMonoidHom.ext fun b => liftAddHom_apply_single f a b
 #align finsupp.lift_add_hom_comp_single Finsupp.liftAddHom_comp_single
 
 theorem comp_liftAddHom [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P)
-    (f : α → M →+ N) : g.comp (liftAddHom f) = liftAddHom fun a => g.comp (f a) :=
+    (f : α → M →+ N) :
+    g.comp ((liftAddHom (α := α) (M := M) (N := N)) f) =
+      (liftAddHom (α := α) (M := M) (N := P)) fun a => g.comp (f a) :=
   liftAddHom.symm_apply_eq.1 <|
     funext fun a => by
       rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
 #align finsupp.comp_lift_add_hom Finsupp.comp_liftAddHom
 
 theorem sum_sub_index [AddCommGroup β] [AddCommGroup γ] {f g : α →₀ β} {h : α → β → γ}
     (h_sub : ∀ a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) : (f - g).sum h = f.sum h - g.sum h :=
-  (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
+  ((liftAddHom (α := α) (M := β) (N := γ)) fun a =>
+    AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
 #align finsupp.sum_sub_index Finsupp.sum_sub_index
 
 @[to_additive]

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -168,7 +168,7 @@ class CancelCommMonoidWithZero (M₀ : Type _) extends CommMonoidWithZero M₀,
 
 instance (priority := 100) CancelCommMonoidWithZero.toCancelMonoidWithZero
     [CancelCommMonoidWithZero M₀] : CancelMonoidWithZero M₀ :=
-{ IsLeftCancelMulZero.to_isCancelMulZero with }
+{ IsLeftCancelMulZero.to_isCancelMulZero (M₀ := M₀) with }
 
 /-- A type `G₀` is a “group with zero” if it is a monoid with zero element (distinct from `1`)
 such that every nonzero element is invertible.

Mathlib/Algebra/Order/Positive/Ring.lean

@@ -140,7 +140,7 @@ section mul_comm
 instance orderedCommMonoid [StrictOrderedCommSemiring R] [Nontrivial R] :
     OrderedCommMonoid { x : R // 0 < x } :=
   { Subtype.partialOrder _,
-    Subtype.coe_injective.commMonoid (Subtype.val) val_one val_mul val_pow with
+    Subtype.coe_injective.commMonoid (M₂ := R) (Subtype.val) val_one val_mul val_pow with
     mul_le_mul_left := fun _ _ hxy c =>
       Subtype.coe_le_coe.1 <| mul_le_mul_of_nonneg_left hxy c.2.le }
 #align positive.subtype.ordered_comm_monoid Positive.orderedCommMonoid

Mathlib/Algebra/Order/Sub/Canonical.lean

@@ -508,7 +508,7 @@ theorem tsub_min : a - min a b = a - b := by
 #align tsub_min tsub_min
 
 theorem tsub_add_min : a - b + min a b = a := by
-  rw [← tsub_min, tsub_add_cancel_of_le]
+  rw [← tsub_min, @tsub_add_cancel_of_le]
   apply min_le_left
 #align tsub_add_min tsub_add_min
 

Mathlib/Algebra/Star/Basic.lean

@@ -326,7 +326,7 @@ end
 /-- `star` as a ring automorphism, for commutative `R`. -/
 @[simps apply]
 def starRingAut [CommSemiring R] [StarRing R] : RingAut R :=
-  { starAddEquiv, starMulAut with toFun := star }
+  { starAddEquiv, starMulAut (R := R) with toFun := star }
 #align star_ring_aut starRingAut
 #align star_ring_aut_apply starRingAut_apply
 

Mathlib/Combinatorics/Colex.lean

@@ -386,8 +386,8 @@ instance [LinearOrder α] [Fintype α] : OrderTop (Finset.Colex α)
   le_top _ := colex_le_of_subset (subset_univ _)
 
 instance [LinearOrder α] : Lattice (Finset.Colex α) :=
-  { (by infer_instance : SemilatticeSup (Finset.Colex α)),
-    (by infer_instance : SemilatticeInf (Finset.Colex α)) with }
+  { inferInstanceAs (SemilatticeSup (Finset.Colex α)),
+    inferInstanceAs (SemilatticeInf (Finset.Colex α)) with }
 
 instance [LinearOrder α] [Fintype α] : BoundedOrder (Finset.Colex α) :=
   { (by infer_instance : OrderTop (Finset.Colex α)),

Mathlib/Data/Finset/Pointwise.lean

@@ -1890,7 +1890,7 @@ theorem mem_inv_smul_finset_iff₀ (ha : a ≠ 0) : b ∈ a⁻¹ • s ↔ a •
   show _ ∈ (Units.mk0 a ha)⁻¹ • _ ↔ _ from mem_inv_smul_finset_iff
 #align finset.mem_inv_smul_finset_iff₀ Finset.mem_inv_smul_finset_iff₀
 
-@[simp]
+-- @[simp] -- Porting note: `simpNF` linter times out
 theorem smul_finset_subset_smul_finset_iff₀ (ha : a ≠ 0) : a • s ⊆ a • t ↔ s ⊆ t :=
   show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_finset_subset_smul_finset_iff
 #align finset.smul_finset_subset_smul_finset_iff₀ Finset.smul_finset_subset_smul_finset_iff₀

Mathlib/Data/List/Basic.lean

@@ -1564,7 +1564,7 @@ theorem modifyNthTail_modifyNthTail_le {f g : List α → List α} (m n : ℕ) (
     (l.modifyNthTail f n).modifyNthTail g m =
       l.modifyNthTail (fun l => (f l).modifyNthTail g (m - n)) n := by
   rcases exists_add_of_le h with ⟨m, rfl⟩
-  rw [add_tsub_cancel_left, add_comm, modifyNthTail_modifyNthTail]
+  rw [@add_tsub_cancel_left, add_comm, modifyNthTail_modifyNthTail]
 #align list.modify_nth_tail_modify_nth_tail_le List.modifyNthTail_modifyNthTail_le
 
 theorem modifyNthTail_modifyNthTail_same {f g : List α → List α} (n : ℕ) (l : List α) :
@@ -2355,7 +2355,7 @@ theorem reverse_take {α} {xs : List α} (n : ℕ) (h : n ≤ xs.length) :
   · replace h' := le_of_succ_le_succ h'
     rw [take_append_of_le_length, xs_ih _ h']
     rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
-    · rwa [succ_eq_add_one, ← tsub_add_eq_add_tsub]
+    · rwa [succ_eq_add_one, ← @tsub_add_eq_add_tsub]
     · rwa [length_reverse]
   · subst h'
     rw [length, tsub_self, drop]

Mathlib/Data/List/BigOperators/Basic.lean

@@ -607,7 +607,7 @@ theorem headI_le_sum (L : List ℕ) : L.headI ≤ L.sum :=
 
 /-- This relies on `default ℕ = 0`. -/
 theorem tail_sum (L : List ℕ) : L.tail.sum = L.sum - L.headI := by
-  rw [← headI_add_tail_sum L, add_comm, add_tsub_cancel_right]
+  rw [← headI_add_tail_sum L, add_comm, @add_tsub_cancel_right]
 #align list.tail_sum List.tail_sum
 
 section Alternating

Mathlib/Data/List/Lattice.lean

@@ -255,7 +255,7 @@ theorem count_bagInter {a : α} :
     · rw [cons_bagInter_of_pos _ hb, count_cons', count_cons', count_bagInter, count_erase, ←
         min_add_add_right]
       by_cases ab : a = b
-      · rw [if_pos ab, tsub_add_cancel_of_le]
+      · rw [if_pos ab, @tsub_add_cancel_of_le]
         rwa [succ_le_iff, count_pos, ab]
       · rw [if_neg ab, tsub_zero, add_zero, add_zero]
     · rw [cons_bagInter_of_neg _ hb, count_bagInter]

Mathlib/Data/Nat/Dist.lean

@@ -78,8 +78,8 @@ theorem dist_zero_left (n : ℕ) : dist 0 n = n :=
 theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
   calc
     dist (n + k) (m + k) = n + k - (m + k) + (m + k - (n + k)) := rfl
-    _ = n - m + (m + k - (n + k)) := by rw [add_tsub_add_eq_tsub_right]
-    _ = n - m + (m - n) := by rw [add_tsub_add_eq_tsub_right]
+    _ = n - m + (m + k - (n + k)) := by rw [@add_tsub_add_eq_tsub_right]
+    _ = n - m + (m - n) := by rw [@add_tsub_add_eq_tsub_right]
 
 #align nat.dist_add_add_right Nat.dist_add_add_right
 

Mathlib/Data/Nat/Order/Basic.lean

@@ -484,7 +484,7 @@ theorem half_le_of_sub_le_half {a b : ℕ} (h : a - b ≤ a / 2) : a / 2 ≤ b :
 theorem two_mul_odd_div_two (hn : n % 2 = 1) : 2 * (n / 2) = n - 1 := by
   conv =>
     rhs
-    rw [← Nat.mod_add_div n 2, hn, add_tsub_cancel_left]
+    rw [← Nat.mod_add_div n 2, hn, @add_tsub_cancel_left]
 #align nat.two_mul_odd_div_two Nat.two_mul_odd_div_two
 
 theorem div_dvd_of_dvd (h : n ∣ m) : m / n ∣ m :=
@@ -521,7 +521,7 @@ theorem not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
 /-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/
 theorem sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by
   rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, tsub_add_eq_tsub_tsub,
-    add_tsub_cancel_left, ← mul_tsub k, Nat.mul_mod_right]
+    @add_tsub_cancel_left, ← mul_tsub k, Nat.mul_mod_right]
 #align nat.sub_mod_eq_zero_of_mod_eq Nat.sub_mod_eq_zero_of_mod_eq
 
 @[simp]

Mathlib/Data/Nat/Order/Lemmas.lean

@@ -135,10 +135,10 @@ theorem succ_div : ∀ a b : ℕ, (a + 1) / b = a / b + if b ∣ a + 1 then 1 el
         rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b,
           add_comm (_ - _), add_assoc, tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
       have wf : a - b < a + 1 := lt_succ_of_le tsub_le_self
-      rw [if_pos h₁, if_pos h₂, add_tsub_add_eq_tsub_right, ← tsub_add_eq_add_tsub hb_le_a,
+      rw [if_pos h₁, if_pos h₂, @add_tsub_add_eq_tsub_right, ← tsub_add_eq_add_tsub hb_le_a,
         have := wf
         succ_div (a - b),
-        add_tsub_add_eq_tsub_right]
+        @add_tsub_add_eq_tsub_right]
       simp [dvd_iff, succ_eq_add_one, add_comm 1, add_assoc]
     · have hba : ¬b ≤ a := not_le_of_gt (lt_trans (lt_succ_self a) (lt_of_not_ge hb_le_a1))
       have hb_dvd_a : ¬b + 1 ∣ a + 2 := fun h =>

Mathlib/GroupTheory/Submonoid/Inverses.lean

@@ -36,11 +36,10 @@ namespace Submonoid
 
 @[to_additive]
 noncomputable instance [Monoid M] : Group (IsUnit.submonoid M) :=
-  { show Monoid (IsUnit.submonoid M) by
-      infer_instance with
-    inv := fun x ↦ ⟨_, x.prop.unit⁻¹.isUnit⟩
-    mul_left_inv := fun x ↦ by
-      exact Subtype.mk_eq_mk.2 ((Units.val_mul _ _).trans x.prop.unit.inv_val) }
+  { inferInstanceAs (Monoid (IsUnit.submonoid M)) with
+    inv := fun x ↦ ⟨x.prop.unit⁻¹.val, x.prop.unit⁻¹.isUnit⟩
+    mul_left_inv := fun x ↦
+      Subtype.ext ((Units.val_mul x.prop.unit⁻¹ _).trans x.prop.unit.inv_val) }
 
 @[to_additive]
 noncomputable instance [CommMonoid M] : CommGroup (IsUnit.submonoid M) :=

Mathlib/Tactic/Have.lean

@@ -43,7 +43,10 @@ def haveLetCore (goal : MVarId) (name : Option Syntax) (bis : Array Syntax)
     let (goal1, t, p) ← elabBinders fun es ↦ do
       let t ← match t with
       | none => mkFreshTypeMVar
-      | some t => Tactic.elabTerm.go t none
+      | some stx => withRef stx do
+          let e ← Term.elabTerm stx none
+          Term.synthesizeSyntheticMVars false
+          instantiateMVars e
       let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
       pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)
     let (fvar, goal2) ← (← declFn goal n t p).intro1P

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-03
+leanprover/lean4:nightly-2023-02-10