## Stream: new members

### Topic: Tactic to collapse arithmetic on constants

#### Jason Orendorff (Jun 16 2020 at 18:52):

I'm doing this as an exercise: https://www.codewars.com/kata/5e8a8f8a18f8ed0010f55280

I'm at the point where I need to prove that ⊢ 2 ^ 2 ^ 5 + 1 = 641 * 6700417.

Is there a tactic that can finish this?

#### Kevin Buzzard (Jun 16 2020 at 18:58):

norm_num

perfect!

#### Johan Commelin (Jun 16 2020 at 19:45):

Does hint tell you that norm_num will do it?

#### Jason Orendorff (Jun 16 2020 at 21:15):

mmm, no, it times out

#### Jason Orendorff (Jun 16 2020 at 21:15):

(deterministic) timeout

#### Reid Barton (Jun 16 2020 at 21:16):

maybe it tried rfl first...

Last updated: May 13 2021 at 21:12 UTC