fix tests

src/Init/Data/Array/Basic.lean

@@ -112,10 +112,6 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
-@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
-
-@[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
-
 end Array
 
 namespace List
@@ -338,8 +334,6 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
   decreasing_by simp_wf; decreasing_trivial_pre_omega
 
--- See also `Array.ofFnM` defined in `Init.Data.Array.OfFn`.
-
 /--
 Constructs an array that contains all the numbers from `0` to `n`, exclusive.
 

src/Init/Data/Array/Lemmas.lean

@@ -61,6 +61,11 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 @[grind] theorem size_empty : (#[] : Array α).size = 0 := rfl
 
+@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
+
+@[deprecated emptyWithCapacity_eq (since := "2025-03-12")]
+theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
+
 /-! ### size -/
 
 @[grind →] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
@@ -242,12 +247,6 @@ theorem back?_pop {xs : Array α} :
 
 /-! ### push -/
 
-@[simp] theorem push_empty : #[].push x = #[x] := rfl
-
-@[simp] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
-  rcases xs with ⟨xs⟩
-  simp
-
 @[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
   cases xs
   simp
@@ -3267,22 +3266,6 @@ rather than `(arr.push a).size` as the argument.
     (xs.push a).foldrM f init start = f a init >>= xs.foldrM f := by
   simp [← foldrM_push, h]
 
-@[simp, grind] theorem _root_.List.foldrM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
-    l.foldrM (fun x xs => xs.push <$> f x) xs = do return xs ++ (← l.reverse.mapM f).toArray := by
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp [ih]
-    congr 1
-    funext l'
-    congr 1
-    funext x
-    simp
-
-@[simp, grind] theorem _root_.List.foldlM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
-    l.foldlM (fun xs x => xs.push <$> f x) xs = do return xs ++ (← l.mapM f).toArray := by
-  induction l generalizing xs <;> simp [*]
-
 /-! ### foldl / foldr -/
 
 @[grind] theorem foldl_empty {f : β → α → β} {init : β} : (#[].foldl f init) = init := rfl
@@ -3379,32 +3362,6 @@ rather than `(arr.push a).size` as the argument.
   rcases as with ⟨as⟩
   simp
 
-@[simp, grind] theorem _root_.List.foldr_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
-    l.foldr (fun x xs => xs.push (f x)) xs = xs ++ (l.reverse.map f).toArray := by
-  induction l <;> simp [*]
-
-/-- Variant of `List.foldr_push_eq_append` specialized to `f = id`. -/
-@[simp, grind] theorem _root_.List.foldr_push_eq_append' {l : List α} {xs : Array α} :
-    l.foldr (fun x xs => xs.push x) xs = xs ++ l.reverse.toArray := by
-  induction l <;> simp [*]
-
-@[simp, grind] theorem _root_.List.foldl_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
-    l.foldl (fun xs x => xs.push (f x)) xs = xs ++ (l.map f).toArray := by
-  induction l generalizing xs <;> simp [*]
-
-/-- Variant of `List.foldl_push_eq_append` specialized to `f = id`. -/
-@[simp, grind] theorem _root_.List.foldl_push_eq_append' {l : List α} {xs : Array α} :
-    l.foldl (fun xs x => xs.push x) xs = xs ++ l.toArray := by
-  simpa using List.foldl_push_eq_append (f := id)
-
-@[deprecated _root_.List.foldl_push_eq_append' (since := "2025-05-18")]
-theorem _root_.List.foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
-  induction l generalizing as <;> simp [*]
-
-@[deprecated _root_.List.foldr_push_eq_append' (since := "2025-05-18")]
-theorem _root_.List.foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
-  rw [List.foldr_eq_foldl_reverse, List.foldl_push_eq_append']
-
 @[simp, grind] theorem foldr_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldr (f · ++ ·) ys = (xs.map f).flatten ++ ys := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Monadic.lean

@@ -25,11 +25,6 @@ open Nat
 
 /-! ## Monadic operations -/
 
-@[simp] theorem map_toList_inj [Monad m] [LawfulMonad m]
-    {xs : m (Array α)} {ys : m (Array α)} :
-   toList <$> xs = toList <$> ys ↔ xs = ys :=
-  _root_.map_inj_right (by simp)
-
 /-! ### mapM -/
 
 @[simp] theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Array α} {f : α → β} :
@@ -39,11 +34,6 @@ open Nat
 @[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
   mapM_pure
 
-@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {xs : Array α} :
-    (xs.map f).mapM g = xs.mapM (g ∘ f) := by
-  rcases xs with ⟨xs⟩
-  simp
-
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {xs ys : Array α} :
     (xs ++ ys).mapM f = (return (← xs.mapM f) ++ (← ys.mapM f)) := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/OfFn.lean

@@ -8,9 +8,7 @@ module
 prelude
 import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
-import Init.Data.Array.Monadic
 import Init.Data.List.OfFn
-import Init.Data.List.FinRange
 
 /-!
 # Theorems about `Array.ofFn`
@@ -21,8 +19,6 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
-/-! ### ofFn -/
-
 @[simp] theorem ofFn_zero {f : Fin 0 → α} : ofFn f = #[] := by
   simp [ofFn, ofFn.go]
 
@@ -36,23 +32,12 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     intro h₃
     simp only [show i = n by omega]
 
-theorem ofFn_add {n m} {f : Fin (n + m) → α} :
-    ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
-  induction m with
-  | zero => simp
-  | succ m ih => simp [ofFn_succ, ih]
-
 @[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
 
 @[simp] theorem toList_ofFn {f : Fin n → α} : (Array.ofFn f).toList = List.ofFn f := by
   apply List.ext_getElem <;> simp
 
-theorem ofFn_succ' {f : Fin (n+1) → α} :
-    ofFn f = #[f 0] ++ ofFn (fun i => f i.succ) := by
-  apply Array.toList_inj.mp
-  simp [List.ofFn_succ]
-
 @[simp]
 theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]
@@ -67,71 +52,4 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-/-! ### ofFnM -/
-
-/-- Construct (in a monadic context) an array by applying a monadic function to each index. -/
-def ofFnM {n} [Monad m] (f : Fin n → m α) : m (Array α) :=
-  Fin.foldlM n (fun xs i => xs.push <$> f i) (Array.emptyWithCapacity n)
-
-@[simp]
-theorem ofFnM_zero [Monad m] {f : Fin 0 → m α} : ofFnM f = pure #[] := by
-  simp [ofFnM]
-
-theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
-    ofFnM f = (do
-      let a ← f 0
-      let as ← ofFnM fun i => f i.succ
-      pure (#[a] ++ as)) := by
-  simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
-
-theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
-    ofFnM f = (do
-      let as ← ofFnM fun i => f i.castSucc
-      let a  ← f (Fin.last n)
-      pure (as.push a)) := by
-  simp [ofFnM, Fin.foldlM_succ_last]
-
-theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
-    ofFnM f = (do
-      let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))
-      let bs ← ofFnM fun i : Fin k => f (i.natAdd n)
-      pure (as ++ bs)) := by
-  induction k with
-  | zero => simp
-  | succ k ih =>
-    simp only [ofFnM_succ, Nat.add_eq, ih, Fin.castSucc_castLE, Fin.castSucc_natAdd, bind_pure_comp,
-      bind_assoc, bind_map_left, Fin.natAdd_last, map_bind, Functor.map_map]
-    congr 1
-    funext xs
-    congr 1
-    funext ys
-    congr 1
-    funext x
-    simp
-
-@[simp] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
-    toList <$> ofFnM f = List.ofFnM f := by
-  induction n with
-  | zero => simp
-  | succ n ih => simp [ofFnM_succ, List.ofFnM_succ_last, ← ih]
-
-@[simp]
-theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
-    ofFnM (pure ∘ f) = (pure (ofFn f) : m (Array α)) := by
-  apply Array.map_toList_inj.mp
-  simp
-
--- Variant of `ofFnM_pure_comp` using a lambda.
--- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
-theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
-    ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (Array α)) :=
-  ofFnM_pure_comp
-
-@[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
-    Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
-  induction n with
-  | zero => simp
-  | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]
-
 end Array

src/Init/Data/Fin/Fold.lean

@@ -100,11 +100,6 @@ Fin.foldrM n f xₙ = do
 
 /-! ### foldlM -/
 
-@[congr] theorem foldlM_congr [Monad m] {n k : Nat} (w : n = k) (f : α → Fin n → m α) :
-    foldlM n f = foldlM k (fun x i => f x (i.cast w.symm)) := by
-  subst w
-  rfl
-
 theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
     foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by
   rw [foldlM.loop, dif_pos h]
@@ -125,49 +120,14 @@ theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1)
     rw [foldlM_loop_eq, foldlM_loop_eq]
 termination_by n - i
 
-@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) : foldlM 0 f = pure := by
-  funext x
-  exact foldlM_loop_eq ..
+@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x :=
+  foldlM_loop_eq ..
 
-theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) :
-    foldlM (n+1) f = fun x => f x 0 >>= foldlM n (fun x j => f x j.succ) := by
-  funext x
-  exact foldlM_loop ..
-
-/-- Variant of `foldlM_succ` that splits off `Fin.last n` rather than `0`. -/
-theorem foldlM_succ_last [Monad m] [LawfulMonad m] (f : α → Fin (n+1) → m α) :
-    foldlM (n+1) f = fun x => foldlM n (fun x j => f x j.castSucc) x >>= (f · (Fin.last n)) := by
-  funext x
-  induction n generalizing x with
-  | zero =>
-    simp [foldlM_succ]
-  | succ n ih =>
-    rw [foldlM_succ]
-    conv => rhs; rw [foldlM_succ]
-    simp only [castSucc_zero, castSucc_succ, bind_assoc]
-    congr 1
-    funext x
-    rw [ih]
-    simp
-
-theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) :
-    foldlM (n + k) f =
-      fun x => foldlM n (fun x i => f x (i.castLE (Nat.le_add_right n k))) x >>= foldlM k (fun x i => f x (i.natAdd n)) := by
-  induction k with
-  | zero =>
-    funext x
-    simp
-  | succ k ih =>
-    funext x
-    simp [foldlM_succ_last, ← Nat.add_assoc, ih]
+theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) :
+    foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
 
 /-! ### foldrM -/
 
-@[congr] theorem foldrM_congr [Monad m] {n k : Nat} (w : n = k) (f : Fin n → α → m α) :
-    foldrM n f = foldrM k (fun i => f (i.cast w.symm)) := by
-  subst w
-  rfl
-
 theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
     foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by
   rw [foldrM.loop]
@@ -185,47 +145,19 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
     conv => rhs; rw [←bind_pure (f 0 x)]
     congr
     funext
-    simp [foldrM_loop_zero]
+    try simp only [foldrM.loop] -- the try makes this proof work with and without opaque wf rec
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..
 
-@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) : foldrM 0 f = pure := by
-  funext x
-  exact foldrM_loop_zero ..
+@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x :=
+  foldrM_loop_zero ..
 
-theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) :
-    foldrM (n+1) f = fun x => foldrM n (fun i => f i.succ) x >>= f 0 := by
-  funext x
-  exact foldrM_loop ..
-
-theorem foldrM_succ_last [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) :
-    foldrM (n+1) f = fun x => f (Fin.last n) x >>= foldrM n (fun i => f i.castSucc) := by
-  funext x
-  induction n generalizing x with
-  | zero => simp [foldrM_succ]
-  | succ n ih =>
-    rw [foldrM_succ]
-    conv => rhs; rw [foldrM_succ]
-    simp [ih]
-
-theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) :
-    foldrM (n + k) f =
-      fun x => foldrM k (fun i => f (i.natAdd n)) x >>= foldrM n (fun i => f (i.castLE (Nat.le_add_right n k))) := by
-  induction k with
-  | zero =>
-    simp
-  | succ k ih =>
-    funext x
-    simp [foldrM_succ_last, ← Nat.add_assoc, ih]
+theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
+    foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
 
 /-! ### foldl -/
 
-@[congr] theorem foldl_congr {n k : Nat} (w : n = k) (f : α → Fin n → α) :
-    foldl n f = foldl k (fun x i => f x (i.cast w.symm)) := by
-  subst w
-  rfl
-
 theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
     foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by
   rw [foldl.loop, dif_pos h]
@@ -255,34 +187,14 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
   rw [foldl_succ]
   induction n generalizing x with
   | zero => simp [foldl_succ, Fin.last]
-  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp
-
-theorem foldl_add (f : α → Fin (n + m) → α) (x) :
-    foldl (n + m) f x =
-      foldl m (fun x i => f x (i.natAdd n))
-        (foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by
-  induction m with
-  | zero => simp
-  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]
+  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = foldlM (m:=Id) n f x := by
   induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
 
--- This is not marked `@[simp]` as it would match on every occurrence of `foldlM`.
-theorem foldlM_pure [Monad m] [LawfulMonad m] {n} {f : α → Fin n → α} :
-    foldlM n (fun x i => pure (f x i)) x = (pure (foldl n f x) : m α) := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => simp [foldlM_succ, foldl_succ, ih]
-
 /-! ### foldr -/
 
-@[congr] theorem foldr_congr {n k : Nat} (w : n = k) (f : Fin n → α → α) :
-    foldr n f = foldr k (fun i => f (i.cast w.symm)) := by
-  subst w
-  rfl
-
 theorem foldr_loop_zero (f : Fin n → α → α) (x) :
     foldr.loop n f 0 (Nat.zero_le _) x = x := by
   rw [foldr.loop]
@@ -308,15 +220,7 @@ theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
     foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
   induction n generalizing x with
   | zero => simp [foldr_succ, Fin.last]
