transfer from term mode to tactic mode

Stream: general

[Huajian Xin]

For extract tactic information in metaprogramming environment I need to transfer some codes from term mode to tactic mode, but it seem to be non-trivial for some inductive proofs. For example, in data.int.basic there is a theorem

theorem div_neg : ∀ (a b : ℤ), a / -b = -(a / b)
| (m : ℕ) 0       := show of_nat (m / 0) = -(m / 0 : ℕ), by rw nat.div_zero; refl
| (m : ℕ) (n+1:ℕ) := rfl
| 0       -[1+ n] := by simp
| (m+1:ℕ) -[1+ n] := (neg_neg _).symm
| -[1+ m] 0       := rfl
| -[1+ m] (n+1:ℕ) := rfl
| -[1+ m] -[1+ n] := rfl

However, the straight transfer seems not work:
image.png

Could anyone help me with this problem? Thanks!

[Yaël Dillies]

The syntax is (annoyingly) different. You need to insert commas between different arguments in each match.

[Huajian Xin]

Thanks! I got it!

[Scott Morrison]

This has become uniform in Lean4.