使用LeanProver消除等式公共常数的自动化命令咨询

我需要证明以下目标：

n_n: ℕ
n_ih: n_n * (n_n + 1) / 2 = arith_sum n_n
⊢ (n_n + 1) * (n_n + 1 + 1) / 2 = n_n + 1 + n_n * (n_n + 1) / 2 

尝试过ring、simp、linarith命令均无效，用calc步骤又过于冗长。请问是否存在可自动消除等式中公共常数的命令？

内容的提问来源于stack exchange，提问作者ksmzzang2003