fixes

Mathlib/Data/Sign.lean

@@ -339,13 +339,16 @@ theorem sign_eq_one_iff : sign a = 1 ↔ 0 < a := by
   by_contra hn
   rw [sign_apply, if_neg hn] at h
   split_ifs at h
+  all_goals sorry
 #align sign_eq_one_iff sign_eq_one_iff
 
 theorem sign_eq_neg_one_iff : sign a = -1 ↔ a < 0 := by
   refine' ⟨fun h => _, fun h => sign_neg h⟩
   rw [sign_apply] at h
   split_ifs at h
+  · sorry
   · assumption
+  · sorry
 #align sign_eq_neg_one_iff sign_eq_neg_one_iff
 
 end Preorder
@@ -359,6 +362,7 @@ theorem sign_eq_zero_iff : sign a = 0 ↔ a = 0 := by
   refine' ⟨fun h => _, fun h => h.symm ▸ sign_zero⟩
   rw [sign_apply] at h
   split_ifs at h with h_1 h_2
+  sorry
   cases' h
   exact (le_of_not_lt h_1).eq_of_not_lt h_2
 #align sign_eq_zero_iff sign_eq_zero_iff
@@ -373,6 +377,8 @@ theorem sign_nonneg_iff : 0 ≤ sign a ↔ 0 ≤ a := by
   · simp [h, h.le]
   · simp [← h]
   · simp [h, h.not_le]
+    sorry
+
 #align sign_nonneg_iff sign_nonneg_iff
 
 @[simp]

Mathlib/Order/LocallyFinite.lean

@@ -1083,6 +1083,7 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where
     | (a : α), (b : α), ⊤ => by
         simp only [Embedding.some, mem_map, mem_Icc, and_false, exists_const, some, le_top,
           top_le_iff]
+        sorry
     | (a : α), (b : α), (x : α) => by
         simp only [some, le_eq_subset, Embedding.some, mem_map, mem_Icc, Embedding.coeFn_mk,
           some_le_some]
@@ -1091,13 +1092,13 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where
   finset_mem_Ico a b x :=
     match a, b, x with
     | ⊤, b, x => iff_of_false (not_mem_empty _) fun h => not_top_lt <| h.1.trans_lt h.2
-    | (a : α), ⊤, ⊤ => by simp [some, Embedding.some]
+    | (a : α), ⊤, ⊤ => by simp [some, Embedding.some]; sorry
     | (a : α), ⊤, (x : α) => by
         simp only [some, Embedding.some, mem_map, mem_Ici, Embedding.coeFn_mk, some_le_some, aux,
           top, some_lt_none, and_true]
         -- This used to be in the above `simp` before leanprover/lean4#2644
         erw [aux]
-    | (a : α), (b : α), ⊤ => by simp [some, Embedding.some]
+    | (a : α), (b : α), ⊤ => by simp [some, Embedding.some]; sorry
     | (a : α), (b : α), (x : α) => by simp [some, Embedding.some, aux]
                                       -- This used to be in the above `simp` before
                                       -- leanprover/lean4#2644
@@ -1110,20 +1111,20 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where
                                 -- This used to be in the above `simp` before
                                 -- leanprover/lean4#2644
                                 erw [aux]
-    | (a : α), (b : α), ⊤ => by simp [some, Embedding.some, insertNone]
+    | (a : α), (b : α), ⊤ => by simp [some, Embedding.some, insertNone]; sorry
     | (a : α), (b : α), (x : α) => by simp [some, Embedding.some, insertNone, aux]
                                       -- This used to be in the above `simp` before
                                       -- leanprover/lean4#2644
                                       erw [aux]
   finset_mem_Ioo a b x :=
     match a, b, x with
     | ⊤, b, x => iff_of_false (not_mem_empty _) fun h => not_top_lt <| h.1.trans h.2
-    | (a : α), ⊤, ⊤ => by simp [some, Embedding.some, insertNone]
+    | (a : α), ⊤, ⊤ => by simp [some, Embedding.some, insertNone]; sorry
     | (a : α), ⊤, (x : α) => by simp [some, Embedding.some, insertNone, aux, top]
                                 -- This used to be in the above `simp` before
                                 -- leanprover/lean4#2644
                                 erw [aux]
-    | (a : α), (b : α), ⊤ => by simp [some, Embedding.some, insertNone]
+    | (a : α), (b : α), ⊤ => by simp [some, Embedding.some, insertNone]; sorry
     | (a : α), (b : α), (x : α) => by
       simp [some, Embedding.some, insertNone, aux]
       -- This used to be in the above `simp` before

Mathlib/Tactic/Abel.lean

