diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index f7376e29a7..684ff82ddb 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -110,8 +110,8 @@ where
       return false
 
 private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
-  if thm.rfl then
-    return (← getConfig).implicitDefEqProofs
+  if (← getConfig).implicitDefEqProofs then
+    thm.getRfl
   else
     return false
 
@@ -218,7 +218,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
-        unless inErasedSet thm || (rflOnly && !thm.rfl) do
+        unless inErasedSet thm || (rflOnly && !(← thm.getRfl)) do
           if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
             trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
             return some result
@@ -236,7 +236,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
       for thm in candidates do
-        unless inErasedSet thm || (rflOnly && !thm.rfl) do
+        unless inErasedSet thm || (rflOnly && !(← thm.getRfl)) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue
             let type ← inferType val
@@ -352,7 +352,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
 def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
   for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
     -- Try lemma
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) }) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rflTask := (← isRflTheorem matchEq) }) with
     | none   => pure ()
     | some r => return .visit r
   return .continue
@@ -433,7 +433,7 @@ def sevalGround : Simproc := fun e => do
     -- `declName` has equation theorems associated with it.
     for eqn in eqns do
       -- TODO: cache SimpTheorem to avoid calls to `isRflTheorem`
-      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } then
+      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rflTask := (← isRflTheorem eqn) } then
         trace[Meta.Tactic.simp.ground] "unfolded, {e} => {result.expr}"
         return .visit result
     return .continue
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 8a4667764d..d0ef53b14d 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -122,45 +122,56 @@ structure SimpTheorem where
     It is also viewed an `id` used to "erase" `simp` theorems from `SimpTheorems`.
   -/
   origin      : Origin
-  /-- `rfl` is true if `proof` is by `Eq.refl` or `rfl`. -/
-  rfl         : Bool
+  /-- True if `proof` is by `Eq.refl` or `rfl`. Lazy so `[simp]` doesn't block the main thread. -/
+  rflTask     : Task Bool
   deriving Inhabited
 
+def SimpTheorem.getRfl (t : SimpTheorem) : CoreM Bool :=
+  traceBlock "SimpTheorem.getRfl" t.rflTask
+
 mutual
-  partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
+  partial def isRflProofCore (env : Environment) (type : Expr) (proof : Expr) : Task Bool :=
     match type with
     | .forallE _ _ type _ =>
       if let .lam _ _ proof _ := proof then
-        isRflProofCore type proof
+        isRflProofCore env type proof
       else
-        return false
+        .pure false
     | _ =>
       if type.isAppOfArity ``Eq 3 then
         if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then
-          return true
+          .pure true
         else if proof.isAppOfArity ``Eq.symm 4 then
           -- `Eq.symm` of rfl theorem is a rfl theorem
-          isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
+          isRflProofCore env type proof.appArg! -- small hack: we don't need to set the exact type
         else if proof.getAppFn.isConst then
           -- The application of a `rfl` theorem is a `rfl` theorem
           -- A constant which is a `rfl` theorem is a `rfl` theorem
-          isRflTheorem proof.getAppFn.constName!
+          isRflTheoremCore env proof.getAppFn.constName!
         else
-          return false
+          .pure false
       else
-        return false
+        .pure false
 
-  partial def isRflTheorem (declName : Name) : CoreM Bool := do
-    let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false
-    let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false
-    isRflProofCore info.type info.value
+  partial def isRflTheoremCore (env : Environment) (declName : Name) : Task Bool := Id.run do
+    env.findTask declName |>.bind (sync := true) fun
+      | none => .pure false
+      | some aconst => aconst.constInfo.bind (sync := true) fun
+        | .thmInfo info => isRflProofCore env info.type info.value
+        | _             => .pure false
 end
 
-def isRflProof (proof : Expr) : MetaM Bool := do
+def isRflProof (proof : Expr) : MetaM (Task Bool) := do
+  let env ← getEnv
   if let .const declName .. := proof then
-    isRflTheorem declName
+    return isRflTheoremCore env declName
   else
-    isRflProofCore (← inferType proof) proof
+    let type ← inferType proof
+    return isRflProofCore env type proof
+
+def isRflTheorem (declName : Name) : MetaM (Task Bool) := do
+  let env ← getEnv
+  return isRflTheoremCore env declName
 
 instance : ToFormat SimpTheorem where
   format s :=
@@ -401,7 +412,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
       match type.eq? with
       | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
-    return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
+    return { origin, keys, perm, post, levelParams, proof, priority := prio, rflTask := (← isRflProof proof) }
 
 private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool) (prio : Nat) : MetaM (Array SimpTheorem) := do
   let cinfo ← getConstVal declName
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index a9525f1e4f..d994a1f900 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -51,7 +51,7 @@ where
       let simpTheorem := {
         origin := .decl matchEqDeclName
         proof := mkConst matchEqDeclName
-        rfl := (← isRflTheorem matchEqDeclName)
+        rflTask := (← isRflTheorem matchEqDeclName)
       }
       match (← withReducible <| Simp.tryTheorem? e simpTheorem) with
       | none => return .continue
diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean
index 524819f8b9..df578584bc 100644
--- a/src/Lean/Meta/Tactic/Unfold.lean
+++ b/src/Lean/Meta/Tactic/Unfold.lean
@@ -22,7 +22,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
     return { expr  := (← deltaExpand e (· == declName)) }
 where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) }) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rflTask := (← isRflTheorem unfoldThm) }) with
     | none   => pure ()
     | some r => match (← reduceMatcher? r.expr) with
       | .reduced e' => return .done { r with expr := e' }