chore: adaptations for nightly-2025-01-29 (#21245)

* chore: bump to nightly-2025-01-09 * bump batteries * bump deps * fix * chore: adaptations for nightly-2025-01-09 * chore: bump to nightly-2025-01-10 * remove upstreamed * Update lean-toolchain for testing leanprover/lean4#6602 * Trigger CI for leanprover/lean4#6602 * fix breakage caused by leanprover/lean4#6602 * chore: adaptations for nightly-2025-01-10 * fix merge * avoid nonrec for leanprover/lean4#6602 * Trigger CI for leanprover/lean4#6602 * chore: bump to nightly-2025-01-14 * bump * fixes * fixes * fixes * chore: bump to nightly-2025-01-15 * fix * empty commit to bump CI * Update lean-toolchain for testing leanprover/lean4#6660 * fixes for leanprover/lean4#6660 * chore: bump to nightly-2025-01-16 * . * fix * chore: bump to nightly-2025-01-17 * deprecation * chore: bump to nightly-2025-01-18 * Merge master into nightly-testing * chore: bump to nightly-2025-01-19 * fix * chore: bump to nightly-2025-01-20 * fix and bump * bump ProofWidgets * chore: bump to nightly-2025-01-21 * bump * Adaptations * fixes * fix * fix * chore: bump to nightly-2025-01-22 * chore: adaptations for nightly-2025-01-22 * remove deprecation for List.indexOf_lt_length * chore: bump to nightly-2025-01-23 * chore: bump to nightly-2025-01-24 * Adjust expected output in MathlibTest.CountHeartbeats * chore: adaptations for nightly-2025-01-24 * chore: bump to nightly-2025-01-25 * chore: bump to nightly-2025-01-26 * chore: bump to nightly-2025-01-27 * Merge master into nightly-testing * Adaption for leanprover/lean4#6755 * Update lean-toolchain for testing leanprover/lean4#6800 * lake update for leanprover/lean4#6800 * Trigger CI for leanprover/lean4#6800 * fixes for leanprover/lean4#6800 * Trigger CI for leanprover/lean4#6800 * fix * Update lean-toolchain for testing leanprover/lean4#6812 * chore: bump to nightly-2025-01-28 * lake update for leanprover/lean4#6812 * TrivSqZeroExt.snd_list_prod fix * Update lean-toolchain for testing leanprover/lean4#6826 * Adaption * fix * fix * remove deprecation/alias * touch for CI for leanprover/lean4#6812 * fix for leanprover/lean4#6812 * Trigger CI for leanprover/lean4#6826 * chore: bump to nightly-2025-01-29 * . * merge lean-pr-testing-6812 * . * lake update * lake update * fixes and deprecations * name clash * fix * fix * update * lint * shake --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Parth Shastri <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Yakov Pechersky <[email protected]> Co-authored-by: Ruben Van de Velde <[email protected]>
leanprover-community · Jan 30, 2025 · c729276 · c729276
1 parent 23c468c
commit c729276
Show file tree

Hide file tree

Showing 28 changed files with 102 additions and 142 deletions.
diff --git a/Mathlib/Algebra/LinearRecurrence.lean b/Mathlib/Algebra/LinearRecurrence.lean
@@ -92,7 +92,8 @@ theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : Fin E.order → α}
   rw [mkSol]
   split_ifs with h'
   · exact mod_cast heq ⟨n, h'⟩
-  · rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
+  · dsimp only
+    rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
     congr with k
     have : n - E.order + k < n := by omega
     rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]