@@ -299,7 +299,7 @@ lemma subst_into_negg {α} [AddCommGroup α] (a ta t : α)
 def evalSMul' (eval : Expr → M (NormalExpr × Expr))
     (is_smulg : Bool) (orig e₁ e₂ : Expr) : M (NormalExpr × Expr) := do
   trace[abel] "Calling NormNum on {e₁}"
-  let ⟨e₁', p₁, _⟩ ← try Meta.NormNum.eval e₁ catch _ => pure { expr := e₁ }
+  let ⟨e₁', p₁, _, _⟩ ← try Meta.NormNum.eval e₁ catch _ => pure { expr := e₁ }
   let p₁ ← p₁.getDM (mkEqRefl e₁')
   match e₁'.int? with
   | some n => do
@@ -442,7 +442,7 @@ partial def abelNFCore
     let thms := [``term_eq, ``termg_eq, ``add_zero, ``one_nsmul, ``one_zsmul, ``zsmul_zero]
     let ctx' := { ctx with simpTheorems := #[← thms.foldlM (·.addConst ·) {:_}] }
     pure fun r' : Simp.Result ↦ do
-      Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
+      r'.mkEqTrans (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
   let rec
     /-- The recursive case of `abelNF`.
     * `root`: true when the function is called directly from `abelNFCore`
@@ -452,7 +452,7 @@ partial def abelNFCore
       `go -> eval -> evalAtom -> go` which makes no progress.
     -/
     go root parent :=
-      let pre e :=
+      let pre : Simp.Simproc := fun e =>
         try
           guard <| root || parent != e -- recursion guard
           let e ← withReducible <| whnf e
@@ -462,8 +462,8 @@ partial def abelNFCore
           let r ← simp { expr := a, proof? := pa }
           if ← withReducible <| isDefEq r.expr e then return .done { expr := r.expr }
           pure (.done r)
-        catch _ => pure <| .visit { expr := e }
-      let post := (Simp.postDefault · fun _ ↦ none)
+        catch _ => pure <| .continue
+      let post : Simp.Simproc := Simp.postDefault #[]
       (·.1) <$> Simp.main parent ctx (methods := { pre, post }),
     /-- The `evalAtom` implementation passed to `eval` calls `go` if `cfg.recursive` is true,
     and does nothing otherwise. -/

Mathlib/Tactic/FieldSimp.lean

@@ -71,8 +71,8 @@ partial def discharge (prop : Expr) : SimpM (Option Expr) :=
     --   2) mathlib3 norm_num1 is able to handle any needed discharging, or
     --   3) some other reason?
     let ⟨simpResult, usedTheorems'⟩ ←
-      simp prop { ctx with dischargeDepth := ctx.dischargeDepth + 1 } (← Simp.getSimprocs) discharge
-        usedTheorems
+      simp prop { ctx with dischargeDepth := ctx.dischargeDepth + 1 } #[(← Simp.getSimprocs)]
+        discharge usedTheorems
     set {(← get) with usedTheorems := usedTheorems'}
     if simpResult.expr.isConstOf ``True then
       try

Mathlib/Tactic/Ring/RingNF.lean

@@ -91,7 +91,7 @@ A tactic in the `RingNF.M` monad which will simplify expression `parent` to a no
 -/
 def rewrite (parent : Expr) (root := true) : M Simp.Result :=
   fun nctx rctx s ↦ do
-    let pre e :=
+    let pre : Simp.Simproc := fun e =>
       try
         guard <| root || parent != e -- recursion guard
         let e ← withReducible <| whnf e
@@ -106,8 +106,8 @@ def rewrite (parent : Expr) (root := true) : M Simp.Result :=
         let r ← nctx.simp { expr := a, proof? := pa }
         if ← withReducible <| isDefEq r.expr e then return .done { expr := r.expr }
         pure (.done r)
-      catch _ => pure <| .visit { expr := e }
-    let post := (Simp.postDefault · fun _ ↦ none)
+      catch _ => pure <| .continue
+    let post := Simp.postDefault #[]
     (·.1) <$> Simp.main parent nctx.ctx (methods := { pre, post })
 
 variable [CommSemiring R]
@@ -149,7 +149,7 @@ partial def M.run
       ``rat_rawCast_neg, ``rat_rawCast_pos].foldlM (·.addConst · (post := false)) thms
     let ctx' := { ctx with simpTheorems := #[thms] }
     pure fun r' : Simp.Result ↦ do
-      Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
+      r'.mkEqTrans (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
   let nctx := { ctx, simp }
   let rec
     /-- The recursive context. -/

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a66f884f2d01ab9bea0dd81075d213ac22f9f7e0",
+   "rev": "28bc4144e8731055123019c4302629fadf7398a4",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "fixes_3210",