chore: bump to 2022-12-22 (#1157)

leanprover-community · Dec 23, 2022 · 4b0358a · 4b0358a
1 parent 8eeb13b
commit 4b0358a
Show file tree

Hide file tree

Showing 14 changed files with 18 additions and 31 deletions.
diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean
@@ -79,7 +79,7 @@ variable [CommMonoidWithZero β] {F : Type _} {G : Type _} [MonoidWithZeroHomCla
   [MulHomClass G β α] (f : F) (g : G) {p : α}
 
 theorem comap_prime (hinv : ∀ a, g (f a : β) = a) (hp : Prime (f p)) : Prime p :=
-  ⟨fun h => hp.1 <| by simp [h]; rw [map_zero], fun h => hp.2.1 <| h.map f, fun a b h => by
+  ⟨fun h => hp.1 <| by simp [h], fun h => hp.2.1 <| h.map f, fun a b h => by
     refine'
         (hp.2.2 (f a) (f b) <| by
               convert map_dvd f h

diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean
@@ -62,7 +62,7 @@ variable {α β K : Type _}
 is defined as `(a / b : K) = (a : K) * (b : K)⁻¹`.
 Use `coe` instead of `rat.castRec` for better definitional behaviour.
 -/
-def Rat.castRec [CoeTail ℕ K] [CoeTail ℤ K] [Mul K] [Inv K] : ℚ → K
+def Rat.castRec [NatCast K] [IntCast K] [Mul K] [Inv K] : ℚ → K
   | ⟨a, b, _, _⟩ => ↑a * (↑b)⁻¹
 #align rat.cast_rec Rat.castRec
 

diff --git a/Mathlib/Algebra/Group/ULift.lean b/Mathlib/Algebra/Group/ULift.lean
@@ -127,12 +127,12 @@ instance commSemigroup [CommSemigroup α] : CommSemigroup (ULift α) :=
 
 @[to_additive]
 instance mulOneClass [MulOneClass α] : MulOneClass (ULift α) :=
-  (Equiv.ulift.injective.mulOneClass _ rfl) fun _ _ => rfl
+  Equiv.ulift.injective.mulOneClass _ rfl (by intros; rfl)
 #align ulift.mul_one_class ULift.mulOneClass
 #align ulift.add_zero_class ULift.addZeroClass
 
 instance mulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass (ULift α) :=
-  (Equiv.ulift.injective.mulZeroOneClass _ rfl rfl) fun _ _ => rfl
+  Equiv.ulift.injective.mulZeroOneClass _ rfl rfl (by intros; rfl)
 #align ulift.mul_zero_one_class ULift.mulZeroOneClass
 
 @[to_additive]

diff --git a/Mathlib/Algebra/Hom/Units.lean b/Mathlib/Algebra/Hom/Units.lean
@@ -257,13 +257,13 @@ theorem coe_liftRight (f : M →* N) (hf : ∀ x, IsUnit (f x)) (x) :
 
 @[simp, to_additive]
 theorem mul_liftRight_inv (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
-  f x * ↑(IsUnit.liftRight f h x)⁻¹ = 1 := Units.mul_liftRight_inv (fun _ => rfl) x
+  f x * ↑(IsUnit.liftRight f h x)⁻¹ = 1 := Units.mul_liftRight_inv (by intro; rfl) x
 #align is_unit.mul_lift_right_inv IsUnit.mul_liftRight_inv
 #align is_add_unit.add_lift_right_neg IsAddUnit.add_liftRight_neg
 
 @[simp, to_additive]
 theorem liftRight_inv_mul (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
-  ↑(IsUnit.liftRight f h x)⁻¹ * f x = 1 := Units.liftRight_inv_mul (fun _ => rfl) x
+  ↑(IsUnit.liftRight f h x)⁻¹ * f x = 1 := Units.liftRight_inv_mul (by intro; rfl) x
 #align is_unit.lift_right_inv_mul IsUnit.liftRight_inv_mul
 #align is_add_unit.lift_right_neg_add IsAddUnit.liftRight_neg_add
 

diff --git a/Mathlib/Algebra/Parity.lean b/Mathlib/Algebra/Parity.lean
@@ -342,11 +342,7 @@ theorem odd_two_mul_add_one (m : α) : Odd (2 * m + 1) :=
 
 theorem Odd.map [RingHomClass F α β] (f : F) : Odd m → Odd (f m) := by
   rintro ⟨m, rfl⟩
-  refine ⟨f m, ?_⟩
-  simp [two_mul]
-  rw [← Nat.cast_one, map_add, map_add, Nat.cast_one]
-  apply congrArg
-  rw [map_one]
+  exact ⟨f m, by simp [two_mul]⟩
 #align odd.map Odd.map
 
 @[simp]

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -453,7 +453,7 @@ theorem pow_sub_lt_descFactorial' {n : ℕ} :
     · refine' ((Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ n) _) _).trans_lt _)
       rw [succ_sub_succ]
       exact pow_sub_lt_descFactorial' ((le_succ _).trans h)
-    · apply tsub_pos_of_lt h
+    · apply tsub_pos_of_lt; apply h
 #align nat.pow_sub_lt_descFactorial' Nat.pow_sub_lt_descFactorial'
 
 theorem pow_sub_lt_descFactorial {n : ℕ} :
@@ -477,8 +477,8 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
     rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
-    exact
-      Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ) (pow_pos hn _)
+    exact Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
+      (pow_pos (Nat.lt_of_succ_le hn) _)
 #align nat.descFactorial_lt_pow Nat.descFactorial_lt_pow
 
 end DescFactorial

diff --git a/Mathlib/Init/Align.lean b/Mathlib/Init/Align.lean
@@ -43,9 +43,6 @@ set_option align.precheck false in #align _sorry_placeholder_ _sorry_placeholder
 #align has_coe_to_sort CoeSort
 #align has_coe_to_sort.coe CoeSort.coe
 
-#align coe_trans coeTransₓ
-#align coe_base coeBaseₓ
-
 /-! ## `init.control.alternative` -/
 
 /-! ## `init.control.applicative` -/

diff --git a/Mathlib/Init/Logic.lean b/Mathlib/Init/Logic.lean
@@ -330,11 +330,7 @@ theorem decidable_eq_inr_neg {α : Sort u} [h : DecidableEq α] {a b : α}
 
 #align inhabited.default Inhabited.default
 #align arbitrary Inhabited.default
-
--- see Note [lower instance priority]
-@[simp]
-instance (priority := 100) nonempty_of_inhabited [Inhabited α] : Nonempty α :=
-⟨default⟩
+#align nonempty_of_inhabited instNonempty
 
 /- subsingleton -/
 

diff --git a/Mathlib/Logic/Nontrivial.lean b/Mathlib/Logic/Nontrivial.lean
@@ -86,8 +86,6 @@ instance (priority := 500) Nontrivial.to_nonempty [Nontrivial α] : Nonempty α
   let ⟨x, _⟩ := _root_.exists_pair_ne α
   ⟨x⟩
 
-attribute [instance] nonempty_of_inhabited
-
 /-- An inhabited type is either nontrivial, or has a unique element. -/
 noncomputable def nontrivial_Psum_Unique (α : Type _) [Inhabited α] :
     PSum (Nontrivial α) (Unique α) :=

diff --git a/Mathlib/Order/Antisymmetrization.lean b/Mathlib/Order/Antisymmetrization.lean
@@ -236,7 +236,7 @@ protected def OrderHom.antisymmetrization (f : α →o β) :
 
 @[simp]
 theorem OrderHom.coe_antisymmetrization (f : α →o β) :
-    f.antisymmetrization = Quotient.map' f (lift_fun_antisymmRel f) :=
+    ⇑f.antisymmetrization = Quotient.map' f (lift_fun_antisymmRel f) :=
   rfl
 #align order_hom.coe_antisymmetrization OrderHom.coe_antisymmetrization
 

diff --git a/Mathlib/Order/InitialSeg.lean b/Mathlib/Order/InitialSeg.lean
@@ -244,7 +244,7 @@ infixl:25 " ≺i " => PrincipalSeg
 
 namespace PrincipalSeg
 
-instance : Coe (r ≺i s) (r ↪r s) :=
+instance : CoeOut (r ≺i s) (r ↪r s) :=
   ⟨PrincipalSeg.toRelEmbedding⟩
 
 instance : CoeFun (r ≺i s) fun _ => α → β :=

diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
@@ -558,7 +558,7 @@ theorem toEquiv_injective : Injective (toEquiv : r ≃r s → α ≃ β)
     congr
 #align rel_iso.to_equiv_injective RelIso.toEquiv_injective
 
-instance : Coe (r ≃r s) (r ↪r s) :=
+instance : CoeOut (r ≃r s) (r ↪r s) :=
   ⟨toRelEmbedding⟩
 
 -- see Note [function coercion]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -32,9 +32,9 @@
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/gebner/aesop",
     "subDir?": null,
-    "rev": "87a654a5a10f5edf3cfaee9052c08a4342b24179",
+    "rev": "6f04ed73886f455a8ec41fbbae21ef6b870c61ff",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
@@ -52,6 +52,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "788ffeee98ac3ef98dd5d54ede953d8194af0593",
+    "rev": "2ace3a9803a96fd765d588b2a95fb6fafaf05bb3",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-12-16
+leanprover/lean4:nightly-2022-12-22