fixes

leanprover-community · Jan 7, 2024 · 885169a · 885169a
1 parent 22688d1
commit 885169a
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 5 deletions.
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -1204,7 +1204,7 @@ theorem LinearOrderedRing.orderOf_le_two : orderOf x ≤ 2 := by
   cases' ne_or_eq |x| 1 with h h
   · simp [orderOf_abs_ne_one h]
   rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)
-  · simp; decide
+  · simp
   apply orderOf_le_of_pow_eq_one <;> norm_num
 #align linear_ordered_ring.order_of_le_two LinearOrderedRing.orderOf_le_two
 

diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -1057,7 +1057,7 @@ theorem succ_zero : succ (0 : Ordinal) = 1 :=
 -- Porting note: Proof used to be rfl
 @[simp]
 theorem succ_one : succ (1 : Ordinal) = 2 := by
-  unfold instOfNat OfNat.ofNat
+  unfold instOfNatAtLeastTwo OfNat.ofNat
   simpa using by rfl
 #align ordinal.succ_one Ordinal.succ_one
 

diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean
@@ -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 := Simp.DefaultMethods.methods)).1
+      Simp.mkEqTrans r' (← 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`

diff --git a/Mathlib/Tactic/Ring/RingNF.lean b/Mathlib/Tactic/Ring/RingNF.lean
@@ -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 := Simp.DefaultMethods.methods)).1
+      Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
   let nctx := { ctx, simp }
   let rec
     /-- The recursive context. -/
@@ -164,7 +164,8 @@ partial def M.run
 /-- Overrides the default error message in `ring1` to use a prettified version of the goal. -/
 initialize ringCleanupRef.set fun e => do
   M.run (← IO.mkRef {}) { recursive := false } fun nctx _ _ =>
-    return (← nctx.simp { expr := e } nctx.ctx |>.run {}).1.expr
+    return (← nctx.simp { expr := e } ({} : Lean.Meta.Simp.Methods).toMethodsRef nctx.ctx
+      |>.run {}).1.expr
 
 open Elab.Tactic Parser.Tactic
 /-- Use `ring_nf` to rewrite the main goal. -/