First few problems in the Lean 3 number game.

lean3-sandbox.lean

import data.real.basic

#check ℝ

open nat

-- Links:
-- * Lean 3's big math library: https://github.com/leanprover-community/mathlib
-- * Number game: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
-- * Agda's Unimath library: https://github.com/UniMath/agda-unimath
-- * Homotopy Type Theory Game: https://thehottgameguide.readthedocs.io/en/latest/index.html

-- Tutorial World 1/4
lemma example' (x y z: ℕ): x * y + z = x * y + z :=
begin
  refl,
end

-- Tutorial World 2/4
lemma example''(x y: ℕ) (h: y = x + 7): 2 * y = 2 * (x + 7) :=
begin
  rw h,
end

-- Tutorial World 3/4
lemma example''' (a b: ℕ) (h: succ a = b): succ (succ a) = succ b :=
begin
  rw h,
end

-- Tutorial World 4/4
lemma add_succ_zero' (a : ℕ) : a + succ 0 = succ a :=
begin
  rw nat.add_succ,
  rw nat.add_zero,
end

-- Addition World 1/6
lemma zero_add' (n : ℕ) : 0 + n = n :=
begin
  induction n with d hd,
  rw nat.add_zero,
  rw nat.add_succ,
  rw hd,
end

-- Addition World 2/6
lemma add_assoc' (a b c : ℕ) : (a + b) + c = a + (b + c) :=
begin
  induction c with d hd,
  repeat { rw nat.add_zero },
  repeat { rw nat.add_succ },
  rw hd,  
end

-- Addition World 3/6
lemma succ_add' (a b : ℕ) : succ a + b = succ (a + b) :=
begin
  induction b with d hd,
  repeat { rw nat.add_zero },
  repeat { rw nat.add_succ },
  rw hd,  
end

-- Addition World 4/6
lemma add_comm' (a b : ℕ) : a + b = b + a :=
begin
  induction b with d hd,
  rw nat.add_zero,
  rw zero_add',
  rw nat.add_succ,
  rw succ_add',
  rw hd,
end

-- Addition World 5/6
lemma succ_eq_add_one (n : ℕ) : succ n = n + 1 :=
begin
  simp,
end