feat: `simp_intro` tactic

[digama0]

trafficstars

The simp_intro tactic is a combination of simp and intro: it will simplify the types of variables as it introduces them and uses the new variables to simplify later arguments and the goal.

example : x + 0 = y → x = z := by
  simp_intro h
  -- h: x = y ⊢ y = z
  sorry