Chapter 8.6 Functional Induction - simp ack is unsued

[rubydusa]

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)

theorem ack_gt_zero : ack n m > 0 := by
  fun_induction ack with
  | case1 y =>
    simp
  | case2 x ih =>
    exact ih
  | case3 x y ih1 ih2 =>
    simp [ack, *]

in case3 ack is unused. ih2 matches exactly the goal and it can also be seen in the explanation:

also:

theorem ack_gt_zero : ack n m > 0 := by
  fun_induction ack <;> simp [*, ack]

unnecessary ack