Pattern match with equation of the original variables?

Stream: new members

[Shanghe Chen]

Hi in the following code, how can I get an equation like h?

import Mathlib.Tactic
namespace Ex1

example (a b : ℕ) : ∃ (c : ℕ), (Int.negSucc b = Int.ofNat c - Int.ofNat a) ∨ (Int.negSucc b = Int.negSucc c - Int.ofNat a) := by
match (Int.ofNat a + Int.negSucc b) with
| Int.ofNat c =>
  constructor
  case w => exact c
  have h : Int.ofNat a + Int.negSucc b = Int.ofNat c := rfl
| Int.negSucc c => sorry

end Ex1

[Kyle Miller]

Try match h : (Int.ofNat a + Int.negSucc b) with

[Kyle Miller]

(those parentheses aren't necessary by the way)

[Shanghe Chen]

It works! Thank you very much Kyle :tada:

[Shanghe Chen]

This match h: syntax seems not mentioned in both TPIL and MIL. Maybe we should add an example for it in TPIL? It seems quite useful sometimes:smiling_face: