feat: in modifier at conv tactic

It is just a macro for `pattern`

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

@@ -134,10 +134,9 @@ private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := w
 
 @[builtinTactic Lean.Parser.Tactic.Conv.conv] def evalConv : Tactic := fun stx => do
   match stx with
-  | `(tactic| conv $[at $loc?]? $[in $e?]? => $code) =>
-    -- TODO: implement `at` support
-    unless e?.isNone do
-      throwError "'in' modifier has not been implemented yet"
+  | `(tactic| conv $[at $loc?]? in $p => $code) =>
+    evalTactic (← `(tactic| conv $[at $loc?]? => pattern $p; ($code:convSeq)))
+  | `(tactic| conv $[at $loc?]? => $code) =>
     if let some loc := loc? then
       convLocalDecl code loc.getId
     else

tests/lean/run/conv1.lean

@@ -86,3 +86,20 @@ example (h₁ : f x = x + 1) (h₂ : x > 0) : f x = f x := by
     rhs
     simp [f, h₂]
   exact h₁
+
+example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f z z = z) (h₂ : ∀ x y, f (g x) (g y) = y) : f (g (0 + y)) (f (g x) (g (x + 0))) = x := by
+  conv in _ + 0 => apply Nat.add_zero
+  traceState
+  conv in 0 + _ => apply Nat.zero_add
+  traceState
+  simp [h₁, h₂]
+
+example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
+        (h₁ : ∀ z, f z z = z) (h₂ : ∀ x y, f (g x) (g y) = y)
+        (h₃ : f (g (0 + x)) (g x) = 0)
+ : g x = 0 := by
+  conv at h₃ in 0 + x => apply Nat.zero_add
+  traceState
+  conv at h₃ => lhs; apply h₁
+  traceState
+  assumption