Unable to resolve functions defined in tactic mode

Stream: mathlib4

[Mrigank Pawagi]

I am facing difficulty while unfolding functions defined using tactic mode, particularly with cases inside their definition. A dummy example is here:

import Mathlib

def myfunction (a b: ℕ) : ℕ := by

  let t₁ := a

  let t₂ := a + b

  have h : t₂ = a + b := rfl

  cases t₁ with

  | zero => exact b

  | succ n => exact t₂

theorem mytheorem (a b: ℕ) : myfunction a b = a + b := by

  unfold myfunction

  simp

  unfold Nat.casesAuxOn Nat.casesOn

  simp

  -- stuck at

  -- ⊢ Nat.rec (motive := fun x => a = x → ℕ) (fun h => b) (fun n n_ih h => a + b) a ⋯ = a + b

  sorry

How do I get rid of Nat.rec? I faced the same issue with And.rec in my actual code. Any help will be highly appreciated! I am new to Lean and still only picking up these things. Thanks! :)

[Eric Wieser]

Try cases a

[Mrigank Pawagi]

@Eric Wieser That did not change anything... Actually I must mention that I am hoping to not change myfunction at all and taking it as is.

Edit: Did you mean cases a in the theorem?

[Eric Wieser]

Yes, I mean your next step in the proof should be cases a

[Eric Wieser]

The way to simplify Nat.rec _ _ a is to turn a into 0 or succ _

[Kevin Buzzard]

Perhaps a more pertinent remark is that it is recommended that you don't use tactic mode to make definitions

[Mrigank Pawagi]

Thanks, that worked for this example, and something similar worked for my case of And.rec!

[Mrigank Pawagi]

@Kevin Buzzard thanks for your remark! I actually went and changed my function a bit to minimize the "tactic mode part" and the proof immediately became much simpler. I should keep this in mind.