How do I improve this terrible proof?

Stream: new members

[Dan Piponi]

Here's my first attempt at proving a non quite trivial theorem about numbers in Lean.

import data.set data.int.basic

def mysum : (ℕ → ℕ) → ℕ → ℕ
| f 0       := 0
| f (n + 1) := f n + mysum f n

theorem lemma1 (n : ℕ) : 2 * mysum id (n + 1) = n * (n + 1) → 2 * mysum id (n + 2) = (n + 1) * (n + 2) :=
assume h, (calc
  2 * mysum id (n + 2) = 2 * (id (n + 1) + mysum id (n + 1)) : rfl
                   ... = 2 * id (n + 1) + 2 * mysum id (n + 1) : by rw left_distrib
                   ... = 2 * id (n + 1) + n * (n + 1) : by rw h
                   ... = 2 * (n + 1) + n * (n + 1) : rfl
                   ... = 2 * n + 2 * 1 + (n * n + n * 1) : by rw [left_distrib, left_distrib, add_assoc]
                   ... = (2 * 1 + (n * n + n * 1)) + 2 * n: by rw [add_assoc, add_comm]
                   ... = n * n + n * 1 + 2 * 1 + 2 * n: by rw add_comm (2 * 1)
                   ... = n * n + 1 * n + 2 * 1 + 2 * n: by rw mul_comm n 1
                   ... = n * n + 1 * n + (2 * 1 + 2 * n): by rw add_assoc
                   ... = n * n + 1 * n + (2 * n + 2 * 1): by rw add_comm (2 * 1)
                   ... = n * n + 1 * n + (n * 2 + 1 * 2) : by rw [mul_comm n 2, mul_comm 2 1]
                   ... = (n + 1) * n + (n * 2 + 1 * 2) : by rw right_distrib
                   ... = (n + 1) * n + (n + 1) * 2 : by rw ←right_distrib
                   ... = (n + 1) * (n + 2) : by rw ←left_distrib)

theorem young_gauss : ∀ (n : ℕ), 2 * mysum id (n + 1) = n * (n + 1)
| 0 := rfl
| (n + 1) := lemma1 n (young_gauss n)

It's a bit long. What should I be learning next to improve it? Can I use the simp tactic or similar to eliminate that long calculation?

[David Renshaw]

The ring tactic can do a lot of those things automatically.

import data.set data.int.basic

import tactic.ring

def mysum : (ℕ → ℕ) → ℕ → ℕ
| f 0       := 0
| f (n + 1) := f n + mysum f n

theorem lemma1 (n : ℕ) : 2 * mysum id (n + 1) = n * (n + 1) → 2 * mysum id (n + 2) = (n + 1) * (n + 2) :=
assume h, (calc
  2 * mysum id (n + 2) = 2 * (id (n + 1) + mysum id (n + 1)) : rfl
                   ... = 2 * id (n + 1) + 2 * mysum id (n + 1) : by rw left_distrib
                   ... = 2 * id (n + 1) + n * (n + 1) : by rw h
                   ... = 2 * (n + 1) + n * (n + 1) : rfl
                   ... = (n + 1) * (n + 2) : by ring)

theorem young_gauss : ∀ (n : ℕ), 2 * mysum id (n + 1) = n * (n + 1)
| 0 := rfl
| (n + 1) := lemma1 n (young_gauss n)

[Patrick Johnson]

lemma lemma1 (n : ℕ) :
  2 * mysum id (n + 1) = n * (n + 1) →
  2 * mysum id (n + 2) = (n + 1) * (n + 2) :=
by simp_rw [mysum, id]; exact (λh, by linarith)