proving a + a = 2* a

Stream: new members

[Atze van der Ploeg]

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]

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

[Chris Hughes]

There's a lemma nat.mul_succ

[Rob Lewis]

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

[Chris Hughes]

Sorry, nat.succ_mul

[Rob Lewis]

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]

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

[Kenny Lau]

well I imagined he would do induction on n

[Atze van der Ploeg]

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]

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

[Mark Dickinson]

There's also two_mul in the standard library:

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