chore: fix tests

tests/lean/matchPatternPartialApp.lean

@@ -1,5 +1,5 @@
 def test2 : (Function.comp id id) = λ x : Nat => x := by
   conv in (Function.comp _) =>
     trace_state
-    simp [Function.comp, id]
+    simp (config := { unfoldPartialApp := true }) [Function.comp, id]
     trace_state

tests/lean/mutwf1.lean

@@ -19,7 +19,7 @@ termination_by'
      | PSum.inr n => (n, 0))
   $ Prod.lex sizeOfWFRel sizeOfWFRel
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.pred_lt

tests/lean/run/discrTreeSimp.lean

@@ -1,4 +1,5 @@
 prelude
+import Init.MetaTypes
 import Init.Data.List.Basic
 
 @[simp] theorem map_comp_map (f : α → β) (g : β → γ) : List.map g ∘ List.map f = List.map (g ∘ f) :=
@@ -18,4 +19,4 @@ theorem ex2 (f : Nat → Nat) : List.map f ∘ List.map f ∘ List.map f = List.
 attribute [simp] map_map
 
 theorem ex3 (f : Nat → Nat) (xs : List Nat) : (xs.map f |>.map f |>.map f) = xs.map (fun x => f (f (f x))) := by
-  simp [Function.comp]
+  simp (config := { unfoldPartialApp := true }) [Function.comp]

tests/lean/run/mutwf3.lean

@@ -20,7 +20,7 @@ termination_by'
       | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
     (Prod.lex sizeOfWFRel sizeOfWFRel)
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.lt_succ_self

tests/lean/run/setOptionTermTactic.lean

@@ -4,6 +4,6 @@ def f (x : Nat) : Nat :=
 def g (x : Nat) : Nat := 0 + x.succ
 
 theorem ex : f = g := by
-  simp only [f]
-  set_option trace.Meta.Tactic.simp true in simp only [Nat.add_succ, g]
-  simp only [Nat.zero_add]
+  simp (config := { unfoldPartialApp := true }) only [f]
+  set_option trace.Meta.Tactic.simp true in simp (config := { unfoldPartialApp := true }) only [Nat.add_succ, g]
+  simp (config := { unfoldPartialApp := true }) only [Nat.zero_add]

tests/lean/run/wfEqns2.lean

@@ -23,7 +23,7 @@ termination_by'
       | PSum.inr n => (n, 1))
     (Prod.lex sizeOfWFRel sizeOfWFRel)
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.lt_succ_self

tests/lean/run/wfEqns4.lean

@@ -26,7 +26,7 @@ termination_by'
       | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
     (Prod.lex sizeOfWFRel sizeOfWFRel)
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.lt_succ_self

tests/lean/simpZetaFalse.lean

@@ -18,7 +18,7 @@ theorem ex2 (x z : Nat) (h : f (f x) = x) (h' : z = x) : (let y := f (f x); y) =
 theorem ex3 (x z : Nat) : (let α := Nat; (fun x : α => 0 + x)) = id := by
   simp (config := { zeta := false, failIfUnchanged := false })
   trace_state -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
-  simp [id]
+  simp (config := { unfoldPartialApp := true }) [id]
 
 theorem ex4 (p : Prop) (h : p) : (let n := 10; fun x : { z : Nat // z < n } => x = x) = fun z => p := by
   simp (config := { zeta := false })

tests/lean/simp_trace.lean

@@ -59,7 +59,7 @@ def f2 : StateM Nat Unit := do
 -- Note: prior to PR #2489, the `Try this` suggestion reported by this `simp`
 -- call was incomplete.
 example : f1 = f2 := by
-  simp [f1, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, pure, set, StateT.set, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet]
+  simp (config := {unfoldPartialApp := true}) [f1, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, pure, set, StateT.set, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet]
 
 def h (x : Nat) : Sum (Nat × Nat) Nat := Sum.inl (x, x)
 

tests/lean/simp_trace.lean.expected.out

@@ -19,8 +19,8 @@ Try this: simp only [g, Id.pure_eq]
       (let x := x;
       pure x)
 [Meta.Tactic.simp.rewrite] @Id.pure_eq:1000, pure x ==> x
-Try this: simp only [f1, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, pure, f2, bind, StateT.bind, get,
-  getThe, MonadStateOf.get, StateT.get, set, StateT.set]
+Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet,
+  StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set]
 [Meta.Tactic.simp.rewrite] unfold f1, f1 ==> modify fun x => g x
 [Meta.Tactic.simp.rewrite] unfold modify, modify fun x => g x ==> modifyGet fun s => (PUnit.unit, (fun x => g x) s)
 [Meta.Tactic.simp.rewrite] unfold StateT.modifyGet, StateT.modifyGet fun s =>