Try this: simp only [↓reduceIte, Nat.reduceAdd]