From 19078655bcfdf30f8309541309456055326dea6c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 3 Jan 2025 03:16:08 +0100
Subject: [PATCH] perf: avoid unnecessary assert/intro pairs in `grind` (#6514)

This PR enhances the assertion of new facts in `grind` by avoiding the
creation of unnecessary metavariables.
---
 src/Lean/Meta/Tactic/Grind/Intro.lean | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean
index 00438e1042..5c3c9da4e1 100644
--- a/src/Lean/Meta/Tactic/Grind/Intro.lean
+++ b/src/Lean/Meta/Tactic/Grind/Intro.lean
@@ -62,12 +62,12 @@ private def introNext (goal : Goal) : GrindM IntroResult := do
   else
     return .done
 
-private def isCasesCandidate (fvarId : FVarId) : MetaM Bool := do
-  let .const declName _ := (← fvarId.getType).getAppFn | return false
+private def isCasesCandidate (type : Expr) : MetaM Bool := do
+  let .const declName _ := type.getAppFn | return false
   isGrindCasesTarget declName
 
 private def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do
-  if (← isCasesCandidate fvarId) then
+  if (← isCasesCandidate (← fvarId.getType)) then
     let mvarIds ← cases goal.mvarId fvarId
     return mvarIds.map fun mvarId => { goal with mvarId }
   else
@@ -109,10 +109,17 @@ partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
 
 /-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
 def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : GrindM (List Goal) := do
-  -- TODO: check whether `prop` may benefit from `intros` or not. If not, we should avoid the `assert`+`intros` step and use `Grind.add`
-  let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
-  let goal := { goal with mvarId }
-  intros goal generation
+  if (← isCasesCandidate prop) then
+    let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
+    let goal := { goal with mvarId }
+    intros goal generation
+  else
+    let goal ← GoalM.run' goal do
+      let r ← simp prop
+      let prop' := r.expr
+      let proof' ← mkEqMP (← r.getProof) proof
+      add prop' proof' generation
+    if goal.inconsistent then return [] else return [goal]
 
 /-- Asserts next fact in the `goal` fact queue. -/
 def assertNext? (goal : Goal) : GrindM (Option (List Goal)) := do