-  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp
-
-theorem foldr_add (f : Fin (n + m) → α → α) (x) :
-    foldr (n + m) f x =
-      foldr n (fun i => f (i.castLE (Nat.le_add_right n m)))
-        (foldr m (fun i => f (i.natAdd n)) x) := by
-  induction m generalizing x with
-  | zero => simp
-  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]
+  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = foldrM (m:=Id) n f x := by
@@ -334,11 +238,4 @@ theorem foldr_rev (f : α → Fin n → α) (x) :
   | zero => simp
   | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]
 
--- This is not marked `@[simp]` as it would match on every occurrence of `foldrM`.
-theorem foldrM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α → α} :
-    foldrM n (fun i x => pure (f i x)) x = (pure (foldr n f x) : m α) := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => simp [foldrM_succ, foldr_succ, ih]
-
 end Fin

src/Init/Data/Fin/Lemmas.lean

@@ -646,20 +646,6 @@ theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := k.rev_cast
 
 theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
 
-@[simp, grind _=_]
-theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := rfl
-
-@[simp, grind =]
-theorem castLE_refl (h : n ≤ n) (i : Fin n) : i.castLE h = i := rfl
-
-@[simp, grind =]
-theorem castSucc_castLE (h : n ≤ m) (i : Fin n) :
-    (i.castLE h).castSucc = i.castLE (by omega) := rfl
-
-@[simp, grind =]
-theorem castSucc_natAdd (n : Nat) (i : Fin k) :
-    (i.natAdd n).castSucc = (i.castSucc).natAdd n := rfl
-
 /-! ### pred -/
 
 @[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl

src/Init/Data/List/FinRange.lean

@@ -6,8 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
-import all Init.Data.List.OfFn
-import Init.Data.List.Monadic
+import Init.Data.List.OfFn
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -58,50 +57,3 @@ theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev :
     simp [Fin.rev_succ]
 
 end List
-
-namespace Fin
-
-theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α) :
-    foldlM n f x = (List.finRange n).foldlM f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    simp [foldlM_succ, List.finRange_succ, List.foldlM_cons]
-    congr 1
-    funext y
-    simp [ih, List.foldlM_map]
-
-theorem foldrM_eq_finRange_foldrM [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
-    foldrM n f x = (List.finRange n).foldrM f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    simp [foldrM_succ, List.finRange_succ, ih, List.foldrM_map]
-
-theorem foldl_eq_finRange_foldl (f : α → Fin n → α) (x : α) :
-    foldl n f x = (List.finRange n).foldl f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    simp [foldl_succ, List.finRange_succ, ih, List.foldl_map]
-
-theorem foldr_eq_finRange_foldr (f : Fin n → α → α) (x : α) :
-    foldr n f x = (List.finRange n).foldr f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    simp [foldr_succ, List.finRange_succ, ih, List.foldr_map]
-
-end Fin
-
-namespace List
-
-theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
-    ofFnM f = (do
-      let a ← f 0
-      let as ← ofFnM fun i => f i.succ
-      pure (a :: as)) := by
-  simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.finRange_succ, List.foldlM_cons_eq_append,
-    List.foldlM_map]
-
-end List

src/Init/Data/List/Lemmas.lean

@@ -2576,11 +2576,6 @@ theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
     l.foldl (fun xs y => f y :: xs) l' = (l.map f).reverse ++ l' := by
   induction l generalizing l' <;> simp [*]
 
