fix: strip hypothesis-naming metadata from proof-mode targets (#13812)

This PR fixes `mconstructor`, `mleft`, and `mright` failing inside
`mhave` blocks (#13691), and `mspecialize` failing after a `mrevert;
mintro` round trip. Both cases stem from hypothesis-naming `Expr.mdata`
leaking from hypothesis-conjunction leaves into non-leaf positions (an
inner target, or the antecedent of an `SPred.imp` target), where
downstream pattern matches did not see through it.

Fixed by stripping the mdata at the offending non-leaf positions in
`elabMHave`, `elabMReplace`, and `mRevert`.

src/Lean/Elab/Tactic/Do/ProofMode/Have.lean

@@ -54,7 +54,7 @@ def elabMHave : Tactic
     let H := hyp.toExpr
     let T := goal.target
     let (PH, hand) := SPred.mkAnd goal.u goal.σs P H
-    let haveGoal := { goal with target := H }
+    let haveGoal := { goal with target := hyp.p }
     let hhave ← elabTermEnsuringType rhs haveGoal.toExpr
     let newGoal := { goal with hyps := PH }
     let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
@@ -80,7 +80,7 @@ def elabMReplace : Tactic
     let hyp := Hyp.mk h.raw.getId uniq H'
     addHypInfo h goal.σs hyp (isBinder := true)
     let H' := hyp.toExpr
-    let haveGoal := { goal with target := H' }
+    let haveGoal := { goal with target := hyp.p }
     let hhave ← elabTermEnsuringType rhs haveGoal.toExpr
     let T := goal.target
     let (PH', hand) := SPred.mkAnd goal.u goal.σs P H'

src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean

@@ -19,11 +19,12 @@ variable {m : Type → Type u} [Monad m] [MonadControlT MetaM m] [MonadLiftT Met
 
 partial def mRevert (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → m Expr) : m Expr := do
   let res ← goal.focusHypWithInfo ref
+  let some hyp := parseHyp? res.focusHyp | liftMetaM <| throwError "impossible; res.focusHyp not a hypothesis"
   let P := goal.hyps
   let Q := res.restHyps
   let H := res.focusHyp
   let T := goal.target
-  let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp [goal.u]) goal.σs H T }
+  let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp [goal.u]) goal.σs hyp.p T }
   let prf := mkApp7 (mkConst ``Revert.revert [goal.u]) goal.σs P Q H T res.proof prf
   return prf
 

tests/elab/issue13691.lean

@@ -0,0 +1,41 @@
+import Std.Do
+import Std.Tactic.Do
+
+/-!
+Regression test for #13691: tactics that pattern-match on `MGoal.target`
+(`mconstructor`, `mleft`, `mright`) failed inside `mhave` because the inner
+goal's target carried hypothesis-naming metadata. The related round trip
+`mrevert h; mintro h; mspecialize h` failed for the symmetric reason inside
+`Revert`.
+-/
+
+open Std.Do
+
+example (P : SPred [Int]) : P ⊢ₛ P ∧ P := by
+  mintro hp
+  mhave h : spred(P ∧ P) := by
+    mconstructor
+    · mexact hp
+    · mexact hp
+  mexact h
+
+example (P : SPred [Int]) : P ⊢ₛ P ∨ P := by
+  mintro hp
+  mhave h : spred(P ∨ P) := by
+    mleft
+    mexact hp
+  mexact h
+
+example (P : SPred [Int]) : P ⊢ₛ P ∨ P := by
+  mintro hp
+  mhave h : spred(P ∨ P) := by
+    mright
+    mexact hp
+  mexact h
+
+example (P Q : SPred [Int]) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mrevert HPQ
+  mintro HPQ
+  mspecialize HPQ HP
+  mexact HPQ