diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 3e1efa5ed7..961e2a99fa 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -131,7 +131,7 @@ protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → Exc
 end ExceptT
 
 @[always_inline]
-instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
+instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
   throw e := ExceptT.mk <| throwThe ε₁ e
   tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
 
diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
index 3b31d69c4e..52e45ef9c7 100644
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -9,7 +9,7 @@ import Init.Meta
 
 open Function
 
-@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
+@[simp] theorem monadLift_self {m : Type u → Type v} (x : m α) : monadLift x = x :=
   rfl
 
 /--
diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
index f662c4c55f..f361949507 100644
--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -14,7 +14,7 @@ open Function
 
 namespace ExceptT
 
-theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
@@ -50,7 +50,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
 protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
   rfl
 
-protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
+protected theorem bind_pure_comp [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
   intros; rfl
 
 protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
@@ -200,11 +200,11 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   show (f >>= fun g => g <$> x).run s = _
   simp
 
-@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
+@[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
   show (x >>= fun _ => y).run s = _
   simp
 
-@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
+@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
   show (x >>= fun a => y >>= fun _ => pure a).run s = _
   simp
 
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 4bf6f19c8b..1df47eda77 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -67,7 +67,7 @@ instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 
-instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
+instance (ε : Type u) [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
   throw e           := OptionT.mk <| throwThe ε e
   tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle
 
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index b0e24e9aa4..541e99d3df 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -32,7 +32,7 @@ instance : MonadControl m (ReaderT ρ m) where
   restoreM x _ := x
 
 @[always_inline]
-instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
+instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
   tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
 
 @[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index ade42f7c0e..c3e6e60b30 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -87,7 +87,7 @@ protected def lift {α : Type u} (t : m α) : StateT σ m α :=
 instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩
 
 @[always_inline]
-instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
+instance (σ m) : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
 
 @[always_inline]
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean
index 3ecfdbf85d..37c8ef9159 100644
--- a/src/Init/Control/StateCps.lean
+++ b/src/Init/Control/StateCps.lean
@@ -14,16 +14,18 @@ def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type
 
 namespace StateCpsT
 
+variable {α σ : Type u} {m : Type u → Type v}
+
 @[always_inline, inline]
-def runK {α σ : Type u} {m : Type u → Type v}  (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
+def runK (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
   x _ s k
 
 @[always_inline, inline]
-def run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
+def run [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
   runK x s (fun a s => pure (a, s))
 
 @[always_inline, inline]
-def run' {α σ : Type u} {m : Type u → Type v}  [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
+def run' [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
   runK x s (fun a _ => pure a)
 
 @[always_inline]
@@ -48,29 +50,29 @@ protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
 instance [Monad m] : MonadLift m (StateCpsT σ m) where
   monadLift := StateCpsT.lift
 
-@[simp] theorem runK_pure {m : Type u → Type v} (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
+@[simp] theorem runK_pure (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
 
-@[simp] theorem runK_get {m : Type u → Type v} (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
+@[simp] theorem runK_get (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
 
-@[simp] theorem runK_set {m : Type u → Type v} (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
+@[simp] theorem runK_set (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
 
-@[simp] theorem runK_modify {m : Type u → Type v} (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
+@[simp] theorem runK_modify (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
 
-@[simp] theorem runK_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
+@[simp] theorem runK_lift [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
 
-@[simp] theorem runK_monadLift {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
+@[simp] theorem runK_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
     : (monadLift x : StateCpsT σ m α).runK s k = (monadLift x : m α) >>= (k . s) := rfl
 
-@[simp] theorem runK_bind_pure {α σ : Type u} [Monad m] (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
+@[simp] theorem runK_bind_pure (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
 
-@[simp] theorem runK_bind_lift {α σ : Type u} [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
+@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
     : (StateCpsT.lift x >>= f).runK s k = x >>= fun a => (f a).runK s k := rfl
 
-@[simp] theorem runK_bind_get {σ : Type u} [Monad m] (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
+@[simp] theorem runK_bind_get (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
 
-@[simp] theorem runK_bind_set {σ : Type u} [Monad m] (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
+@[simp] theorem runK_bind_set (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
 
-@[simp] theorem runK_bind_modify {σ : Type u} [Monad m] (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
+@[simp] theorem runK_bind_modify (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
 
 @[simp] theorem run_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s (fun a s => pure (a, s)) := rfl
 
diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index 7bbdd8c341..f38da6c2e9 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -34,22 +34,22 @@ protected def lift (x : m α) : StateRefT' ω σ m α :=
 
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
-instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
+instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
 instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
 
 @[inline]
-protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
+protected def get [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
   fun ref => ref.get
 
 @[inline]
-protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
+protected def set [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
   fun ref => ref.set s
 
 @[inline]
-protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
+protected def modifyGet [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
   fun ref => ref.modifyGet f
 
-instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
+instance [MonadLiftT (ST ω) m] : MonadStateOf σ (StateRefT' ω σ m) where
   get       := StateRefT'.get
   set       := StateRefT'.set
   modifyGet := StateRefT'.modifyGet
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 60730494cf..417df57192 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -642,7 +642,7 @@ instance : LawfulBEq String := inferInstance
 
 /-! # Logical connectives and equality -/
 
-@[inherit_doc True.intro] def trivial : True := ⟨⟩
+@[inherit_doc True.intro] theorem trivial : True := ⟨⟩
 
 theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
   fun ha => h₂ (h₁ ha)
@@ -1173,7 +1173,7 @@ def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
   s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
 
 instance Prod.lexLtDec
-    [LT α] [LT β] [DecidableEq α] [DecidableEq β]
+    [LT α] [LT β] [DecidableEq α]
     [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
     : (s t : α × β) → Decidable (Prod.lexLt s t) :=
   fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 2dd8f8ea33..1baab7545c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -184,8 +184,7 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     · simp only [h]
       rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
       · decide
-      · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
-        omega
+      · omega
 
 @[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
     x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
@@ -331,10 +330,7 @@ theorem toNat_eq_nat (x : BitVec w) (y : Nat)
   : (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by
   apply Iff.intro
   · intro eq
-    simp at eq
-    have lt := x.isLt
-    simp [eq] at lt
-    simp [←eq, lt, x.isLt]
+    simp [←eq, x.isLt]
   · intro eq
     simp [Nat.mod_eq_of_lt, eq]
 
@@ -1240,11 +1236,7 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
     (x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
   rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
-  suffices (x <<< r).getLsb i = false by
-    simp; omega
-  simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
-    Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
-  omega
+  simp; omega
 
 /--
 Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index be5fef7131..a4d5088b55 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -636,7 +636,7 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
   have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
 
 @[simp]
-theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
+theorem emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
   by_cases h : y = 0
   · simp [h]
   · simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index 4d5dad6956..60f1dba7f1 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -583,8 +583,6 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
   have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
   have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
   have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
-  have : (1 == (0 : Nat)) = false := rfl
-  have : (1 == (1 : Nat)) = true  := rfl
   by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
      <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 43be55f701..d8dfcadac9 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -740,7 +740,7 @@ prove `p` given any element `x : α`, then `p` holds. Note that it is essential
 that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
 to `Classical.choice`.
 -/
-protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
+protected theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
   match h₁ with
   | intro a => h₂ a
 
@@ -3150,7 +3150,7 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW
 instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
   withReader f := monadMap (m := m) (withTheReader ρ f)
 
-instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
+instance {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where
   withReader f x := fun ctx => x (f ctx)
 
 /--
@@ -3233,7 +3233,7 @@ def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → 
 of the state. It is equivalent to `get <* modify f` but may be more efficient.
 -/
 @[always_inline, inline]
-def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ :=
+def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ :=
   modifyGet fun s => (s, f s)
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 84c5f2c69c..121e361100 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -37,7 +37,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
-def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
+theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
   h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
@@ -58,7 +58,7 @@ class WellFoundedRelation (α : Sort u) where
   wf  : WellFounded rel
 
 namespace WellFounded
-def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
+theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
 section
@@ -78,7 +78,7 @@ noncomputable def fixF (x : α) (a : Acc r x) : C x := by
   induction a with
   | intro x₁ _ ih => exact F x₁ ih
 
-def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
+theorem fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
   induction acx with
   | intro x r _ => exact rfl
 
@@ -112,14 +112,14 @@ def emptyWf {α : Sort u} : WellFoundedRelation α where
 namespace Subrelation
 variable {α : Sort u} {r q : α → α → Prop}
 
-def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
+theorem accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
   induction ac with
   | intro x _ ih =>
     apply Acc.intro
     intro y h
     exact ih y (h₁ h)
 
-def wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
+theorem wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
   ⟨fun a => accessible @h₁ (apply h₂ a)⟩
 end Subrelation
 
@@ -136,10 +136,10 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
     subst x
     apply ih (f y) lt y rfl
 
-def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
+theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
   accAux f ac a rfl
 
-def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
+theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
@@ -151,7 +151,7 @@ end InvImage
 namespace TC
 variable {α : Sort u} {r : α → α → Prop}
 
-def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
+theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
   induction ac with
   | intro x acx ih =>
     apply Acc.intro x
@@ -160,7 +160,7 @@ def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
     | base a b rab => exact ih a rab
     | trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
 
-def wf (h : WellFounded r) : WellFounded (TC r) :=
+theorem wf (h : WellFounded r) : WellFounded (TC r) :=
   ⟨fun a => accessible (apply h a)⟩
 end TC
 
@@ -251,7 +251,7 @@ instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRe
         apply isFalse; intro contra; cases contra <;> contradiction
 
 -- TODO: generalize
-def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
+theorem right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
   match Nat.eq_or_lt_of_le h₁ with
   | Or.inl h => h ▸ Prod.Lex.right a₁ h₂
   | Or.inr h => Prod.Lex.left b₁ _ h
@@ -268,7 +268,7 @@ section
 variable {α : Type u} {β : Type v}
 variable {ra  : α → α → Prop} {rb  : β → β → Prop}
 
-def lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
+theorem lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
   induction aca generalizing b with
   | intro xa _ iha =>
     induction (acb b) with
@@ -347,7 +347,7 @@ variable {α : Sort u} {β : Sort v}
 def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
   Lex r (fun _ => s)
 
-def lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
+theorem lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
   WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun _ => hb) b
 end
 
@@ -365,7 +365,7 @@ open WellFounded
 variable {α : Sort u} {β : Sort v}
 variable {r  : α → α → Prop} {s : β → β → Prop}
 
-def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
+theorem revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
   induction acb with
   | intro xb _ ihb =>
     intro a
@@ -377,7 +377,7 @@ def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α)
       | left  => apply iha; assumption
       | right => apply ihb; assumption
 
-def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
+theorem revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
   WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
 end
 
@@ -389,7 +389,7 @@ def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFou
   rel := SkipLeft α hb.rel
   wf  := revLex emptyWf.wf hb.wf
 
-def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
+theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
   RevLex.right _ _ h
 end
 
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index e36bc0deff..0edd4a78d8 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -185,7 +185,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
 
-def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
+def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
     name            := impl.ref
     mkInitial       := pure {}
@@ -239,7 +239,7 @@ structure EnumAttributes (α : Type) where
   ext   : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
   deriving Inhabited
 
-def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α))
+def registerEnumAttributes (attrDescrs : List (Name × String × α))
     (validate : Name → α → AttrM Unit := fun _ _ => pure ())
     (applicationTime := AttributeApplicationTime.afterTypeChecking)
     (ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean
index 2c3ca13e69..066d1e967a 100644
--- a/src/Lean/DocString.lean
+++ b/src/Lean/DocString.lean
@@ -53,7 +53,7 @@ def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
 def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
   env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
 
-def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
+def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
   match stx.raw[1] with
   | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
   | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 50af639240..083af21296 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -39,7 +39,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
+def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
@@ -55,7 +55,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
   return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -65,7 +65,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 52b497d09e..132630b606 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -498,7 +498,7 @@ private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBeh
   Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
   If `mayPostpone == false`, then all of them must be synthesized.
   Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
-@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
+@[inline] def withSynthesize [MonadFunctorT TermElabM m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
   monadMap (m := TermElabM) (withSynthesizeImp · postpone) k
 
 private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α := do
@@ -512,7 +512,7 @@ private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α :=
     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
 /-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
-@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] [Monad m] (k : m α) : m α :=
+@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] (k : m α) : m α :=
   monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 
 /-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 69c23f1ee0..e66efb42dc 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -353,7 +353,7 @@ part. `act` is then run on the inner part but with reuse information adjusted as
 For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
 tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
 -/
-def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
+def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
     [MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
     (stx : Syntax) : m α := do
   let (outer, inner) := split stx
@@ -377,7 +377,7 @@ NOTE: child nodes after `argIdx` are not tested (which would almost always disab
 necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
 depend on them (i.e. they should not be inspected beforehand).
 -/
-def withNarrowedArgTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
+def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Context m]
     [MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
   withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
 
@@ -387,7 +387,7 @@ to `none`. This should be done for tactic blocks that are run multiple times as
 reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
 similarly questionable).
 -/
-def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
+def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
     (cond : Bool) (act : m α) : m α := do
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.filter fun tacSnap => Id.run do
@@ -398,7 +398,7 @@ def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOp
   }) act
 
 /-- Disables incremental tactic reuse for `act` if `cond` is true. -/
-def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
+def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
     (cond : Bool) (act : m α) : m α := do
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 3a2865fb7c..dd22b0469c 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -599,7 +599,7 @@ end TagDeclarationExtension
 
 def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
 
-def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
+def mkMapDeclarationExtension (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
   registerSimplePersistentEnvExtension {
     name          := name,
     addImportedFn := fun _ => {},
diff --git a/src/Lean/HeadIndex.lean b/src/Lean/HeadIndex.lean
index 24ea6874d5..dee9c91f50 100644
--- a/src/Lean/HeadIndex.lean
+++ b/src/Lean/HeadIndex.lean
@@ -32,8 +32,6 @@ inductive HeadIndex where
   | forallE
   deriving Inhabited, BEq, Repr
 
-namespace HeadIndex
-
 /-- Hash code for a `HeadIndex` value. -/
 protected def HeadIndex.hash : HeadIndex → UInt64
   | fvar fvarId         => mixHash 11 <| hash fvarId
@@ -47,8 +45,6 @@ protected def HeadIndex.hash : HeadIndex → UInt64
 
 instance : Hashable HeadIndex := ⟨HeadIndex.hash⟩
 
-end HeadIndex
-
 namespace Expr
 
 /-- Return the number of arguments in the given expression with respect to its `HeadIndex` -/
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 45a60f5264..d390a58d8d 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -850,7 +850,7 @@ def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
 Check for the presence of a value satisfying a predicate.
 -/
 @[inline]
-def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
+def containsValueP (t : DiscrTree α) (f : α → Bool) : Bool :=
   t.foldValues (init := false) fun r a => r || f a
 
 /--
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 51c55e24c7..fa6c13fa5d 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -175,7 +175,7 @@ def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
   | .stx _ ref => return ref
   | .other n => return n
 
-def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
+def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
   let perm := if s.perm then ":perm" else ""
   let name ← ppOrigin s.origin
   let prio := m!":{s.priority}"
diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index b0e82875cf..fc3ef6adab 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -81,7 +81,7 @@ namespace Meta
   `.const f` is not visited again. Put differently: every `.const f` is visited once, with its
   arguments if present, on its own otherwise.
  -/
-partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [AddMessageContext m]
+partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
     (input : Expr)
     (pre   : Expr → m TransformStep := fun _ => return .continue)
     (post  : Expr → m TransformStep := fun e => return .done e)
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index 2dac2267a2..ab6bf712c3 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -165,11 +165,11 @@ def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m Reducibil
   return getReducibilityStatusCore (← getEnv) declName
 
 /-- Set the reducibility attribute for the given declaration. -/
-def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
+def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
   modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
 /-- Set the given declaration as `[reducible]` -/
-def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
   setReducibilityStatus declName ReducibilityStatus.reducible
 
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
@@ -185,7 +185,7 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | _ => return false
 
 /-- Set the given declaration as `[irreducible]` -/
-def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
   setReducibilityStatus declName ReducibilityStatus.irreducible
 
 
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 6c583629b3..d4ff184656 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -307,7 +307,7 @@ def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Na
 def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
   ensureNoOverload n (← resolveGlobalConstCore n)
 
-def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
+def preprocessSyntaxAndResolve [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
   match stx with
   | .ident _ _ n pre => do
     let pre := pre.filterMap fun
diff --git a/src/Lean/Util/ForEachExprWhere.lean b/src/Lean/Util/ForEachExprWhere.lean
index e38bf0c56b..b2571d97be 100644
--- a/src/Lean/Util/ForEachExprWhere.lean
+++ b/src/Lean/Util/ForEachExprWhere.lean
@@ -16,8 +16,6 @@ if the number of subterms satisfying `p` is a small subset of the set of subterm
 If `p` holds for most subterms, then it is more efficient to use `forEach f e`.
 -/
 
-variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
-
 namespace ForEachExprWhere
 abbrev cacheSize : USize := 8192 - 1
 
@@ -37,7 +35,9 @@ unsafe def initCache : State := {
   checked := {}
 }
 
-abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] := StateRefT' ω State m
+abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] := StateRefT' ω State m
+
+variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
 
 unsafe def visited (e : Expr) : ForEachM m Bool := do
   let s ← get
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index 2ea1f902d5..179f9e9a3c 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -64,7 +64,7 @@ info: [Meta.debug] (Add.add => (node
     (* => (node #[5]))
     (Nat.add => (node (0 => (node (20 => (node #[3]))))))
 [Meta.debug] #[5, 1]
-[Meta.debug] Add.add ?m.4906 ?m.4906
+[Meta.debug] Add.add ?m.4899 ?m.4899
 [Meta.debug] #[5]
 [Meta.debug] #[5, 1, 4, 2]
 [Meta.debug] #[1, 4, 2, 5, 3]