is it possible to "loop" the same thing?

Stream: general

[eax]

for example if I'm trying to prove lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b :=

rw zero_mul,
rw zero_mul,
rw zero_mul,
refl,```
gets the base case; but I'd really just like to say `apply zero_mul repeatedly until you can't` ?

[Bryan Gin-ge Chen]

There's tactic#repeat, (I think it may be covered later in the Natural Number Game).

[Bryan Gin-ge Chen]

I also often use simp only [zero_mul] for a bunch of repeated rewrites.

[eax]

thanks! the whole tactic library is generally useful (I was looking for it); that said if the game teaches it I'll just wait until I get there too

[eax]

in the meantime its hard enough to re-learn the basics of proofs using peano axioms while also learning lean :-p