## Stream: new members

### Topic: proving a + a = 2* a

#### Atze van der Ploeg (Jan 11 2019 at 10:53):

I'm trying to prove the shocking lemma ∀ n : ℕ, n + n = 2*n , how do i tell lean to unfold the definition of *?

#### Kenny Lau (Jan 11 2019 at 10:59):

you don't; you just tell Lean what you want it to unfold to

#### Chris Hughes (Jan 11 2019 at 10:59):

There's a lemma nat.mul_succ

#### Rob Lewis (Jan 11 2019 at 11:00):

You can use simp only [(*)]. This will unfold the notation, then you'll have to deal with the definition nat.mul.

#### Chris Hughes (Jan 11 2019 at 11:00):

Sorry, nat.succ_mul

#### Rob Lewis (Jan 11 2019 at 11:00):

You can unfold that with the same method, or unfold nat.mul, but since it's defined by recursion on n, you'll have to use induction first.

#### Chris Hughes (Jan 11 2019 at 11:01):

You can't actually unfold multiplication in this scenario, since it's defined by recursion on the second argument.

#### Kenny Lau (Jan 11 2019 at 11:01):

well I imagined he would do induction on n

#### Atze van der Ploeg (Jan 11 2019 at 12:05):

Thanks, nat.succ_mul works fine, or using mul_comm but this requires me to know that nat.mul is defined by recursively on the second argument.

#### Kevin Buzzard (Jan 11 2019 at 12:23):

You can just use the 'ring' tactic if you don't care about what the low level proof looks like

#### Mark Dickinson (Jan 11 2019 at 18:40):

There's also two_mul in the standard library:

two_mul : ∀ {α : Type u_1} [_inst_1 : semiring α] (n : α), 2 * n = n + n


Last updated: May 13 2021 at 18:26 UTC