-/-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/
-@[simp, grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
-    l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
-  induction l generalizing l' <;> simp [*]
-
 @[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
   induction l <;> simp [*]

src/Init/Data/List/Monadic.lean

@@ -8,8 +8,6 @@ module
 prelude
 import Init.Data.List.TakeDrop
 import Init.Data.List.Attach
-import Init.Data.List.OfFn
-import Init.Data.Array.Bootstrap
 import all Init.Data.List.Control
 
 /-!
@@ -71,17 +69,13 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α}
 @[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f :=
   mapM_pure
 
-@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {l : List α} :
-    (l.map f).mapM g = l.mapM (g ∘ f) := by
-  induction l <;> simp_all
-
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
 /-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`. -/
 theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α → m β} {as : List α} {b : β} {bs : List β} :
-    (as.foldlM (init := b :: bs) fun acc a => (· :: acc) <$> f a) =
-      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => (· :: acc) <$> f a := by
+    (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
+      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc) := by
   induction as generalizing b bs with
   | nil => simp
   | cons a as ih =>
@@ -89,7 +83,7 @@ theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α → m β} {as :
     simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]
 
 theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
-    mapM f l = reverse <$> (l.foldlM (fun acc a => (· :: acc) <$> f a) []) := by
+    mapM f l = reverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) []) := by
   rw [← mapM'_eq_mapM]
   induction l with
   | nil => simp

src/Init/Data/List/OfFn.lean

@@ -27,13 +27,6 @@ Examples:
 -/
 def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
 
-/--
-Creates a list wrapped in a monad by applying the monadic function `f : Fin n → m α`
-to each potential index in order, starting at `0`.
--/
-def ofFnM {n} [Monad m] (f : Fin n → m α) : m (List α) :=
-  List.reverse <$> Fin.foldlM n (fun xs i => (· :: xs) <$> f i) []
-
 @[simp]
 theorem length_ofFn {f : Fin n → α} : (ofFn f).length = n := by
   simp only [ofFn]
@@ -56,8 +49,7 @@ protected theorem getElem_ofFn {f : Fin n → α} (h : i < (ofFn f).length) :
       simp_all
 
 @[simp]
-protected theorem getElem?_ofFn {f : Fin n → α} :
-    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
+protected theorem getElem?_ofFn {f : Fin n → α} : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
   if h : i < (ofFn f).length
   then by
     rw [getElem?_eq_getElem h, List.getElem_ofFn]
@@ -68,31 +60,16 @@ protected theorem getElem?_ofFn {f : Fin n → α} :
 
 /-- `ofFn` on an empty domain is the empty list. -/
 @[simp]
-theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] := by
-  rw [ofFn, Fin.foldr_zero]
+theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] :=
+  ext_get (by simp) (fun i hi₁ hi₂ => by contradiction)
 
+@[simp]
 theorem ofFn_succ {n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
   ext_get (by simp) (fun i hi₁ hi₂ => by
     cases i
     · simp
     · simp)
 
-theorem ofFn_succ_last {n} {f : Fin (n + 1) → α} :
-    ofFn f = (ofFn fun i => f i.castSucc) ++ [f (Fin.last n)] := by
-  induction n with
-  | zero => simp [ofFn_succ]
-  | succ n ih =>
-    rw [ofFn_succ]
-    conv => rhs; rw [ofFn_succ]
-    rw [ih]
-    simp
-
-theorem ofFn_add {n m} {f : Fin (n + m) → α} :
-    ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
-  induction m with
-  | zero => simp
-  | succ m ih => simp [ofFn_succ_last, ih]
-
 @[simp]
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]
@@ -115,66 +92,4 @@ theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩ := by
   simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]
 
-/-- `ofFnM` on an empty domain is the empty list. -/
-@[simp]
-theorem ofFnM_zero [Monad m] [LawfulMonad m] {f : Fin 0 → m α} : ofFnM f = pure [] := by
-  simp [ofFnM]
-
-/-! See `Init.Data.List.FinRange` for the `ofFnM_succ` variant. -/
-
-theorem ofFnM_succ_last {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
-    ofFnM f = (do
-      let as ← ofFnM fun i => f i.castSucc
-      let a  ← f (Fin.last n)
-      pure (as ++ [a])) := by
-  simp [ofFnM, Fin.foldlM_succ_last]
-
-theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
-    ofFnM f = (do
-      let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))
-      let bs ← ofFnM fun i : Fin k => f (i.natAdd n)
-      pure (as ++ bs)) := by
-  induction k with
-  | zero => simp
-  | succ k ih => simp [ofFnM_succ_last, ih]
-
-
-end List
-
-namespace Fin
-
-theorem foldl_cons_eq_append {f : Fin n → α} {xs : List α} :
-    Fin.foldl n (fun xs i => f i :: xs) xs = (List.ofFn f).reverse ++ xs := by
-  induction n generalizing xs with
-  | zero => simp
-  | succ n ih => simp [Fin.foldl_succ, List.ofFn_succ, ih]
-
-theorem foldr_cons_eq_append {f : Fin n → α} {xs : List α} :
-    Fin.foldr n (fun i xs => f i :: xs) xs = List.ofFn f ++ xs:= by
-  induction n generalizing xs with
-  | zero => simp
-  | succ n ih => simp [Fin.foldr_succ, List.ofFn_succ, ih]
-
-end Fin
-
-namespace List
-
-@[simp]
-theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
-    ofFnM (pure ∘ f) = (pure (ofFn f) : m (List α)) := by
-  simp [ofFnM, Fin.foldlM_pure, Fin.foldl_cons_eq_append]
-
--- Variant of `ofFnM_pure_comp` using a lambda.
--- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
-theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
-    ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (List α)) :=
-  ofFnM_pure_comp
-
-@[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
-    Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
-  induction n with
-  | zero => simp
-  | succ n ih => simp [ofFnM_succ_last, ofFn_succ_last, ih]
-
 end List

src/Init/Data/List/ToArray.lean

@@ -210,6 +210,12 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
   cases as
   simp
 
+@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
+  induction l generalizing as <;> simp [*]
+
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
+  rw [foldr_eq_foldl_reverse, foldl_push]
+
 @[simp, grind =] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]

src/Init/Data/Nat/Fold.lean

@@ -197,64 +197,6 @@ theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bo
       omega
   go n 0 f
 
-/-! # `dfold` -/
-
-private def dfoldCast {n : Nat} (α : (i : Nat) → (h : i ≤ n := by omega) → Type u)
-    {i j : Nat} {hi : i ≤ n} (w : i = j) (x : α i hi) : α j (by omega) := by
-  subst w
-  exact x
-
-@[local simp] private theorem dfoldCast_rfl (h : i ≤ n) (w : i = i) (x : α i h) : dfoldCast α w x = x := by
-  simp [dfoldCast]
-
-@[local simp] private theorem dfoldCast_trans (h : i ≤ n) (w₁ : i = j) (w₂ : j = k) (x : α i h) :
-    dfoldCast @α w₂ (dfoldCast @α w₁ x) = dfoldCast @α (w₁.trans w₂) x := by
-  cases w₁
-  cases w₂
-  simp [dfoldCast]
-
-@[local simp] private theorem dfoldCast_eq_dfoldCast_iff {α : (i : Nat) → (h : i ≤ n := by omega) → Type u} {w₁ w₂ : i = j} {h : i ≤ n} {x : α i h} :
-    dfoldCast @α w₁ x = dfoldCast (n := n) (fun i h => α i) (hi := hi) w₂ x ↔ w₁ = w₂ := by
-  cases w₁
-  cases w₂
-  simp [dfoldCast]
-
-private theorem apply_dfoldCast {α : (i : Nat) → (h : i ≤ n := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n) → α i → α (i + 1)) {i j : Nat} (h : i < n) {w : i = j} {x : α i (by omega)} :
-    f j (by omega) (dfoldCast @α w x) = dfoldCast (n := n) (fun i h => α i) (hi := by omega) (by omega) (f i h x) := by
-  subst w
-  simp
-
-/--
-`Nat.dfold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
-* `Nat.dfold f 3 init = init |> f 0 |> f 1 |> f 2`
-The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α i → α (i + 1)`.
--/
-@[specialize]
-def dfold (n : Nat) {α : (i : Nat) → (h : i ≤ n := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n) → α i → α (i + 1)) (init : α 0) : α n :=
-  let rec @[specialize] loop : ∀ j, j ≤ n → α (n - j) → α n
-    | 0,      h, a => a
-    | succ m, h, a =>
-      loop m (by omega) (dfoldCast @α (by omega) (f (n - succ m) (by omega) a))
-  loop n (by omega) (dfoldCast @α (by omega) init)
-
-/--
-`Nat.dfoldRev` evaluates `f` on the numbers up to `n` exclusive, in decreasing order:
-* `Nat.dfoldRev f 3 init = f 0 <| f 1 <| f 2 <| init`
-The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α (i + 1) → α i`.
--/
-@[specialize]
-def dfoldRev (n : Nat) {α : (i : Nat) → (h : i ≤ n := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n) → α (i + 1) → α i) (init : α n) : α 0 :=
-  match n with
-  | 0       => init
-  | (n + 1) => dfoldRev n (α := fun i h => α i) (fun i h => f i (by omega)) (f n (by omega) init)
-
-/-! # Theorems -/
-
-/-! ### `fold` -/
-
 @[simp] theorem fold_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
     fold 0 f init = init := by simp [fold]
 
@@ -268,8 +210,6 @@ theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n
   | succ n ih =>
     simp [ih, List.finRange_succ_last, List.foldl_map]
 
-/-! ### `foldRev` -/
-
 @[simp] theorem foldRev_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
     foldRev 0 f init = init := by simp [foldRev]
 
@@ -283,12 +223,10 @@ theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i <
   | zero => simp
   | succ n ih => simp [ih, List.finRange_succ_last, List.foldr_map]
 
-/-! ### `any` -/
-
 @[simp] theorem any_zero {f : (i : Nat) → i < 0 → Bool} : any 0 f = false := by simp [any]
 
 @[simp] theorem any_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
-    any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
+  any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
 
 theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
     any n f = (List.finRange n).any (fun ⟨i, h⟩ => f i h) := by
@@ -296,12 +234,10 @@ theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
   | zero => simp
   | succ n ih => simp [ih, List.finRange_succ_last, List.any_map, Function.comp_def]
 
-/-! ### `all` -/
-
 @[simp] theorem all_zero {f : (i : Nat) → i < 0 → Bool} : all 0 f = true := by simp [all]
 
 @[simp] theorem all_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
-    all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
+  all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
 
 theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
     all n f = (List.finRange n).all (fun ⟨i, h⟩ => f i h) := by
@@ -309,108 +245,12 @@ theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
   | zero => simp
   | succ n ih => simp [ih, List.finRange_succ_last, List.all_map, Function.comp_def]
 
-/-! ### `dfold` -/
-
-@[simp]
-theorem dfold_zero
-    {α : (i : Nat) → (h : i ≤ 0 := by omega) → Type u}
-    (f : (i : Nat) → (h : i < 0) → α i → α (i + 1)) (init : α 0) :
-    dfold 0 f init = init := by
-  simp [dfold, dfold.loop]
-
-private theorem dfold_loop_succ
-    {α : (i : Nat) → (h : i ≤ n + 1 := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n + 1) → α i → α (i + 1))
-    (a : α (n + 1 - (j + 1))) (w : j ≤ n):
-    dfold.loop (n + 1) f (j + 1) (by omega) a =
-      f n (by omega)
-        (dfold.loop n (α := fun i h => α i) (fun i h => f i (by omega)) j w (dfoldCast @α (by omega) a)) := by
-  induction j with
-  | zero => simp [dfold.loop]
-  | succ j ih =>
-    rw [dfold.loop, ih _ (by omega)]
-    congr 2
-    simp only [succ_eq_add_one, dfoldCast_trans]
-    rw [apply_dfoldCast (h := by omega) f]
-    · erw [dfoldCast_trans (h := by omega)]
-      erw [dfoldCast_eq_dfoldCast_iff]
-      omega
-
-@[simp]
-theorem dfold_succ
-    {α : (i : Nat) → (h : i ≤ n + 1 := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n + 1) → α i → α (i + 1)) (init : α 0) :
-    dfold (n + 1) f init =
-      f n (by omega) (dfold n (α := fun i h => α i) (fun i h => f i (by omega)) init) := by
-  simp [dfold]
-  rw [dfold_loop_succ (w := Nat.le_refl _)]
-  congr 2
-  simp only [dfoldCast_trans]
-  erw [dfoldCast_eq_dfoldCast_iff]
-  exact le_add_left 0 (n + 1)
-
--- This isn't a proper `@[congr]` lemma, but it doesn't seem possible to state one.
-theorem dfold_congr
-    {n m : Nat} (w : n = m)
-    {α : (i : Nat) → (h : i ≤ n := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n) → α i → α (i + 1)) (init : α 0) :
-      dfold n f init =
-        cast (by subst w; rfl)
-          (dfold m (α := fun i h => α i) (fun i h => f i (by omega)) init) := by
-  subst w
-  rfl
-
-theorem dfold_add
-    {α : (i : Nat) → (h : i ≤ n + m := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n + m) → α i → α (i + 1)) (init : α 0) :
-    dfold (n + m) f init =
-      dfold m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega))
-        (dfold n (α := fun i h => α i) (fun i h => f i (by omega)) init) := by
-  induction m with
-  | zero => simp; rfl
-  | succ m ih =>
-    simp [dfold_congr (Nat.add_assoc n m 1).symm, ih]
-
-@[simp] theorem dfoldRev_zero
-    {α : (i : Nat) → (h : i ≤ 0 := by omega) → Type u}
-    (f : (i : Nat) → (_ : i < 0) → α (i + 1) → α i) (init : α 0) :
-    dfoldRev 0 f init = init := by
-  simp [dfoldRev]
-
-@[simp] theorem dfoldRev_succ
-    {α : (i : Nat) → (h : i ≤ n + 1 := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n + 1) → α (i + 1) → α i) (init : α (n + 1)) :
-    dfoldRev (n + 1) f init =
-      dfoldRev n (α := fun i h => α i) (fun i h => f i (by omega)) (f n (by omega) init) := by
-  simp [dfoldRev]
-
-@[congr]
-theorem dfoldRev_congr
-    {n m : Nat} (w : n = m)
-    {α : (i : Nat) → (h : i ≤ n := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n) → α (i + 1) → α i) (init : α n) :
-      dfoldRev n f init =
-        dfoldRev m (α := fun i h => α i) (fun i h => f i (by omega))
-          (cast (by subst w; rfl) init) := by
-  subst w
-  rfl
-
-theorem dfoldRev_add
-    {α : (i : Nat) → (h : i ≤ n + m := by omega) → Type u}
-    (f : (i : Nat) → (h : i < n + m) → α (i + 1) → α i) (init : α (n + m)) :
-    dfoldRev (n + m) f init =
-      dfoldRev n (α := fun i h => α i) (fun i h => f i (by omega))
-        (dfoldRev m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega)) init) := by
-  induction m with
-  | zero => simp; rfl
-  | succ m ih => simp [← Nat.add_assoc, ih]
-
 end Nat
 
 namespace Prod
 
 /--
