power world level 8 in 19 rewrites

Stream: new members

[Nicolas Tessore]

not sure if this is a thing, but the text mentions a record of 25... I guess it could be reduced more

rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw add_assoc,
rw succ_mul,
rw one_mul,
rw add_comm (b*b),
rw ← add_assoc,
rw add_mul a a b,
rw ← add_assoc,
rw ← mul_add,
rw add_assoc,
rw ← add_mul,
rw mul_comm a,
rw ← mul_add,
refl,

[Kevin Buzzard]

Nice :-) is there an issue where someone claims to have solved it in even fewer?

[Thomas Browning]

Here's one less:

rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw succ_mul,
rw one_mul,
rw mul_add,
rw add_mul,
rw add_mul,
rw add_mul,
rw add_assoc,
rw add_assoc,
rw add_comm (b * b),
rw add_assoc,
rw mul_comm a b,
refl,

[Thomas Browning]

Looks like you can get down to 17 with add_right_comm:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/function.20with.20random.20definition/near/202661258
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/function.20with.20random.20definition/near/225697465