diff --git a/Mathlib/Algebra/TrivSqZeroExt.lean b/Mathlib/Algebra/TrivSqZeroExt.lean
@@ -658,12 +658,12 @@ $r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$. -/
 theorem snd_list_prod [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
     [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) :
     l.prod.snd =
-      (l.enum.map fun x : ℕ × tsze R M =>
-          ((l.map fst).take x.1).prod •> x.snd.snd <• ((l.map fst).drop x.1.succ).prod).sum := by
+      (l.zipIdx.map fun x : tsze R M × ℕ =>
+          ((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum := by
   induction l with
   | nil => simp
   | cons x xs ih =>
-    rw [List.enum_cons, ← List.map_fst_add_enum_eq_enumFrom]
+    rw [List.zipIdx_cons']
     simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
       List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
       List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,

diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
@@ -550,7 +550,7 @@ def compChangeOfVariables (m M N : ℕ) (i : Σ n, Fin n → ℕ) (hi : i ∈ co
   rw [mem_compPartialSumSource_iff] at hi
   refine ⟨∑ j, f j, ofFn fun a => f a, fun hi' => ?_, by simp [sum_ofFn]⟩
   rename_i i
-  obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn, Set.mem_range] at hi'
+  obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi'
   exact (hi.2 j).1
 
 @[simp]

diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean
@@ -478,7 +478,7 @@ theorem eq_ones_iff_length {c : Composition n} : c = ones n ↔ c.length = n :=
       _ < ∑ i : Fin c.length, c.blocksFun i := by
         {
         obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
-        rw [← ofFn_blocksFun, mem_ofFn c.blocksFun, Set.mem_range] at hi
+        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
         obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
         rw [← hj] at i_blocks
         exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -29,10 +29,6 @@ open Nat hiding one_pos
 
 namespace List
 
--- Renamed in lean core; to be removed with the version bump.
-alias replicate_append_replicate := append_replicate_replicate
-alias append_eq_nil_iff := append_eq_nil
-
 universe u v w
 
 variable {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {l₁ l₂ : List α}
@@ -694,9 +690,6 @@ theorem indexOf_eq_length_iff {a : α} {l : List α} : indexOf a l = length l
     rw [← ih]
     exact succ_inj'
 
-@[deprecated (since := "2025-01-28")]
-alias indexOf_eq_length := indexOf_eq_length_iff
-
 @[simp]
 theorem indexOf_of_not_mem {l : List α} {a : α} : a ∉ l → indexOf a l = length l :=
   indexOf_eq_length_iff.2

diff --git a/Mathlib/Data/List/Enum.lean b/Mathlib/Data/List/Enum.lean
@@ -21,62 +21,31 @@ namespace List
 
 variable {α : Type*}
 
-@[deprecated getElem?_enumFrom (since := "2024-08-15")]
-theorem get?_enumFrom (n) (l : List α) (m) :
-    get? (enumFrom n l) m = (get? l m).map fun a => (n + m, a) := by
-  simp
-
-@[deprecated (since := "2024-04-06")] alias enumFrom_get? := get?_enumFrom
-
-@[deprecated getElem?_enum (since := "2024-08-15")]
-theorem get?_enum (l : List α) (n) : get? (enum l) n = (get? l n).map fun a => (n, a) := by
-  simp
-
-@[deprecated (since := "2024-04-06")] alias enum_get? := get?_enum
-
-@[deprecated getElem_enumFrom (since := "2024-08-15")]
-theorem get_enumFrom (l : List α) (n) (i : Fin (l.enumFrom n).length) :
-    (l.enumFrom n).get i = (n + i, l.get (i.cast enumFrom_length)) := by
-  simp
-
-@[deprecated getElem_enum (since := "2024-08-15")]
-theorem get_enum (l : List α) (i : Fin l.enum.length) :
-    l.enum.get i = (i.1, l.get (i.cast enum_length)) := by
-  simp
-
-@[deprecated mk_add_mem_enumFrom_iff_getElem? (since := "2024-08-12")]
-theorem mk_add_mem_enumFrom_iff_get? {n i : ℕ} {x : α} {l : List α} :
-    (n + i, x) ∈ enumFrom n l ↔ l.get? i = x := by
-  simp [mem_iff_get?]
-
-@[deprecated mk_mem_enumFrom_iff_le_and_getElem?_sub (since := "2024-08-12")]
-theorem mk_mem_enumFrom_iff_le_and_get?_sub {n i : ℕ} {x : α} {l : List α} :
-    (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = x := by
-  simp [mk_mem_enumFrom_iff_le_and_getElem?_sub]
-
-@[deprecated mk_mem_enum_iff_getElem? (since := "2024-08-15")]
-theorem mk_mem_enum_iff_get? {i : ℕ} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l.get? i = x := by
-  simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]
-
-set_option linter.deprecated false in
-@[deprecated mem_enum_iff_getElem? (since := "2024-08-15")]
-theorem mem_enum_iff_get? {x : ℕ × α} {l : List α} : x ∈ enum l ↔ l.get? x.1 = x.2 :=
-  mk_mem_enum_iff_get?
-
-theorem forall_mem_enumFrom {l : List α} {n : ℕ} {p : ℕ × α → Prop} :
-    (∀ x ∈ l.enumFrom n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (n + i, l[i]) := by
-  simp only [forall_mem_iff_getElem, getElem_enumFrom, enumFrom_length]
-
-theorem forall_mem_enum {l : List α} {p : ℕ × α → Prop} :
-    (∀ x ∈ l.enum, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (i, l[i]) :=
-  forall_mem_enumFrom.trans <| by simp
-
-theorem exists_mem_enumFrom {l : List α} {n : ℕ} {p : ℕ × α → Prop} :
-    (∃ x ∈ l.enumFrom n, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (n + i, l[i]) := by
-  simp only [exists_mem_iff_getElem, getElem_enumFrom, enumFrom_length]
-
-theorem exists_mem_enum {l : List α} {p : ℕ × α → Prop} :
-    (∃ x ∈ l.enum, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (i, l[i]) :=
-  exists_mem_enumFrom.trans <| by simp
+theorem forall_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} :
+    (∀ x ∈ l.zipIdx n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], n + i) := by
+  simp only [forall_mem_iff_getElem, getElem_zipIdx, length_zipIdx]
+
+/-- Variant of `forall_mem_zipIdx` with the `zipIdx` argument specialized to `0`. -/
+theorem forall_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} :
+    (∀ x ∈ l.zipIdx, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], i) :=
+  forall_mem_zipIdx.trans <| by simp
+
+theorem exists_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} :
+    (∃ x ∈ l.zipIdx n, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (l[i], n + i) := by
+  simp only [exists_mem_iff_getElem, getElem_zipIdx, length_zipIdx]
+
+/-- Variant of `exists_mem_zipIdx` with the `zipIdx` argument specialized to `0`. -/
+theorem exists_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} :
+    (∃ x ∈ l.zipIdx, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (l[i], i) :=
+  exists_mem_zipIdx.trans <| by simp
+
+@[deprecated (since := "2025-01-28")]
+alias forall_mem_enumFrom := forall_mem_zipIdx
+@[deprecated (since := "2025-01-28")]
+alias forall_mem_enum := forall_mem_zipIdx'
+@[deprecated (since := "2025-01-28")]
+alias exists_mem_enumFrom := exists_mem_zipIdx
+@[deprecated (since := "2025-01-28")]
+alias exists_mem_enum := exists_mem_zipIdx'
 
 end List
diff --git a/Mathlib/Data/List/Indexes.lean b/Mathlib/Data/List/Indexes.lean
@@ -42,6 +42,7 @@ theorem mapIdx_append_one : ∀ {f : ℕ → α → β} {l : List α} {e : α},
     mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] :=
   mapIdx_concat
 
+set_option linter.deprecated false in
 @[deprecated "Deprecated without replacement." (since := "2025-01-29"), local simp]
 theorem map_enumFrom_eq_zipWith : ∀ (l : List α) (n : ℕ) (f : ℕ → α → β),
     map (uncurry f) (enumFrom n l) = zipWith (fun i ↦ f (i + n)) (range (length l)) l := by
@@ -68,11 +69,12 @@ theorem map_enumFrom_eq_zipWith : ∀ (l : List α) (n : ℕ) (f : ℕ → α
 
 @[deprecated (since := "2024-10-15")] alias mapIdx_eq_nil := mapIdx_eq_nil_iff
 
+set_option linter.deprecated false in
 @[deprecated "Deprecated without replacement." (since := "2025-01-29")]
 theorem get_mapIdx (l : List α) (f : ℕ → α → β) (i : ℕ) (h : i < l.length)
     (h' : i < (l.mapIdx f).length := h.trans_le length_mapIdx.ge) :
     (l.mapIdx f).get ⟨i, h'⟩ = f i (l.get ⟨i, h⟩) := by
-  simp [mapIdx_eq_enum_map, enum_eq_zip_range]
+  simp [mapIdx_eq_zipIdx_map, enum_eq_zip_range]
 
 @[deprecated (since := "2024-08-19")] alias nthLe_mapIdx := get_mapIdx
 
@@ -160,6 +162,7 @@ end MapIdx
 section FoldrIdx
 
 -- Porting note: Changed argument order of `foldrIdxSpec` to align better with `foldrIdx`.
+set_option linter.deprecated false in
 /-- Specification of `foldrIdx`. -/
 @[deprecated "Deprecated without replacement." (since := "2025-01-29")]
 def foldrIdxSpec (f : ℕ → α → β → β) (b : β) (as : List α) (start : ℕ) : β :=
@@ -205,6 +208,7 @@ theorem findIdxs_eq_map_indexesValues (p : α → Prop) [DecidablePred p] (as :
 section FoldlIdx
 
 -- Porting note: Changed argument order of `foldlIdxSpec` to align better with `foldlIdx`.
+set_option linter.deprecated false in
 /-- Specification of `foldlIdx`. -/
 @[deprecated "Deprecated without replacement." (since := "2025-01-29")]
 def foldlIdxSpec (f : ℕ → α → β → α) (a : α) (bs : List β) (start : ℕ) : α :=
@@ -257,6 +261,7 @@ section MapIdxM
 -- Porting note: `[Applicative m]` replaced by `[Monad m] [LawfulMonad m]`
 variable {m : Type u → Type v} [Monad m]
 
+set_option linter.deprecated false in
 /-- Specification of `mapIdxMAux`. -/
 @[deprecated "Deprecated without replacement." (since := "2025-01-29")]
 def mapIdxMAuxSpec {β} (f : ℕ → α → m β) (start : ℕ) (as : List α) : m (List β) :=

diff --git a/Mathlib/Data/List/OfFn.lean b/Mathlib/Data/List/OfFn.lean
@@ -127,15 +127,14 @@ theorem ofFn_getElem_eq_map {β : Type*} (l : List α) (f : α → β) :
 theorem ofFn_get_eq_map {β : Type*} (l : List α) (f : α → β) : ofFn (f <| l.get ·) = l.map f := by
   simp
 
--- not registered as a simp lemma, as otherwise it fires before `forall_mem_ofFn_iff` which
--- is much more useful
-theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f := by
+-- Note there is a now another `mem_ofFn` defined in Lean, with an existential on the RHS,
+-- which is marked as a simp lemma.
+theorem mem_ofFn' {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f := by
   simp only [mem_iff_get, Set.mem_range, get_ofFn]
   exact ⟨fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩⟩
 
-@[simp]
 theorem forall_mem_ofFn_iff {n : ℕ} {f : Fin n → α} {P : α → Prop} :
-    (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j) := by simp only [mem_ofFn, Set.forall_mem_range]
+    (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j) := by simp
 
 @[simp]
 theorem ofFn_const : ∀ (n : ℕ) (c : α), (ofFn fun _ : Fin n => c) = replicate n c

diff --git a/Mathlib/Data/List/ProdSigma.lean b/Mathlib/Data/List/ProdSigma.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Data.List.Basic
 import Mathlib.Data.Prod.Basic
-import Mathlib.Data.Sigma.Basic
 
 /-!
 # Lists in product and sigma types

diff --git a/Mathlib/Data/List/Sigma.lean b/Mathlib/Data/List/Sigma.lean
@@ -128,7 +128,10 @@ theorem nodupKeys_flatten {L : List (List (Sigma β))} :
 
 @[deprecated (since := "2024-10-15")] alias nodupKeys_join := nodupKeys_flatten
 
-theorem nodup_enum_map_fst (l : List α) : (l.enum.map Prod.fst).Nodup := by simp [List.nodup_range]
+theorem nodup_zipIdx_map_snd (l : List α) : (l.zipIdx.map Prod.snd).Nodup := by
+  simp [List.nodup_range']
+
+@[deprecated (since := "2025-01-28")] alias nodup_enum_map_fst := nodup_zipIdx_map_snd
 
 theorem mem_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.Nodup) (nd₁ : l₁.Nodup)
     (h : ∀ x, x ∈ l₀ ↔ x ∈ l₁) : l₀ ~ l₁ :=

diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean
@@ -367,9 +367,9 @@ theorem revzip_sublists (l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l
   rw [revzip]
   induction' l using List.reverseRecOn with l' a ih
   · intro l₁ l₂ h
-    simp? at h says
+    simp?  at h says
       simp only [sublists_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons, zip_nil_right,
-        mem_singleton, Prod.mk.injEq] at h
+        mem_cons, Prod.mk.injEq, not_mem_nil, or_false] at h
     simp [h]
   · intro l₁ l₂ h
     rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,

diff --git a/Mathlib/Data/List/ToFinsupp.lean b/Mathlib/Data/List/ToFinsupp.lean
@@ -125,15 +125,18 @@ theorem toFinsupp_concat_eq_toFinsupp_add_single {R : Type*} [AddZeroClass R] (x
     addLeftEmbedding_apply, add_zero]
 
 
-theorem toFinsupp_eq_sum_map_enum_single {R : Type*} [AddMonoid R] (l : List R)
+theorem toFinsupp_eq_sum_mapIdx_single {R : Type*} [AddMonoid R] (l : List R)
     [DecidablePred (getD l · 0 ≠ 0)] :
-    toFinsupp l = (l.enum.map fun nr : ℕ × R => Finsupp.single nr.1 nr.2).sum := by
+    toFinsupp l = (l.mapIdx fun n r => Finsupp.single n r).sum := by
   /- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: `induction` fails to substitute `l = []` in
   `[DecidablePred (getD l · 0 ≠ 0)]`, so we manually do some `revert`/`intro` as a workaround -/
   revert l; intro l
   induction l using List.reverseRecOn with
   | nil => exact toFinsupp_nil
   | append_singleton x xs ih =>
-    classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
+    classical simp [toFinsupp_concat_eq_toFinsupp_add_single, ih]
+
+@[deprecated (since := "2025-01-28")]
+alias toFinsupp_eq_sum_map_enum_single := toFinsupp_eq_sum_mapIdx_single
 
 end List
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
@@ -150,22 +150,22 @@ theorem ofDigits_eq_foldr {α : Type*} [Semiring α] (b : α) (L : List ℕ) :
   · dsimp [ofDigits]
     rw [ih]
 
-theorem ofDigits_eq_sum_map_with_index_aux (b : ℕ) (l : List ℕ) :
-    ((List.range l.length).zipWith ((fun i a : ℕ => a * b ^ (i + 1))) l).sum =
-      b * ((List.range l.length).zipWith (fun i a => a * b ^ i) l).sum := by
+theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) :
+    (l.zipWith ((fun a i : ℕ => a * b ^ (i + 1))) (List.range l.length)).sum =
+      b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum := by
   suffices
-    (List.range l.length).zipWith (fun i a : ℕ => a * b ^ (i + 1)) l =
-      (List.range l.length).zipWith (fun i a => b * (a * b ^ i)) l
+    l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
+      l.zipWith (fun a i=> b * (a * b ^ i)) (List.range l.length)
     by simp [this]
   congr; ext; simp [pow_succ]; ring
 
 theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) :
     ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum := by
-  rw [List.mapIdx_eq_enum_map, List.enum_eq_zip_range, List.map_uncurry_zip_eq_zipWith,
-    ofDigits_eq_foldr]
+  rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith,
+    ofDigits_eq_foldr, ← List.range_eq_range']
   induction' L with hd tl hl
   · simp
-  · simpa [List.range_succ_eq_map, List.zipWith_map_left, ofDigits_eq_sum_map_with_index_aux] using
+  · simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using
       Or.inl hl
 
 @[simp]

diff --git a/Mathlib/Data/Sigma/Basic.lean b/Mathlib/Data/Sigma/Basic.lean
@@ -50,12 +50,8 @@ instance instDecidableEqSigma [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq
       | _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂
     | _, _, _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun e₁ _ ↦ n e₁
 
--- sometimes the built-in injectivity support does not work
-@[simp]
 theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
-    Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂ :=
-  ⟨fun h ↦ by cases h; simp,
-   fun ⟨h₁, h₂⟩ ↦ by subst h₁; rw [eq_of_heq h₂]⟩
+    Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂ := by simp
 
 @[simp]
 theorem eta : ∀ x : Σa, β a, Sigma.mk x.1 x.2 = x
@@ -227,11 +223,6 @@ instance decidableEq [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)]
       | _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂
     | _, _, _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun e₁ _ ↦ n e₁
 
--- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/porting.20data.2Esigma.2Ebasic/near/304855864
--- for an explanation of why this is currently needed. It generates `PSigma.mk.inj`.
--- This could be done elsewhere.
-gen_injective_theorems% PSigma
-
 theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
     @PSigma.mk α β a₁ b₁ = @PSigma.mk α β a₂ b₂ ↔ a₁ = a₂ ∧ HEq b₁ b₂ :=
   (Iff.intro PSigma.mk.inj) fun ⟨h₁, h₂⟩ ↦

diff --git a/Mathlib/Data/ULift.lean b/Mathlib/Data/ULift.lean
@@ -46,9 +46,7 @@ theorem up_surjective : Surjective (@up α) :=
 theorem up_bijective : Bijective (@up α) :=
   Equiv.plift.symm.bijective
 
-@[simp]
-theorem up_inj {x y : α} : up x = up y ↔ x = y :=
-  up_injective.eq_iff
+theorem up_inj {x y : α} : up x = up y ↔ x = y := by simp
 
 theorem down_surjective : Surjective (@down α) :=
   Equiv.plift.surjective
@@ -103,9 +101,7 @@ theorem up_surjective : Surjective (@up α) :=
 theorem up_bijective : Bijective (@up α) :=
   Equiv.ulift.symm.bijective
 
-@[simp]
-theorem up_inj {x y : α} : up x = up y ↔ x = y :=
-  up_injective.eq_iff
+theorem up_inj {x y : α} : up x = up y ↔ x = y := by simp
 
 theorem down_surjective : Surjective (@down α) :=
   Equiv.ulift.surjective