-Combines an initial value with each natural number from a range, in increasing order.
+Combines an initial value with each natural number from in a range, in increasing order.
 
 In particular, `(start, stop).foldI f init` applies `f`on all the numbers
 from `start` (inclusive) to `stop` (exclusive) in increasing order:
@@ -420,7 +260,7 @@ Examples:
 * `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]`
 * `(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]`
 -/
-@[inline, simp] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (init : α) : α :=
+@[inline] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (init : α) : α :=
   (i.2 - i.1).fold (fun j _ => f (i.1 + j) (by omega) (by omega)) init
 
 /--
@@ -434,7 +274,7 @@ Examples:
  * `(5, 8).anyI (fun j _ _ => j % 2 = 0) = true`
  * `(6, 6).anyI (fun j _ _ => j % 2 = 0) = false`
 -/
-@[inline, simp] def anyI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
+@[inline] def anyI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
   (i.2 - i.1).any (fun j _ => f (i.1 + j) (by omega) (by omega))
 
 /--
@@ -448,7 +288,7 @@ Examples:
  * `(5, 8).allI (fun j _ _ => j % 2 = 0) = false`
  * `(6, 7).allI (fun j _ _ => j % 2 = 0) = true`
 -/
-@[inline, simp] def allI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
+@[inline] def allI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
   (i.2 - i.1).all (fun j _ => f (i.1 + j) (by omega) (by omega))
 
 end Prod

src/Init/Data/Vector/Basic.lean

@@ -307,8 +307,6 @@ abbrev zipWithIndex := @zipIdx
 @[inline] def ofFn (f : Fin n → α) : Vector α n :=
   ⟨Array.ofFn f, by simp⟩
 
-/-! See also `Vector.ofFnM` defined in `Init.Data.Vector.OfFn`. -/
-
 /--
 Swap two elements of a vector using `Fin` indices.
 

src/Init/Data/Vector/Lemmas.lean

