fix: fix: bug in mkEqProof within grind

This PR fixes another bug in the equality proof generator in the (WIP) `grind`
tactic.

src/Lean/Meta/Tactic/Grind.lean

@@ -32,5 +32,6 @@ builtin_initialize registerTraceClass `grind.debug.proofs
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.congr
 builtin_initialize registerTraceClass `grind.proof
+builtin_initialize registerTraceClass `grind.proof.detail
 
 end Lean

src/Lean/Meta/Tactic/Grind/Proof.lean

@@ -81,6 +81,7 @@ mutual
     else
       flipProof h flipped heq
 
+  /-- Given `acc : lhs₀ = lhs`, returns a proof of `lhs₀ = common`. -/
   private partial def mkProofTo (lhs : Expr) (common : Expr) (acc : Option Expr) (heq : Bool) : GoalM (Option Expr) := do
     if isSameExpr lhs common then
       return acc
@@ -92,9 +93,7 @@ mutual
     let acc ← mkTrans' acc h heq
     mkProofTo target common (some acc) heq
 
-  /--
-  Given `lhsEqCommon : lhs = common`, returns a proof for `lhs = rhs`.
-  -/
+  /-- Given `lhsEqCommon : lhs = common`, returns a proof for `lhs = rhs`. -/
   private partial def mkProofFrom (rhs : Expr) (common : Expr) (lhsEqCommon? : Option Expr) (heq : Bool) : GoalM (Option Expr) := do
     if isSameExpr rhs common then
       return lhsEqCommon?
@@ -124,14 +123,22 @@ Returns a proof that `a = b` (or `HEq a b`).
 It assumes `a` and `b` are in the same equivalence class.
 -/
 def mkEqProof (a b : Expr) : GoalM Expr := do
-  let n ← getRootENode a
-  trace[grind.proof] "{a} {if n.heqProofs then "≡" else "="} {b}"
-  if !n.heqProofs then
-    mkEqProofCore a b (heq := false)
-  else if (← withDefault <| isDefEq (← inferType a) (← inferType b)) then
-    mkEqProofCore a b (heq := false)
-  else
-    mkEqProofCore a b (heq := true)
+  let p ← go
+  trace[grind.proof.detail] "{p}"
+  return p
+where
+  go : GoalM Expr := do
+    let n ← getRootENode a
+    if !n.heqProofs then
+      trace[grind.proof] "{a} = {b}"
+      mkEqProofCore a b (heq := false)
+    else
+      if (← withDefault <| isDefEq (← inferType a) (← inferType b)) then
+        trace[grind.proof] "{a} = {b}"
+        mkEqOfHEq (← mkEqProofCore a b (heq := true))
+      else
+        trace[grind.proof] "{a} ≡ {b}"
+        mkEqProofCore a b (heq := true)
 
 /--
 Returns a proof that `a = True`.

tests/lean/run/grind_pre.lean

@@ -9,6 +9,7 @@ elab "grind_pre" : tactic => do
 abbrev f (a : α) := a
 
 set_option grind.debug true
+set_option grind.debug.proofs true
 
 /--
 warning: declaration uses 'sorry'
@@ -112,7 +113,13 @@ theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x :=
 
 def h (a : α) := a
 
-set_option trace.grind.pre true
+set_option trace.grind.pre true in
 example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c ∧ c = a → a = b ∧ b = a → a ≠ c := by
   grind_pre
   sorry
+
+set_option trace.grind.proof.detail true in
+set_option trace.grind.proof true in
+example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by
+  grind_pre
+  sorry