chore: bump lean 01-29 (#1927)

Mathlib/Algebra/Group/Semiconj.lean

@@ -120,6 +120,7 @@ variable [Monoid M]
 @[to_additive "If `a` semiconjugates an additive unit `x` to an additive unit `y`, then it
 semiconjugates `-x` to `-y`."]
 theorem units_inv_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹ :=
+  show _ = _ from -- lean4#2073
   calc
     a * ↑x⁻¹ = ↑y⁻¹ * (y * a) * ↑x⁻¹ := by rw [Units.inv_mul_cancel_left]
     _        = ↑y⁻¹ * a              := by rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
@@ -136,6 +137,7 @@ theorem units_inv_right_iff {a : M} {x y : Mˣ} : SemiconjBy a ↑x⁻¹ ↑y⁻
 @[to_additive "If an additive unit `a` semiconjugates `x` to `y`, then `-a` semiconjugates `y` to
 `x`."]
 theorem units_inv_symm_left {a : Mˣ} {x y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x :=
+  show _ = _ from -- lean4#2073
   calc
     ↑a⁻¹ * y = ↑a⁻¹ * (y * a * ↑a⁻¹) := by rw [Units.mul_inv_cancel_right]
     _ = x * ↑a⁻¹ := by rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]

Mathlib/Algebra/Invertible.lean

@@ -283,6 +283,7 @@ theorem mul_right_eq_iff_eq_mul_invOf [Monoid α] [Invertible (c : α)] :
 
 theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a b) :
     Commute a (⅟ b) :=
+  show _ = _ from -- lean4#2073
   calc
     a * ⅟ b = ⅟ b * (b * a * ⅟ b) := by simp [mul_assoc]
     _ = ⅟ b * (a * b * ⅟ b) := by rw [h.eq]
@@ -292,6 +293,7 @@ theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a
 
 theorem Commute.invOf_left [Monoid α] {a b : α} [Invertible b] (h : Commute b a) :
     Commute (⅟ b) a :=
+  show _ = _ from -- lean4#2073
   calc
     ⅟ b * a = ⅟ b * (a * b * ⅟ b) := by simp [mul_assoc]
     _ = ⅟ b * (b * a * ⅟ b) := by rw [h.eq]
@@ -300,6 +302,7 @@ theorem Commute.invOf_left [Monoid α] {a b : α} [Invertible b] (h : Commute b
 #align commute.inv_of_left Commute.invOf_left
 
 theorem commute_invOf {M : Type _} [One M] [Mul M] (m : M) [Invertible m] : Commute m (⅟ m) :=
+  show _ = _ from -- lean4#2073
   calc
     m * ⅟ m = 1 := mul_invOf_self m
     _ = ⅟ m * m := (invOf_mul_self m).symm

Mathlib/Data/Nat/Order/Basic.lean

@@ -177,6 +177,7 @@ theorem lt_one_iff {n : ℕ} : n < 1 ↔ n = 0 :=
 
 
 theorem add_pos_left {m : ℕ} (h : 0 < m) (n : ℕ) : 0 < m + n :=
+  show _ > _ from -- lean4#2073
   calc
     m + n > 0 + n := Nat.add_lt_add_right h n
     _ = n := Nat.zero_add n

Mathlib/Data/Set/Intervals/OrdConnectedComponent.lean

@@ -90,6 +90,7 @@ theorem mem_ordConnectedComponent_comm :
 
 theorem mem_ordConnectedComponent_trans (hxy : y ∈ ordConnectedComponent s x)
     (hyz : z ∈ ordConnectedComponent s y) : z ∈ ordConnectedComponent s x :=
+  show _ ⊆ _ from -- lean4#2073
   calc
     [[x, z]] ⊆ [[x, y]] ∪ [[y, z]] := uIcc_subset_uIcc_union_uIcc
     _ ⊆ s := union_subset hxy hyz

Mathlib/Data/ZMod/Defs.lean

@@ -49,22 +49,22 @@ open Nat.ModEq Int
 instance (n : ℕ) : CommSemigroup (Fin n) :=
   { inferInstanceAs (Mul (Fin n)) with
     mul_assoc := fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ =>
-      Fin.eq_of_veq
-        (calc
+      Fin.eq_of_veq <|
+        show _ ≡ _ [MOD _] from -- lean4#2073
+        calc
           a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
           _ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
           _ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
-          )
     mul_comm := Fin.mul_comm }
 
 private theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a * b + a * c :=
   fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ =>
-  Fin.eq_of_veq
-    (calc
+  Fin.eq_of_veq <|
+    show _ ≡ _ [MOD _] from -- lean4#2073
+    calc
       a * ((b + c) % n) ≡ a * (b + c) [MOD n] := (Nat.mod_modEq _ _).mul_left _
       _ ≡ a * b + a * c [MOD n] := by rw [mul_add]
       _ ≡ a * b % n + a * c % n [MOD n] := (Nat.mod_modEq _ _).symm.add (Nat.mod_modEq _ _).symm
-      )
 
 /-- Commutative ring structure on `Fin n`. -/
 instance (n : ℕ) [NeZero n] : CommRing (Fin n) :=

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -58,6 +58,7 @@ protected theorem eq (hf : IsFixedPt f x) : f x = x :=
 
 /-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`. -/
 protected theorem comp (hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x :=
+  show _ = _ from -- lean4#2073
   calc
     f (g x) = f x := congr_arg f hg
     _ = x := hf
@@ -71,6 +72,7 @@ protected theorem iterate (hf : IsFixedPt f x) (n : ℕ) : IsFixedPt (f^[n]) x :
 
 /-- If `x` is a fixed point of `f ∘ g` and `g`, then it is a fixed point of `f`. -/
 theorem left_of_comp (hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixedPt f x :=
+  show _ = _ from -- lean4#2073
   calc
     f x = f (g x) := congr_arg f hg.symm
     _ = x := hfg
@@ -80,6 +82,7 @@ theorem left_of_comp (hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixe
 /-- If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed
 point of `g`. -/
 theorem to_leftInverse (hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g x :=
+  show _ = _ from -- lean4#2073
   calc
     g x = g (f x) := congr_arg g hf.symm
     _ = x := h x
@@ -90,6 +93,7 @@ theorem to_leftInverse (hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g
 of `fb`. -/
 protected theorem map {x : α} (hx : IsFixedPt fa x) {g : α → β} (h : Semiconj g fa fb) :
     IsFixedPt fb (g x) :=
+  show _ = _ from -- lean4#2073
   calc
     fb (g x) = g (fa x) := (h.eq x).symm
     _ = g x := congr_arg g hx

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -2777,6 +2777,7 @@ variable {M : Type _} [MulOneClass M]
 def ker (f : G →* M) : Subgroup G :=
   { MonoidHom.mker f with
     inv_mem' := fun {x} (hx : f x = 1) =>
+      show _ = _ from -- lean4#2073
       calc
         f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
         _ = 1 := by rw [← map_mul, mul_inv_self, map_one] }

Mathlib/Logic/Denumerable.lean

@@ -256,13 +256,15 @@ theorem le_succ_of_forall_lt_le {x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ
   show (x : ℕ) ≤ (y : ℕ) + Nat.find hx + 1 from
     le_of_not_gt fun hxy =>
       (h ⟨_, Nat.find_spec hx⟩ hxy).not_lt <|
+        show _ < _ from -- lean4#2073
         calc
           (y : ℕ) ≤ (y : ℕ) + Nat.find hx := le_add_of_nonneg_right (Nat.zero_le _)
           _ < (y : ℕ) + Nat.find hx + 1 := Nat.lt_succ_self _
 
 #align nat.subtype.le_succ_of_forall_lt_le Nat.Subtype.le_succ_of_forall_lt_le
 
-theorem lt_succ_self (x : s) : x < succ x := by
+theorem lt_succ_self (x : s) : x < succ x :=
+  show _ < _ from -- lean4#2073
   calc
     -- Porting note: replaced `x + _`, added type annotations
     (x : ℕ) ≤ (x + Nat.find (exists_succ x): ℕ) := le_self_add

Mathlib/Logic/Equiv/Basic.lean

@@ -1209,6 +1209,7 @@ def sigmaSubtypeEquivOfSubset (p : α → Type v) (q : α → Prop) (h : ∀ x,
 `Σ y : {y // p y}, {x // f x = y}` is equivalent to `α`. -/
 def sigmaSubtypeFiberEquiv {α β : Type _} (f : α → β) (p : β → Prop) (h : ∀ x, p (f x)) :
     (Σ y : Subtype p, { x : α // f x = y }) ≃ α :=
+  show _ ≃ _ from -- lean4#2073
   calc
     _ ≃ Σy : β, { x : α // f x = y } := sigmaSubtypeEquivOfSubset _ p fun _ ⟨x, h'⟩ => h' ▸ h x
     _ ≃ α := sigmaFiberEquiv f

Mathlib/Logic/Equiv/Fin.lean

@@ -117,7 +117,7 @@ def finCongr (h : m = n) : Fin m ≃ Fin n :=
   rfl
 #align fin_congr_symm finCongr_symm
 
-@[simp] theorem finCongr_apply_coe (h : m = n) (k : Fin m) : (finCongr h k : ℕ) = k := 
+@[simp] theorem finCongr_apply_coe (h : m = n) (k : Fin m) : (finCongr h k : ℕ) = k :=
   rfl
 #align fin_congr_apply_coe finCongr_apply_coe
 
@@ -465,6 +465,7 @@ def finProdFinEquiv : Fin m × Fin n ≃ Fin (m * n)
     where
   toFun x :=
     ⟨x.2 + n * x.1,
+      show _ ≤ _ from -- lean4#2073
       calc
         x.2.1 + n * x.1.1 + 1 = x.1.1 * n + x.2.1 + 1 := by ac_rfl
         _ ≤ x.1.1 * n + n := Nat.add_le_add_left x.2.2 _

lake-manifest.json

@@ -1,31 +1,7 @@
 {"version": 4,
- "packagesDir": "./lake-packages",
+ "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/xubaiw/CMark.lean",
-    "subDir?": null,
-    "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8",
-    "name": "CMark",
-    "inputRev?": "main"}},
-  {"git":
-   {"url": "https://github.com/leanprover/lake",
-    "subDir?": null,
-    "rev": "d0b530530f14dde97a547b03abf87eee06360d60",
-    "name": "lake",
-    "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/leanprover/doc-gen4",
-    "subDir?": null,
-    "rev": "09dbebed9ca85368152bb5146ef6f1271b1be425",
-    "name": "doc-gen4",
-    "inputRev?": "main"}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli",
-    "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
-    "name": "Cli",
-    "inputRev?": "nightly"}},
-  {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
     "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
@@ -34,24 +10,12 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "645e92db52499582bb31984396a5e41772241012",
+    "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea",
     "name": "aesop",
     "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/hargonix/LeanInk",
-    "subDir?": null,
-    "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
-    "name": "leanInk",
-    "inputRev?": "doc-gen"}},
-  {"git":
-   {"url": "https://github.com/xubaiw/Unicode.lean",
-    "subDir?": null,
-    "rev": "6dd6ae3a3839c8350a91876b090eda85cf538d1d",
-    "name": "Unicode",
-    "inputRev?": "main"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "7977f08b1c427b4e8070ba4cc1f599617ebda867",
+    "rev": "cda27d551340756d5ed6f9b83716a9db799c5537",
     "name": "std",
     "inputRev?": "main"}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-01-16
+leanprover/lean4:nightly-2023-01-29