fix: avoid mkEqMP

This PR ensures that `grind` does not use `mkEqMP`. It often triggered
type errors because `grind` uses the `[reducible]` transparency
setting by default. Increasing the transparency setting to default
was another possible, but less efficient fix.

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

@@ -65,7 +65,7 @@ private def closeGoalWithTrueEqFalse : GoalM Unit := do
   let mvarId := (← get).mvarId
   unless (← mvarId.isAssigned) do
     let trueEqFalse ← mkEqFalseProof (← getTrueExpr)
-    let falseProof ← mkEqMP trueEqFalse (mkConst ``True.intro)
+    let falseProof := mkApp4 (mkConst ``Eq.mp [levelZero]) (← getTrueExpr) (← getFalseExpr) trueEqFalse (mkConst ``True.intro)
     closeGoal falseProof
 
 /-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class. -/
@@ -74,7 +74,7 @@ private def closeGoalWithValuesEq (lhs rhs : Expr) : GoalM Unit := do
   let hp ← mkEqProof lhs rhs
   let d ← mkDecide p
   let pEqFalse := mkApp3 (mkConst ``eq_false_of_decide) p d.appArg! (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``false))
-  let falseProof ← mkEqMP pEqFalse hp
+  let falseProof := mkApp4 (mkConst ``Eq.mp [levelZero]) p (← getFalseExpr) pEqFalse hp
   closeGoal falseProof
 
 /--

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

@@ -28,7 +28,7 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   -- `e` is equal to `False`
   let eEqFalse ← mkEqFalseProof e
   -- So, we use `Eq.mp` to build a `proof` of `False`
-  let proof ← mkEqMP eEqFalse proof
+  let proof := mkApp4 (mkConst ``Eq.mp [levelZero]) e (← getFalseExpr) eEqFalse proof
   let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
   let proof' ← instantiateMVars (← mkLambdaFVars mvars proof)
   let prop' ← inferType proof'

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

@@ -216,7 +216,7 @@ def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : GrindTactic' := f
     let goal ← GoalM.run' goal do
       let r ← preprocess prop
       let prop' := r.expr
-      let proof' ← mkEqMP (← r.getProof) proof
+      let proof' := mkApp4 (mkConst ``Eq.mp [levelZero]) prop r.expr (← r.getProof) proof
       add prop' proof' generation
     if goal.inconsistent then return [] else return [goal]