feat: nested tactic support in conv mode

src/Init/Conv.lean

@@ -31,7 +31,7 @@ syntax (name := change) "change " term : conv
 syntax (name := rewrite) "rewrite " rwRuleSeq : conv
 syntax (name := erewrite) "erewrite " rwRuleSeq : conv
 syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
-syntax (name := nestedTactic) "tactic " tacticSeq : conv
+syntax (name := nestedTactic) "tactic" " => " tacticSeq : conv
 syntax (name := nestedConv) convSeqBracketed : conv
 syntax (name := paren) "(" convSeq ")" : conv
 

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -93,6 +93,14 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 @[builtinTactic Lean.Parser.Tactic.Conv.traceState] def evalTraceState : Tactic :=
   Tactic.evalTraceState
 
+@[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
+  let seq := stx[2]
+  let target ← getMainTarget
+  if let some _ := isLHSGoal? target then
+    liftMetaTactic1 fun mvarId =>
+      replaceTargetDefEq mvarId target.mdataExpr!
+  focus <| evalTactic seq
+
 private def convTarget (conv : Syntax) : TacticM Unit := do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (evalTactic conv)

src/Lean/Expr.lean

@@ -598,6 +598,10 @@ def consumeMData : Expr → Expr
   | mdata _ e _ => consumeMData e
   | e           => e
 
+def mdataExpr! : Expr → Expr
+  | mdata _ e _ => e
+  | _           => panic! "mdata expression expected"
+
 def hasLooseBVars (e : Expr) : Bool :=
   e.looseBVarRange > 0
 

tests/lean/run/conv1.lean

@@ -41,3 +41,16 @@ example (x y : Nat) : p (x + y) (0 + y + x) := by
     skip
     done
   rfl
+
+axiom div_self (x : Nat) : x ≠ 0 → x / x = 1
+
+example (h : x ≠ 0) : x / x + x = x.succ := by
+  conv =>
+    lhs
+    arg 2
+    rw [div_self]
+    skip
+    tactic => assumption
+    done
+  show 1 + x = x.succ
+  rw [Nat.succ_add, Nat.zero_add]