## Stream: general

### Topic: is it possible to "loop" the same thing?

#### eax (Feb 28 2021 at 01:58):

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 (Feb 28 2021 at 02:01):

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

#### Bryan Gin-ge Chen (Feb 28 2021 at 02:01):

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

#### eax (Feb 28 2021 at 02:03):

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 (Feb 28 2021 at 02:03):

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

Last updated: May 18 2021 at 16:25 UTC