chore(GRewrite): copy how rw elaborates (#38558)

Since `grw` has been merged, some subtle changes have been made to how `rw` elaborates. This PR copies those changes over to `grw`.

In one place, a proof had to be adapted. Previously, the side goals created by `grw` were filled in by unification in the next rewrite. This is not possible anymore because these side goals are now marked synthetic opaque.

Author: JovanGerb

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -248,8 +248,8 @@ theorem aestronglyMeasurable_condExpInd (hs : MeasurableSet s) (hμs : μ s ≠
 @[simp]
 theorem condExpInd_empty : condExpInd G hm μ ∅ = (0 : G →L[ℝ] α →₁[μ] G) := by
   ext x
-  grw [condExpInd_ae_eq_condExpIndSMul, condExpIndSMul_empty, zero_apply, Lp.coeFn_zero,
-    Lp.coeFn_zero]
+  grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
+    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]
 
 theorem condExpInd_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) :
     condExpInd F hm μ s (c • x) = c • condExpInd F hm μ s x :=
@@ -291,7 +291,8 @@ theorem setIntegral_condExpInd (hs : MeasurableSet[m] s) (ht : MeasurableSet t)
 theorem condExpInd_of_measurable (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) (c : G) :
     condExpInd G hm μ s c = indicatorConstLp 1 (hm s hs) hμs c := by
   ext1
-  grw [indicatorConstLp_coeFn, condExpInd_ae_eq_condExpIndSMul, condExpIndSMul_ae_eq_smul]
+  grw [indicatorConstLp_coeFn, condExpInd_ae_eq_condExpIndSMul hm (hm s hs) hμs,
+    condExpIndSMul_ae_eq_smul]
   rw [condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)]
   filter_upwards [@indicatorConstLp_coeFn α _ _ 2 μ _ s (hm s hs) hμs (1 : ℝ)] with x hx
   rw [hx]

Mathlib/Tactic/GRewrite/Elab.lean

@@ -21,25 +21,44 @@ This file defines the tactics that use the backend defined in `Mathlib.Tactic.GR
 
 -/
 
-public meta section
+meta section
 
 namespace Mathlib.Tactic
 
 open Lean Meta Elab Parser Tactic
 
+/-- Analogous to `elabRewrite`. -/
+def elabGRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax) (forwardImp symm : Bool)
+    (config : GRewrite.Config) : TacticM GRewriteResult := do
+  let mvarCounterSaved := (← getMCtx).mvarCounter
+  let thm ← elabTerm stx none true
+  if thm.hasSyntheticSorry then
+    throwAbortTactic
+  unless ← occursCheck mvarId thm do
+    throwErrorAt stx
+      "Occurs check failed: Expression{indentExpr thm}\ncontains the goal {Expr.mvar mvarId}"
+  let r ← mvarId.grewrite e thm (forwardImp := forwardImp) (symm := symm) (config := config)
+  let mctx ← getMCtx
+  let mvarIds := r.mvarIds.filter fun mvarId => mvarCounterSaved ≤ (mctx.getDecl mvarId).index
+  return { r with mvarIds }
+
+/-- Analogous to `finishElabRewrite`. -/
+def finishElabGRewrite (r : GRewriteResult) : MetaM GRewriteResult := do
+  let mvarIds ← r.mvarIds.filterM (not <$> ·.isAssigned)
+  mvarIds.forM fun newMVarId => newMVarId.withContext do
+    if ← Meta.isProp (← newMVarId.getType) then
+      newMVarId.setKind .syntheticOpaque
+  return { r with mvarIds }
+
 /-- Apply the `grewrite` tactic to the current goal. -/
 def grewriteTarget (stx : Syntax) (symm : Bool) (config : GRewrite.Config) : TacticM Unit := do
   let goal ← getMainGoal
-  Term.withSynthesize <| goal.withContext do
-    let e ← elabTerm stx none true
-    if e.hasSyntheticSorry then
-      throwAbortTactic
-    let goal ← getMainGoal
-    let target ← goal.getType
-    let r ← goal.grewrite target e (forwardImp := false) (symm := symm) (config := config)
-    let mvarNew ← mkFreshExprSyntheticOpaqueMVar r.eNew (← goal.getTag)
-    goal.assign (mkApp r.impProof mvarNew)
-    replaceMainGoal (mvarNew.mvarId! :: r.mvarIds)
+  let r ← Term.withSynthesize <| goal.withContext do
+    elabGRewrite goal (← goal.getType) stx (forwardImp := false) (symm := symm) (config := config)
+  let r ← finishElabGRewrite r
+  let mvarNew ← mkFreshExprSyntheticOpaqueMVar r.eNew (← goal.getTag)
+  goal.assign (r.impProof.app mvarNew)
+  replaceMainGoal (mvarNew.mvarId! :: r.mvarIds)
 
 /-- Apply the `grewrite` tactic to a local hypothesis. -/
 def grewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : GRewrite.Config) :
@@ -48,12 +67,9 @@ def grewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : G
   -- See issues https://github.com/leanprover-community/mathlib4/issues/2711 and https://github.com/leanprover-community/mathlib4/issues/2727.
   let goal ← getMainGoal
   let r ← Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    if e.hasSyntheticSorry then
-      throwAbortTactic
-    let localDecl ← fvarId.getDecl
-    goal.grewrite localDecl.type e (forwardImp := true) (symm := symm) (config := config)
-  let proof := .app (r.impProof) (.fvar fvarId)
+    elabGRewrite (← getMainGoal) (← fvarId.getType) stx symm (forwardImp := true) (config := config)
+  let r ← finishElabGRewrite r
+  let proof := r.impProof.app (.fvar fvarId)
   let { mvarId, .. } ← goal.replace fvarId proof r.eNew
   replaceMainGoal (mvarId :: r.mvarIds)
 
@@ -95,7 +111,8 @@ interprets `· → ·` as a relation instead of adding the hypothesis as a side
 -/
 syntax (name := grewriteSeq) "grewrite" optConfig rwRuleSeq (location)? : tactic
 
-@[tactic grewriteSeq, inherit_doc grewriteSeq] def evalGRewriteSeq : Tactic := fun stx => do
+@[tactic grewriteSeq, inherit_doc grewriteSeq]
+public def evalGRewriteSeq : Tactic := fun stx => do
   let cfg ← elabGRewriteConfig stx[1]
   let loc := expandOptLocation stx[3]
   withRWRulesSeq stx[0] stx[2] fun symm term => do