chore: changes required for leanprover/lean4#2783

Std/Classes/LawfulMonad.lean

@@ -74,7 +74,8 @@ namespace SatisfiesM
 /-- If `p` is always true, then every `x` satisfies it. -/
 theorem of_true [Applicative m] [LawfulApplicative m] {x : m α}
     (h : ∀ a, p a) : SatisfiesM p x :=
-  ⟨(fun a => ⟨a, h a⟩) <$> x, by simp [← comp_map, Function.comp]⟩
+  ⟨(fun a => ⟨a, h a⟩) <$> x,
+    by simp (config := { unfoldPartialApp := true }) [← comp_map, Function.comp]⟩
 
 /--
 If `p` is always true, then every `x` satisfies it.
@@ -93,7 +94,8 @@ protected theorem map [Functor m] [LawfulFunctor m] {x : m α}
     (hx : SatisfiesM p x) (hf : ∀ {a}, p a → q (f a)) : SatisfiesM q (f <$> x) := by
   let ⟨x', hx⟩ := hx
   refine ⟨(fun ⟨a, h⟩ => ⟨f a, hf h⟩) <$> x', ?_⟩
-  rw [← hx]; simp [← comp_map, Function.comp]
+  rw [← hx];
+  simp (config := { unfoldPartialApp := true }) [← comp_map, Function.comp]
 
 /--
 `SatisfiesM` distributes over `<$>`, strongest postcondition version.
@@ -126,8 +128,10 @@ protected theorem seq [Applicative m] [LawfulApplicative m] {x : m α}
     (H : ∀ {f a}, p₁ f → p₂ a → q (f a)) : SatisfiesM q (f <*> x) := by
   match f, x, hf, hx with | _, _, ⟨f, rfl⟩, ⟨x, rfl⟩ => ?_
   refine ⟨(fun ⟨a, h₁⟩ ⟨b, h₂⟩ => ⟨a b, H h₁ h₂⟩) <$> f <*> x, ?_⟩
-  simp only [← pure_seq]; simp [SatisfiesM, seq_assoc]
-  simp only [← pure_seq]; simp [seq_assoc, Function.comp]
+  simp only [← pure_seq]
+  simp only [seq_assoc, map_pure, seq_pure]
+  simp only [← pure_seq]
+  simp (config := { unfoldPartialApp := true }) only [Function.comp, seq_assoc, map_pure, seq_pure]
 
 /-- `SatisfiesM` distributes over `<*>`, strongest postcondition version. -/
 protected theorem seq_post [Applicative m] [LawfulApplicative m] {x : m α}

Std/Data/List/Basic.lean

@@ -656,7 +656,7 @@ theorem scanlTR_go_eq : ∀ l, scanlTR.go f l a acc = acc.data ++ scanl f a l
   | a :: l => by simp [scanlTR.go, scanl, scanlTR_go_eq l]
 
 @[csimp] theorem scanl_eq_scanlTR : @scanl = @scanlTR := by
-  funext α f n l; simp [scanlTR, scanlTR_go_eq]
+  funext α f n l; simp (config := { unfoldPartialApp := true }) [scanlTR, scanlTR_go_eq]
 
 /--
 Fold a function `f` over the list from the right, returning the list of partial results.
@@ -866,7 +866,7 @@ def tailsTR (l : List α) : List (List α) := go l #[] where
   funext α
   have H (l : List α) : ∀ acc, tailsTR.go l acc = acc.toList ++ tails l := by
     induction l <;> simp [*, tailsTR.go]
-  simp [tailsTR, H]
+  simp (config := { unfoldPartialApp := true }) [tailsTR, H]
 
 /--
 `sublists' l` is the list of all (non-contiguous) sublists of `l`.

Std/Data/List/Pairwise.lean

@@ -231,7 +231,7 @@ theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length),
   | cons₂ _ _ IH =>
     rcases IH with ⟨is,IH⟩
     refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
-    simp [comp, pairwise_map, IH]
+    simp (config := { unfoldPartialApp := true }) [comp, pairwise_map, IH]
 
 theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j) := by
   rw [pairwise_iff_forall_sublist]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-10-28
+leanprover/lean4-pr-releases:pr-release-2783