happy function

Stream: new members

[Angela Li]

Hello again! Not really sure if I should make a new topic since I want to ask about happy numbers again. I think I might rename this topic to just "happy function" for now, unless it would be good to make a new topic? Anyways, I wanted to be able to get the ith iteration of the happy function so I have this recursive definition that I've been using to prove some small things.

def happyfunction' (p : ℕ) (b : ℕ) (n : ℕ) : ℕ → ℕ
| 0 := n
| (i+1) := happyfunction p b (happyfunction' (i))

I'm not really sure if this is the easiest to work with, so would it be better if I used something else like a stream?

Anyways (again), I am now trying to formalize https://oeis.org/A003621/a003621.pdf about 10-happy/sad numbers. I can't seem to figure out how to show ∀ (d ∈ (digits 10 n)), d ≤ 9 so then I can show that the sum of the digits squared must be less than 81*(number of digits), and then that the happy function on a 4 or more digit number results in a smaller number. Here is what I've done so far (that is probably really inefficient and messy):

lemma ten_happyfunction_lt_four_digits (n : ℕ) (H : (digits 10 n).length ≥ 4) : happyfunction 2 10 n < n
begin
  have H₁ : ∀ (d ∈ (digits 10 n)), d ≤ 9,
  intros d hd,
  unfold digits at hd,
  rw digits_aux_def at hd,
  cases hd,
  rw hd,
  have h : n%10 < 10,
  exact nat.mod_lt n (by linarith),
  linarith,
end

I wasn't sure how to deal with the list from the theorem digits_aux_def so I randomly used cases just to try and use the mod part to make some progress. Is there some tactic or way to show that every digit would be mod 10 and thus less than or equal to 9? I currently have this goal now:

case or.inr
n : ℕ,
H : (digits 10 n).length ≥ 4,
d : ℕ,
hd : list.mem d (digits_aux 10 _ (n / 10))
⊢ d ≤ 9

Hmm I tried library_search and hint but they weren't too helpful. Maybe there's some easy way that I am overlooking?
Thank you so much!