How to "step in"/unfold a function defined as a match?

Stream: new members

[Kent Van Vels]

I want to prove the following lemma

theorem mnwe (xp xn yp yn : ℕ) (h0 : xp + yn = xn + yp) :
  Int.subNatNat xp xn = Int.subNatNat yp yn := by sorry

Int.subNatNat is function that constructs an Int as the signed difference of two Nats. So subNatNat 4 15 = -11 and subNatNat 15 4 = 11.

It is defined as

    Int.subNatNat m n =   match n - m with
      | 0 => Int.ofNat (m - n)
      | k.succ => Int.negSucc k

Do I have to do induction on (xp-xn)? I feel like I knew how to do this at some point but I can't find where. I appreciate any help.

[Eric Wieser]

Does

theorem mnwe (xp xn yp yn : ℕ) (h0 : xp + yn = xn + yp) :
    Int.subNatNat xp xn = Int.subNatNat yp yn := by
  unfold Int.subNatNat
  split

help?

[Kent Van Vels]

It might. I will look more into it. I can split again to get the other cases. Thanks.

[Kent Van Vels]

I was able to do it by doing a
lean4 rcases (em (xn <=xp))
and then quite a bit of tedium. But I got it. Thanks for the idea. I will think of way to make it better later.

If anyone is interested, here is the code

theorem mnwe' (xp xn yp yn : ℕ) (h0 : xp + yn = xn + yp) :
  Int.subNatNat xp xn = Int.subNatNat yp yn := by
  unfold Int.subNatNat
  rcases (em (xn ≤ xp)) with (hxnn|hxn)
  rcases (Nat.exists_eq_add_of_le hxnn) with ⟨k,hxnn'⟩
  have hynn' : yp = yn+k := by linarith
  rw [hxnn',hynn']
  have ha : xn - (xn + k) = 0 := Nat.sub_self_add xn k
  have hb : yn - (yn + k) = 0 := Nat.sub_self_add yn k
  rw [ha,hb]
  dsimp
  rw [Int.ofNat_inj]
  repeat rw [Nat.add_sub_cancel_left]
  push_neg at hxn
  rcases (Nat.exists_eq_add_of_lt) hxn with ⟨k,hxn'⟩
  rw [add_assoc,←Nat.succ_eq_add_one] at hxn'
  have hyn' : yn = yp + k.succ  := by linarith
  rw [hxn',hyn']
  have ha : xp + k.succ - xp = k.succ := Nat.add_sub_self_left xp k.succ
  have hb : yp + k.succ - yp = k.succ := Nat.add_sub_self_left yp k.succ
  rw [ha,hb]