simp_all_arith weakness

Stream: lean4

[Henrik Böving]

While I was writing my translation of chapter 8 CPDT to Lean I wrote the following proof for an RbTree theorem:

inductive Color
  | red : Color
  | black : Color

inductive RbTree : Color → Nat → Type
  | leaf : RbTree .black 0
  | red : RbTree .black n → Nat → RbTree .black n → RbTree .red n
  | black : RbTree c1 n → Nat → RbTree c2 n → RbTree .black n.succ

def RbTree.depth (f : Nat → Nat → Nat) : RbTree c n → Nat
  | leaf => 0
  | red t1 _ t2 => Nat.succ (f (depth f t1) (depth f t2))
  | black t1 _ t2 => Nat.succ (f (depth f t1) (depth f t2))

theorem RbTree.depth_min : ∀ c n (t : RbTree c n), n ≤ depth Nat.min t  := by
  intro c n t
  induction t with simp[depth]
  | red =>
    rw [Nat.min]
    split <;> (apply Nat.le_succ_of_le; assumption)
  | black =>
    rw [Nat.min]
    split <;> (apply Nat.succ_le_succ; assumption)

The goals I'm trying to prove after the splits are obviously quite trivial, just one lemma and an induction hypothesis away but using simp_all_arith I wasn't able to solve them, can we improve in this regard? Or is this out of scope for simp_all_arith?

[Evgeniy Kuznetsov]

@[simp]
theorem Nat.le_min_iff:
  n ≤ Nat.min m k ↔ n ≤ m ∧ n ≤ k := by
    simp only [Nat.min]
    constructor <;> intro h <;> split at * <;> simp_all
    apply Nat.le_trans <;> assumption
    apply Nat.le_trans ‹_› $ Nat.le_of_lt $ Nat.gt_of_not_le ‹_›

theorem RbTree.depth_min : ∀ c n (t : RbTree c n), n ≤ depth Nat.min t  := by
  intro c n t
  induction t <;> simp_all_arith[depth, Nat.le_succ_of_le]