chore: further backports for leanprover/lean4#6397 (#20098)

Co-authored-by: Johan Commelin <johan@commelin.net>

Author: kim-em

Mathlib/Algebra/FreeMonoid/Count.lean

@@ -14,6 +14,15 @@ In this file we define `FreeMonoid.countP`, `FreeMonoid.count`, `FreeAddMonoid.c
 additive homomorphisms from `FreeMonoid` and `FreeAddMonoid`.
 
 We do not use `to_additive` because it can't map `Multiplicative ℕ` to `ℕ`.
+
+## TODO
+
+There is lots of defeq abuse here of `FreeAddMonoid α = List α`, e.g. in statements like
+```
+theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl
+```
+This needs cleaning up.
+
 -/
 
 variable {α : Type*} (p : α → Prop) [DecidablePred p]
@@ -27,7 +36,8 @@ def countP : FreeAddMonoid α →+ ℕ where
   map_add' := List.countP_append _
 
 theorem countP_of (x : α) : countP p (of x) = if p x = true then 1 else 0 := by
-  simp [countP, List.countP, List.countP.go]
+  change List.countP p [x] = _
+  simp [List.countP_cons]
 
 theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl
 
@@ -36,8 +46,8 @@ theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rf
 def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countP (· = x)
 
 theorem count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y := by
-  simp [Pi.single, Function.update, count, countP, List.countP, List.countP.go,
-    Bool.beq_eq_decide_eq]
+  change List.count x [y] = _
+  simp [Pi.single, Function.update, List.count_cons]
 
 theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) : count x l = List.count x l :=
   rfl

Mathlib/Algebra/Group/Defs.lean

@@ -451,7 +451,7 @@ theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
     match k' with
     | 0 => rfl
     | 1 => simp [npowRec']
-    | k + 2 => simp [npowRec', ← mul_assoc, ← ih]
+    | k + 2 => simp [npowRec', ← mul_assoc, Nat.mul_add, ← ih]
 
 @[to_additive]
 theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :

Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

@@ -361,7 +361,7 @@ lemma Real.Gamma_nat_add_one_add_half (k : ℕ) :
   induction k with
   | zero => simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]; ring
   | succ k ih =>
-    rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih]
+    rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
     field_simp
     ring
 

Mathlib/CategoryTheory/Functor/OfSequence.lean

@@ -81,7 +81,7 @@ lemma map_comp (i j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) :
           · omega
           · obtain rfl : j = 0 := by omega
             rw [map_id, comp_id]
-          · dsimp [map]
+          · simp only [map, Nat.reduceAdd]
             rw [hj (fun n ↦ f (n + 1)) (k + 1) (by omega) (by omega)]
             obtain _|j := j
             all_goals simp [map]

Mathlib/Combinatorics/Quiver/SingleObj.lean

@@ -113,7 +113,7 @@ theorem listToPath_pathToList {x : SingleObj α} (p : Path (star α) x) :
     listToPath (pathToList p) = p.cast rfl ext := by
   induction p with
   | nil => rfl
-  | cons _ _ ih => dsimp at *; rw [ih]
+  | cons _ _ ih => dsimp [pathToList] at *; rw [ih]
 
 theorem pathToList_listToPath (l : List α) : pathToList (listToPath l) = l := by
   induction l with

Mathlib/Computability/PartrecCode.lean

@@ -495,10 +495,10 @@ theorem eval_const : ∀ n m, eval (Code.const n) m = Part.some n
   | n + 1, m => by simp! [eval_const n m]
 
 @[simp]
-theorem eval_id (n) : eval Code.id n = Part.some n := by simp! [Seq.seq]
+theorem eval_id (n) : eval Code.id n = Part.some n := by simp! [Seq.seq, Code.id]
 
 @[simp]
-theorem eval_curry (c n x) : eval (curry c n) x = eval c (Nat.pair n x) := by simp! [Seq.seq]
+theorem eval_curry (c n x) : eval (curry c n) x = eval c (Nat.pair n x) := by simp! [Seq.seq, curry]
 
 theorem const_prim : Primrec Code.const :=
   (_root_.Primrec.id.nat_iterate (_root_.Primrec.const zero)

Mathlib/Computability/RegularExpressions.lean

@@ -364,7 +364,7 @@ def map (f : α → β) : RegularExpression α → RegularExpression β
 @[simp]
 protected theorem map_pow (f : α → β) (P : RegularExpression α) :
     ∀ n : ℕ, map f (P ^ n) = map f P ^ n
-  | 0 => by dsimp; rfl
+  | 0 => by unfold map; rfl
   | n + 1 => (congr_arg (· * map f P) (RegularExpression.map_pow f P n) : _)
 
 #adaptation_note /-- around nightly-2024-02-25,

Mathlib/Computability/TMToPartrec.lean

@@ -515,11 +515,11 @@ def Cont.then : Cont → Cont → Cont
 theorem Cont.then_eval {k k' : Cont} {v} : (k.then k').eval v = k.eval v >>= k'.eval := by
   induction k generalizing v with
   | halt => simp only [Cont.eval, Cont.then, pure_bind]
-  | cons₁ => simp only [Cont.eval, bind_assoc, *]
-  | cons₂ => simp only [Cont.eval, *]
-  | comp _ _ k_ih => simp only [Cont.eval, bind_assoc, ← k_ih]
+  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
+  | cons₂ => simp only [Cont.eval, Cont.then, *]
+  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
   | fix _ _ k_ih =>
-    simp only [Cont.eval, *]
+    simp only [Cont.eval, Cont.then, *]
     split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
 
 /-- The `then k` function is a "configuration homomorphism". Its operation on states is to append

Mathlib/Data/List/Basic.lean

@@ -1233,11 +1233,11 @@ theorem getElem_succ_scanl {i : ℕ} (h : i + 1 < (scanl f b l).length) :
   induction i generalizing b l with
   | zero =>
     cases l
-    · simp only [length, zero_eq, lt_self_iff_false] at h
+    · simp only [scanl, length, zero_eq, lt_self_iff_false] at h
     · simp
   | succ i hi =>
     cases l
-    · simp only [length] at h
+    · simp only [scanl, length] at h
       exact absurd h (by omega)
     · simp_rw [scanl_cons]
       rw [getElem_append_right]

Mathlib/Data/List/DropRight.lean

@@ -188,8 +188,9 @@ theorem rtakeWhile_eq_nil_iff : rtakeWhile p l = [] ↔ ∀ hl : l ≠ [], ¬p (
   induction' l using List.reverseRecOn with l a
   · simp only [rtakeWhile, takeWhile, reverse_nil, true_iff]
     intro f; contradiction
-  · simp only [rtakeWhile, reverse_append, takeWhile, ne_eq, not_false_eq_true,
-      getLast_append_of_ne_nil, getLast_singleton, reduceCtorEq]
+  · simp only [rtakeWhile, reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append,
+      takeWhile, ne_eq, cons_ne_self, not_false_eq_true, getLast_append_of_ne_nil,
+      getLast_singleton]
     refine ⟨fun h => ?_ , fun h => ?_⟩
     · split at h <;> simp_all
     · simp [h]