@@ -53,9 +53,9 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
     (Vector.mk xs size).contains a = xs.contains a := by
   simp [contains]
 
-@[simp] theorem push_mk {xs : Array α} {size : xs.size = n} :
-    (Vector.mk xs size).push =
-      fun x => Vector.mk (xs.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
+@[simp] theorem push_mk {xs : Array α} {size : xs.size = n} {x : α} :
+    (Vector.mk xs size).push x =
+      Vector.mk (xs.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
 
 @[simp] theorem pop_mk {xs : Array α} {size : xs.size = n} :
     (Vector.mk xs size).pop = Vector.mk xs.pop (by simp [size]) := rfl
@@ -1660,12 +1660,12 @@ theorem forall_mem_append {p : α → Prop} {xs : Vector α n} {ys : Vector α m
     (∀ (x) (_ : x ∈ xs ++ ys), p x) ↔ (∀ (x) (_ : x ∈ xs), p x) ∧ (∀ (x) (_ : x ∈ ys), p x) := by
   simp only [mem_append, or_imp, forall_and]
 
-@[simp, grind]
+@[grind]
 theorem empty_append {xs : Vector α n} : (#v[] : Vector α 0) ++ xs = xs.cast (by omega) := by
   rcases xs with ⟨as, rfl⟩
   simp
 
-@[simp, grind]
+@[grind]
 theorem append_empty {xs : Vector α n} : xs ++ (#v[] : Vector α 0) = xs := by
   rw [← toArray_inj, toArray_append, Array.append_empty]
 

src/Init/Data/Vector/Monadic.lean

@@ -38,11 +38,6 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
   apply map_toArray_inj.mp
   simp
 
-@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {xs : Vector α n} :
-    (xs.map f).mapM g = xs.mapM (g ∘ f) := by
-  apply map_toArray_inj.mp
-  simp
-
 @[congr] theorem mapM_congr [Monad m] {xs ys : Vector α n} (w : xs = ys)
     {f : α → m β} :
     xs.mapM f = ys.mapM f := by

src/Init/Data/Vector/OfFn.lean

@@ -8,7 +8,6 @@ module
 prelude
 import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
-import Init.Data.Vector.Monadic
 import Init.Data.Array.OfFn
 
 /-!
@@ -41,122 +40,4 @@ theorem back_ofFn {n} [NeZero n] {f : Fin n → α} :
     (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩ := by
   simp [back]
 
-theorem ofFn_succ {f : Fin (n+1) → α} :
-    ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
-  ext i h
-  · simp only [getElem_ofFn, getElem_push, Fin.castSucc_mk, left_eq_dite_iff]
-    intro h'
-    have : i = n := by omega
-    simp_all
-
-theorem ofFn_add {n m} {f : Fin (n + m) → α} :
-    ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
-  apply Vector.toArray_inj.mp
-  simp [Array.ofFn_add]
-
-theorem ofFn_succ' {f : Fin (n+1) → α} :
-    ofFn f = (#v[f 0] ++ ofFn (fun i => f i.succ)).cast (by omega) := by
-  apply Vector.toArray_inj.mp
-  simp [Array.ofFn_succ']
-
-/-! ### ofFnM -/
-
-/-- Construct (in a monadic context) a vector by applying a monadic function to each index. -/
-def ofFnM {n} [Monad m] (f : Fin n → m α) : m (Vector α n) :=
-  go 0 (by omega) (Array.emptyWithCapacity n) rfl where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #v[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (h' : i ≤ n) (acc : Array α) (w : acc.size = i) : m (Vector α n) := do
-    if h : i < n then
-      go (i+1) (by omega) (acc.push (← f ⟨i, h⟩)) (by simp [w])
-    else
-      pure ⟨acc, by omega⟩
-
-@[simp]
-theorem ofFnM_zero [Monad m] {f : Fin 0 → m α} : Vector.ofFnM f = pure #v[] := by
-  simp [ofFnM, ofFnM.go]
-
-private theorem ofFnM_go_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α}
-    (hi : i ≤ n := by omega) {h : xs.size = i} :
-    ofFnM.go f i (by omega) xs h = (do
-      let as ← ofFnM.go (fun i => f i.castSucc) i hi xs h
-      let a  ← f (Fin.last n)
-      pure (as.push a)) := by
-  fun_induction ofFnM.go f i (by omega) xs h
-  case case1 acc h' h ih =>
-    if h : acc.size = n then
-      unfold ofFnM.go
-      rw [dif_neg (by omega)]
-      have h : ¬ acc.size + 1 < n + 1 := by omega
-      have : Fin.last n = ⟨acc.size, by omega⟩ := by ext; simp; omega
-      simp [*]
-    else
-      have : acc.size + 1 ≤ n := by omega
-      simp only [ih, this]
-      conv => rhs; unfold ofFnM.go
-      rw [dif_pos (by omega)]
-      simp
-  case case2 =>
-    omega
-
-theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
-    ofFnM f = (do
-      let as ← ofFnM fun i => f i.castSucc
-      let a  ← f (Fin.last n)
-      pure (as.push a)) := by
-  simp [ofFnM, ofFnM_go_succ]
-
-theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
-    ofFnM f = (do
-      let as ← ofFnM (fun i => f (i.castLE (Nat.le_add_right n k)))
-      let bs ← ofFnM (fun i => f (i.natAdd n))
-      pure (as ++ bs)) := by
-  induction k with
-  | zero => simp
-  | succ k ih => simp [ofFnM_succ, ih, ← push_append]
-
-@[simp, grind] theorem toArray_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
-    toArray <$> ofFnM f = Array.ofFnM f := by
-  induction n with
-  | zero => simp
-  | succ n ih => simp [ofFnM_succ, Array.ofFnM_succ, ← ih]
-
-@[simp, grind] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
-    toList <$> Vector.ofFnM f = List.ofFnM f := by
-  unfold toList
-  suffices Array.toList <$> (toArray <$> ofFnM f) = List.ofFnM f by
-    simpa [-toArray_ofFnM]
-  simp
-
-theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
-    ofFnM f = (do
-      let a ← f 0
-      let as ← ofFnM fun i => f i.succ
-      pure ((#v[a] ++ as).cast (by omega))) := by
-  apply Vector.map_toArray_inj.mp
-  simp only [toArray_ofFnM, Array.ofFnM_succ', bind_pure_comp, map_bind, Functor.map_map,
-    toArray_cast, toArray_append]
-  congr 1
-  funext x
-  have : (fun xs : Vector α n => #[x] ++ xs.toArray) = (#[x] ++ ·) ∘ toArray := by funext xs; simp
-  simp [this, comp_map]
-
-@[simp]
-theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
-    ofFnM (pure ∘ f) = (pure (ofFn f) : m (Vector α n)) := by
-  apply Vector.map_toArray_inj.mp
-  simp
-
--- Variant of `ofFnM_pure_comp` using a lambda.
--- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
-theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
-    ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (Vector α n)) :=
-  ofFnM_pure_comp
-
-@[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
-    Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
-  induction n with
-  | zero => simp
-  | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]
-
 end Vector

src/Init/Grind/CommRing/Basic.lean

@@ -10,6 +10,7 @@ import Init.Data.Zero
 import Init.Data.Int.DivMod.Lemmas
 import Init.Data.Int.Pow
 import Init.TacticsExtra
+import Init.Grind.Module.Basic
 
 /-!
 # A monolithic commutative ring typeclass for internal use in `grind`.
@@ -108,6 +109,24 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
   next => simp [pow_zero, mul_one]
   next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc]
 
+instance : NatModule α where
+  hMul a x := a * x
+  add_zero := by simp [add_zero]
+  zero_add := by simp [zero_add]
+  add_assoc := by simp [add_assoc]
+  add_comm := by simp [add_comm]
+  zero_hmul := by simp [natCast_zero, zero_mul]
+  one_hmul := by simp [natCast_one, one_mul]
+  add_hmul := by simp [natCast_add, right_distrib]
+  hmul_zero := by simp [mul_zero]
+  hmul_add := by simp [left_distrib]
+  mul_hmul := by simp [natCast_mul, mul_assoc]
+
+theorem hmul_eq_natCast_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = (k : α) * a := rfl
+
+theorem hmul_eq_ofNat_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = OfNat.ofNat k * a := by
+  simp [ofNat_eq_natCast, hmul_eq_natCast_mul]
+
 end Semiring
 
 namespace Ring
@@ -243,6 +262,24 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
   next => simp [pow_zero, Int.pow_zero, intCast_one]
   next k ih => simp [pow_succ, Int.pow_succ, intCast_mul, *]
 
+instance : IntModule α where
+  hMul a x := a * x
+  add_zero := by simp [add_zero]
+  zero_add := by simp [zero_add]
+  add_assoc := by simp [add_assoc]
+  add_comm := by simp [add_comm]
+  zero_hmul := by simp [intCast_zero, zero_mul]
+  one_hmul := by simp [intCast_one, one_mul]
+  add_hmul := by simp [intCast_add, right_distrib]
+  hmul_zero := by simp [mul_zero]
+  hmul_add := by simp [left_distrib]
+  mul_hmul := by simp [intCast_mul, mul_assoc]
+  neg_hmul := by simp [intCast_neg, neg_mul]
+  neg_add_cancel := by simp [neg_add_cancel]
+  sub_eq_add_neg := by simp [sub_eq_add_neg]
+
+theorem hmul_eq_intCast_mul {α} [Ring α] {k : Int} {a : α} : HMul.hMul (α := Int) k a = (k : α) * a := rfl
+
 end Ring
 
 namespace CommSemiring
@@ -347,14 +384,7 @@ theorem natCast_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
 
 end IsCharP
 
-/--
-Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
--/
-class NoNatZeroDivisors (α : Type u) [Ring α] where
-  no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
-
-export NoNatZeroDivisors (no_nat_zero_divisors)
-
+-- TODO: This should be generalizable to any `IntModule α`, not just `Ring α`.
 theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k : Int} {a : α}
     : k ≠ 0 → k * a = 0 → a = 0 := by
   match k with
@@ -362,13 +392,12 @@ theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k :
     simp [intCast_natCast]
     intro h₁ h₂
     replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
-    rw [← ofNat_eq_natCast] at h₂
     exact no_nat_zero_divisors k a h₁ h₂
   | -(k+1 : Nat) =>
     rw [Int.natCast_add, ← Int.natCast_add, intCast_neg, intCast_natCast]
     intro _ h
     replace h := congrArg (-·) h; simp at h
-    rw [← neg_mul, neg_neg, neg_zero, ← ofNat_eq_natCast] at h
+    rw [← neg_mul, neg_neg, neg_zero, ← hmul_eq_natCast_mul] at h
     exact no_nat_zero_divisors (k+1) a (Nat.succ_ne_zero _) h
 
 end Lean.Grind

src/Init/Grind/CommRing/Fin.lean

@@ -104,7 +104,11 @@ instance (n : Nat) [NeZero n] : CommRing (Fin n) where
   intCast_neg := Fin.intCast_neg
 
 instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where
-  ofNat_eq_zero_iff x := by simp only [OfNat.ofNat, Fin.ofNat']; simp
+  ofNat_eq_zero_iff x := by
+    change Fin.ofNat' _ _ = Fin.ofNat' _ _ ↔ _
+    simp only [Fin.ofNat']
+    simp only [Nat.zero_mod]
+    simp only [Fin.mk.injEq]
 
 end Fin
 

src/Init/Grind/Module/Basic.lean

@@ -49,13 +49,6 @@ instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
     hmul_add := by simp [IntModule.hmul_add]
     mul_hmul := by simp [IntModule.mul_hmul] }
 
-/--
-We keep track of rational linear combinations as integer linear combinations,
-but with the assurance that we can cancel the GCD of the coefficients.
--/
-class RatModule (M : Type u) extends IntModule M where
-  no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k * a = 0 → a = 0
-
 /-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
 class Preorder (α : Type u) extends LE α, LT α where
   le_refl : ∀ a : α, a ≤ a
@@ -73,4 +66,12 @@ class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
   hmul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k * a
   hmul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k * a ≤ 0
 
+/--
+Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
+-/
+class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where
+  no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0
+
+export NoNatZeroDivisors (no_nat_zero_divisors)
+
 end Lean.Grind

src/Init/Grind/Module/Int.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Grind.Module.Basic
+import Init.Grind.CommRing.Int
 import Init.Omega
 
 /-!
@@ -15,21 +16,6 @@ import Init.Omega
 
 namespace Lean.Grind
 
-instance : IntModule Int where
-  add_zero := Int.add_zero
-  zero_add := Int.zero_add
-  add_comm := Int.add_comm
-  add_assoc := Int.add_assoc
-  zero_hmul := Int.zero_mul
-  one_hmul := Int.one_mul
-  add_hmul := Int.add_mul
-  neg_hmul := Int.neg_mul
-  hmul_zero := Int.mul_zero
-  hmul_add := Int.mul_add
-  mul_hmul := Int.mul_assoc
-  neg_add_cancel := Int.add_left_neg
-  sub_eq_add_neg _ _ := Int.sub_eq_add_neg
-
 instance : Preorder Int where
   le_refl := Int.le_refl
   le_trans _ _ _ := Int.le_trans

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -111,8 +111,13 @@ where
         | trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
       trace_goal[grind.ring] "characteristic: {n}"
       pure <| some (charInst, n)
-    let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type ringInst
-    let noZeroDivInst? := (← trySynthInstance noZeroDivType).toOption
+    let noZeroDivInst? ← withNewMCtxDepth do
+      let zeroType := mkApp (mkConst ``Zero [u]) type
+      let .some zeroInst ← trySynthInstance zeroType | return none
+      let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
+      let .some hmulInst ← trySynthInstance hmulType | return none
+      let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
+      LOption.toOption <$> trySynthInstance noZeroDivType
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let addFn ← getAddFn type u semiringInst
     let mulFn ← getMulFn type u semiringInst

tests/lean/grind/module_normalization.lean

@@ -10,8 +10,8 @@ example (a b : R) : a + b = b + a := by grind
 example (a : R) : a + 0 = a := by grind
 example (a : R) : 0 + a = a := by grind
 example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 • a = a + a := by grind
-example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
+example (a : R) : 2 * a = a + a := by grind
+example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
 
 end NatModule
 
@@ -23,10 +23,10 @@ example (a b : R) : a + b = b + a := by grind
 example (a : R) : a + 0 = a := by grind
 example (a : R) : 0 + a = a := by grind
 example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 • a = a + a := by grind
-example (a : R) : (-2 : Int) • a = -a - a := by grind
-example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
-example (a b c : R) : 2 • (b + c) - 3 • c + b + b = c + 5 • b - 2 • c := by grind
-example (a b c : R) : 2 • (b + c) + (-3 : Int) • c + b + b = c + (5 : Int) • b - 2 • c := by grind
+example (a : R) : 2 * a = a + a := by grind
+example (a : R) : (-2 : Int) * a = -a - a := by grind
+example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
+example (a b c : R) : 2 * (b + c) - 3 * c + b + b = c + 5 * b - 2 * c := by grind
+example (a b c : R) : 2 * (b + c) + (-3 : Int) * c + b + b = c + (5 : Int) * b - 2 • c := by grind
 
 end IntModule

tests/lean/grind/module_relations.lean

@@ -8,20 +8,20 @@ variable (R : Type u) [IntModule R]
 
 -- In an `IntModule`, we should be able to handle relations
 -- this is harder, and less important, than being able to do this in `RatModule`.
-example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
+example (a b : R) (h : a + b = 0) : 3 * a - 7 * b = 9 * a + a := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) + a := by grind
 
 end IntModule
 
 section RatModule
 
-variable (R : Type u) [RatModule R]
+variable (R : Type u) [IntModule R] [NoNatZeroDivisors R]
 
-example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
+example (a b : R) (h : a + b = 0) : 3 * a - 7 * b = 9 * a + a := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) + a := by grind
 
 -- In a `RatModule` we can clear common divisors.
 example (a : R) (h : a + a = 0) : a = 0 := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - 3 • b := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - 3 * b := by grind
 
 end RatModule

tests/lean/grind/ordered_modules.lean

@@ -2,7 +2,7 @@ open Lean.Grind
 
 set_option grind.warning false
 
-variable (R : Type u) [RatModule R] [Preorder R] [IntModule.IsOrdered R]
+variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [Preorder R] [IntModule.IsOrdered R]
 
 example (a b c : R) (h : a < b) : a + c < b + c := by grind
 example (a b c : R) (h : a < b) : c + a < c + b := by grind
@@ -15,50 +15,50 @@ example (a b : R) (h : a ≤ b) : -b ≤ -a := by grind
 example (a b : R) (h : a ≤ b) : -a ≤ -b := by grind
 
 example (a : R) (h : 0 < a) : 0 ≤ a := by grind
-example (a : R) (h : 0 < a) : -2 • a < 0 := by grind
+example (a : R) (h : 0 < a) : -2 * a < 0 := by grind
 
 example (a b c : R) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c := by grind
 example (a b c : R) (_ : a ≤ b) (_ : b < c) : a < c := by grind
 example (a b c : R) (_ : a < b) (_ : b ≤ c) : a < c := by grind
 example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
 
-example (a : R) (h : 2 • a < 0) : a < 0 := by grind
-example (a : R) (h : 2 • a < 0) : 0 ≤ -a := by grind
+example (a : R) (h : 2 * a < 0) : a < 0 := by grind
+example (a : R) (h : 2 * a < 0) : 0 ≤ -a := by grind
 
 example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
 example (a b : R) (_ : a < b ∧ b < a) : False := by grind
 example (a b : R) (_ : a < b) : a ≠ b := by grind
 
-example (a b c e v0 v1 : R) (h1 : v0 = 5 • a) (h2 : v1 = 3 • b) (h3 : v0 + v1 + c = 10 • e) :
-    v0 + 5 • e + (v1 - 3 • e) + (c - 2 • e) = 10 • e := by
+example (a b c e v0 v1 : R) (h1 : v0 = 5 * a) (h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10 * e) :
+    v0 + 5 * e + (v1 - 3 * e) + (c - 2 * e) = 10 * e := by
   grind
 
 example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
   grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) : False := by
+example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
   grind
 
 example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
     False := by grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) :
+example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) :
     False := by grind
 
 example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3*y := by
   grind
-example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
+example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
 example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
   grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) : ¬ 12 • y - 4 • z < 0 := by
+example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12 * y - 4 * z < 0 := by
   grind
 
 example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
-example (x y z : R) (hx : ¬ x > 3 • y) (h2 : ¬ y > 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
+example (x y z : R) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
 example (x y z : Nat) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
-example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
+example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind

tests/lean/run/infoFromFailure.lean

@@ -16,21 +16,7 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
-    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
-    [Meta.synthInstance] new goal Lean.Grind.IntModule String
-      [Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule String
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
-    [Meta.synthInstance] no instances for Lean.Grind.RatModule String
-      [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
-    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
-    [Meta.synthInstance] new goal Lean.Grind.NatModule String
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
-  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
+    [Meta.synthInstance.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd, @Lean.Grind.Semiring.toAdd]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -51,6 +37,20 @@ trace: [Meta.synthInstance] ❌️ Add String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
     [Meta.synthInstance] no instances for Lean.Grind.CommRing String
       [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] new goal Lean.Grind.IntModule String
+      [Meta.synthInstance.instances] #[@Lean.Grind.Ring.instIntModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.instIntModule to Lean.Grind.IntModule String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] new goal Lean.Grind.NatModule String
+      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.instNatModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.instNatModule to Lean.Grind.NatModule String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
+  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
   [Meta.synthInstance] result <not-available>
 -/
 #guard_msgs in
@@ -61,21 +61,7 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
-    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
-    [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
-      [Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule Bool
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
-    [Meta.synthInstance] no instances for Lean.Grind.RatModule Bool
-      [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
-    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
-    [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
-  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
+    [Meta.synthInstance.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd, @Lean.Grind.Semiring.toAdd]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.Semiring Bool
@@ -96,6 +82,20 @@ trace: [Meta.synthInstance] ❌️ Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
     [Meta.synthInstance] no instances for Lean.Grind.CommRing Bool
       [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.Ring.instIntModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.instIntModule to Lean.Grind.IntModule Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
+      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.instNatModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.instNatModule to Lean.Grind.NatModule Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
+  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
   [Meta.synthInstance] result <not-available>
 -/
 #guard_msgs in