10. Lean

two lean math datasets: Huggingface -> Data Studio to browse and search from Lean-Workbook and FineLeanCorpus

10.1. Games & solus

10.1.1. Natural Number Game

• This game is where you have to prove theorems about natural numbers(0,1,2,etc…). There are multiple ways to pass through the levels and there is a final boss(Fermat’s Last Theorem) is at the end of power world.

-- World: Tutorial World
-- Level 1 / 8 : The rfl tactic. example (x q : ℕ) : 37 * x + q = 37 * x + q := by
rfl
-- Level 2 / 8 : the rw tactic. example (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
rw[h]
rfl
-- Level 3 / 8 : Numbers. example : 2 = succ (succ 0) := by
rw[two_eq_succ_one]
rw[one_eq_succ_zero]
rfl
-- Level 4 / 8 : rewriting backwards. example : 2 = succ (succ 0) := by
rw[← one_eq_succ_zero, ← two_eq_succ_one]
rfl
-- Level 5 / 8 : Adding zero. example (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
rw[add_zero]
rw[add_zero]
rfl
-- Level 6 / 8 : Precision rewriting. example (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
rw[add_zero c]
rw[add_zero]
rfl
-- Level 7 / 8 : add_succ. theorem succ_eq_add_one n : succ n = n + 1 := by
rw[one_eq_succ_zero]
rw[add_succ]
rw[add_zero]
rfl
-- Level 8 / 8 : 2+2=4. example : (2 : ℕ) + 2 = 4 := by
rw[four_eq_succ_three, three_eq_succ_two, two_eq_succ_one, one_eq_succ_zero]
nth_rewrite 1[succ_eq_add_one, succ_eq_add_one]
nth_rewrite 2[succ_eq_add_one, succ_eq_add_one, succ_eq_add_one, succ_eq_add_one]
nth_rewrite 1[add_succ]
nth_rewrite 1[← succ_eq_add_one]
rw[succ_eq_add_one]
rw[succ_eq_add_one]
rw[succ_eq_add_one]
rw[← succ_eq_add_one]
rw[← succ_eq_add_one]
rw[← succ_eq_add_one]
nth_rewrite 6[succ_eq_add_one]
nth_rewrite 5[succ_eq_add_one]
nth_rewrite 1[succ_eq_add_one]
nth_rewrite 1[succ_eq_add_one]
nth_rewrite 1[succ_eq_add_one]
rw[← one_eq_succ_zero]
rfl


-- World: Addition World
-- Level 1 / 5 : zero_add. theorem zero_add (n : ℕ) : 0 + n = n := by
induction n with d hd
rw[add_zero]
rfl
rw[add_succ]
rw[hd]
rfl
-- Level 2 / 5 : succ_add. theorem succ_add (a b : ℕ) : succ a + b = succ (a + b) := by
induction b with d hd
rw[succ_eq_add_one]
rw[succ_eq_add_one]
rw[add_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[add_succ]
rw[hd]
rfl
-- Level 3 / 5 : add_comm (level boss). theorem add_comm (a b : ℕ) : a + b = b + a := by
induction a with d hd
rw[add_zero]
rw[zero_add]
rfl
rw[succ_add]
rw[add_succ]
rw[hd]
rfl
-- Level 4 / 5 : add_assoc (associativity of addition). theorem add_assoc (a b c : ℕ) : a + b + c = a + (b + c) := by
induction c with d hd
rw[add_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[add_succ]
rw[add_succ]
rw[hd]
rfl
-- Level 5 / 5 : add_right_comm. theorem add_right_comm (a b c : ℕ) : a + b + c = a + c + b := by
induction a with d hd
rw[zero_add]
rw[zero_add]
rw[add_comm]
rfl
rw[succ_add]
rw[succ_add]
rw[succ_add]
rw[succ_add]
rw[hd]
rfl


-- World: Multiplication World
-- Level 1 / 9 : mul_one. theorem mul_one (m : ℕ) : m * 1 = m := by
rw[one_eq_succ_zero]
rw[mul_succ]
rw[mul_zero]
rw[zero_add]
rfl
-- Level 2 / 9 : zero_mul. theorem zero_mul (m : ℕ) : 0 * m = 0 := by
induction m with d hd
rw[mul_zero]
rfl
rw[mul_succ]
rw[hd]
rw[add_zero]
rfl
-- Level 3 / 9 : succ_mul. theorem succ_mul (a b : ℕ) : succ a * b = a * b + b := by
induction b with d hd
rw[mul_zero]
rw[mul_zero]
rw[add_zero]
rfl
rw[mul_succ]
rw[hd]
nth_rewrite 1[succ_eq_add_one]
rw[← add_assoc]
rw[mul_succ]
rw[succ_eq_add_one]
rw[← add_assoc]
nth_rewrite 2[add_right_comm]
rfl
-- Level 4 / 9 : mul_comm. theorem mul_comm (a b : ℕ) : a * b = b * a := by
induction a with d hd
rw[mul_zero]
rw[zero_mul]
rfl
rw[mul_succ]
rw[succ_mul]
rw[hd]
rfl
-- Level 5 / 9 : one_mul. theorem one_mul (m : ℕ): 1 * m = m := by
rw[mul_comm]
rw[mul_one]
rfl
-- Level 6 / 9 : two_mul. theorem two_mul (m : ℕ): 2 * m = m + m := by
rw[two_eq_succ_one]
rw[succ_mul]
rw[one_mul]
rfl
-- Level 7 / 9 : mul_add. theorem mul_add (a b c : ℕ) : a * (b + c) = a * b + a * c := by
induction c with d hd
rw[add_zero]
rw[mul_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[mul_succ]
rw[hd]
rw[mul_succ]
rw[add_assoc]
rfl
-- Level 8 / 9 : add_mul. theorem add_mul (a b c : ℕ) : (a + b) * c = a * c + b * c := by
rw[mul_comm]
nth_rewrite 2[mul_comm]
nth_rewrite 3[mul_comm]
rw[mul_add]
rfl
-- Level 9 / 9 : mul_assoc. theorem mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c) := by
induction a with d hd
rw[zero_mul]
rw[zero_mul]
rw[zero_mul]
rfl
nth_rewrite 2[succ_mul]
rw[← hd]
rw[succ_mul]
rw[add_mul]
rfl


-- World: Implication World
-- Level 1 / 11 : The `exact` tactic
exact h1
-- Level 2 / 11 : `exact` practice.
rw[zero_add] at h
rw[zero_add] at h
exact h
-- Level 3 / 11 : The `apply` tactic.
apply h2 at h1
exact h1
-- Level 4 / 11 : succ_inj : the successor function is injective. example (x : ℕ) (h : x + 1 = 4) : x = 3 := by
rw[four_eq_succ_three] at h
rw[← succ_eq_add_one] at h
apply succ_inj at h
exact h
-- Level 5 / 11 : Arguing backwards. example (x : ℕ) (h : x + 1 = 4) : x = 3 := by
apply succ_inj
rw[succ_eq_add_one]
rw[← four_eq_succ_three]
exact h
-- Level 6 / 11 : intro
intro h
exact h
-- Level 7 / 11 : intro practice
intro h
rw[← succ_eq_add_one] at h
rw[← succ_eq_add_one] at h
apply succ_inj at h
exact h
-- Level 8 / 11 : ≠
apply h2 at h1
exact h1
-- Level 9 / 11 : zero_ne_succ
intro h
rw[one_eq_succ_zero] at h
apply zero_ne_succ at h
exact h
-- Level 10 / 11 : 1 ≠ 0
intro h
symm at h
apply zero_ne_one at h
exact h
-- Level 11 / 11 : 2 + 2 ≠ 5
intro h
rw[add_succ] at h
apply succ_inj at h
rw[succ_add] at h
apply succ_inj at h
rw[add_succ] at h
apply succ_inj at h
rw[succ_add] at h
apply succ_inj at h
rw[zero_add] at h
rw[succ_eq_add_one] at h
rw[zero_add] at h
apply zero_ne_one at h
exact h


-- World: Power World
-- Level 1 / 10 : zero_pow_zero. theorem zero_pow_zero : (0 : ℕ) ^ 0 = 1 := by
rw[pow_zero]
rfl
-- Level 2 / 10 : zero_pow_succ. theorem zero_pow_succ (m : ℕ) : (0 : ℕ) ^ (succ m) = 0 := by
rw[pow_succ]
rw[mul_zero]
rfl
-- Level 3 / 10 : pow_one. theorem pow_one (a : ℕ) : a ^ 1 = a := by
rw[one_eq_succ_zero]
rw[pow_succ]
rw[pow_zero]
rw[one_mul]
rfl
-- Level 4 / 10 : one_pow. theorem one_pow (m : ℕ) : (1 : ℕ) ^ m = 1 := by
induction m with d hd
rw[pow_zero]
rfl
rw[pow_succ, hd]
rw[mul_one]
rfl
-- Level 5 / 10 : pow_two. theorem pow_two (a : ℕ) : a ^ 2 = a * a := by
rw[two_eq_succ_one, pow_succ]
rw[pow_one]
rfl
-- Level 6 / 10 : pow_add. theorem pow_add (a m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n := by
induction m with d hd
rw[zero_add]
rw[pow_zero]
rw[one_mul]
rfl
rw[succ_add]
rw[pow_succ]
rw[hd]
rw[pow_succ]
nth_rewrite 1[mul_comm]
nth_rewrite 4[mul_comm]
rw[mul_assoc]
rfl
-- Level 7 / 10 : mul_pow. theorem mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by
induction n with d hd
repeat rw[pow_zero]
rw[mul_one]
rfl
repeat rw[pow_succ]
rw[hd]
rw[← mul_assoc]
rw[← mul_assoc]
nth_rewrite 5[mul_comm]
nth_rewrite 3[mul_comm]
rw[← mul_assoc]
rfl
-- Level 8 / 10 : pow_pow. theorem pow_pow (a m n : ℕ) : (a ^ m) ^ n = a ^ (m * n) := by
induction n with d hd
rw[mul_zero]
repeat rw[pow_zero]
rfl
rw[pow_succ]
rw[hd]
rw[mul_succ]
rw[←pow_add]
rfl
-- Level 9 / 10 : add_sq. theorem add_sq (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
induction b with d hd
simp[add_zero,mul_zero,two_eq_succ_one,zero_pow_succ]
simp[hd,mul_pow,one_pow,pow_add,pow_one,pow_pow,pow_succ,pow_two,pow_zero,zero_pow_succ,zero_pow_zero,add_mul,mul_add,mul_assoc,mul_comm,mul_one,mul_succ,mul_zero,one_mul,succ_mul,two_mul,zero_mul,add_assoc,add_comm,add_right_comm,add_succ,succ_eq_add_one,add_zero,zero_add,succ_add]
repeat rw[←add_assoc]
repeat rw[mul_comm a 2,two_mul]
rw[←add_assoc]
rw[←two_mul]
rw[mul_comm 2 a]
rw[←mul_assoc d a 2]
rw[two_eq_succ_one]
rw[mul_succ]
rw[←add_assoc]
rw[mul_one]
repeat rw[←pow_two]
repeat rw[mul_comm a d]
nth_rewrite 3[add_comm]
repeat rw[←add_assoc]
nth_rewrite 15[add_comm]
repeat rw[←add_assoc]
nth_rewrite 1[add_comm]
repeat rw[←add_assoc]
nth_rewrite 13[add_comm]
repeat rw[←add_assoc]
nth_rewrite 3[add_comm]
repeat rw[←add_assoc]
nth_rewrite 4[add_comm]
repeat rw[←add_assoc]
nth_rewrite 9[add_comm]
repeat rw[←add_assoc]
nth_rewrite 9[add_comm]
repeat rw[←add_assoc]
nth_rewrite 9[add_comm]
repeat rw[←add_assoc]
nth_rewrite 9[add_comm]
repeat rw[←add_assoc]
nth_rewrite 9[add_comm]
repeat rw[←add_assoc]
nth_rewrite 9[add_comm]
repeat rw[←add_assoc]
nth_rewrite 3[add_comm]
repeat rw[←add_assoc]
nth_rewrite 3[add_comm]
repeat rw[←add_assoc]
nth_rewrite 1[add_comm]
repeat rw[←add_assoc]
nth_rewrite 1[add_comm]
repeat rw[←add_assoc]
rfl
-- Level 10 / 10 : Fermat's Last Theorem
xyzzy


-- World: Advanced Addition World
-- Level 1 / 6 : add_right_cancel. theorem add_right_cancel (a b n : ℕ) : a + n = b + n → a = b := by
induction n with d hd
rw[add_zero]
rw[add_zero]
intro h
exact h
intro h
rw[add_succ] at h
rw[add_succ] at h
apply succ_inj at h
apply hd at h
exact h
-- Level 2 / 6 : add_left_cancel. theorem add_left_cancel (a b n : ℕ) : n + a = n + b → a = b := by
rw[add_comm]
nth_rewrite 2[add_comm]
apply add_right_cancel
-- Level 3 / 6 : add_left_eq_self. theorem add_left_eq_self (x y : ℕ) : x + y = y → x = 0 := by
induction y with d hd
rw[add_zero]
intro h
exact h
rw[add_succ]
intro h
apply succ_inj at h
apply hd at h
exact h
-- Level 4 / 6 : add_right_eq_self. theorem add_right_eq_self (x y : ℕ) : x + y = x → y = 0 := by
rw[add_comm]
apply add_left_eq_self
-- Level 5 / 6 : add_right_eq_zero. theorem add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
cases b with d
rw[add_zero]
intro h
exact h
rw[add_succ]
intro h
apply succ_ne_zero at h
cases h
-- Level 6 / 6 : add_left_eq_zero. theorem add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0 := by
cases a with d
rw[zero_add]
intro h
exact h
rw[succ_add]
intro h
apply succ_ne_zero at h
cases h


-- World: Algorithm World
-- Level 1 / 9 : add_left_comm. theorem add_left_comm (a b c : ℕ) : a + (b + c) = b + (a + c) := by
rw[add_comm]
rw[← add_assoc]
rw[add_right_comm]
rfl
-- Level 2 / 9 : making life easier. example (a b c d : ℕ) : a + b + (c + d) = a + c + d + b := by
repeat rw[add_assoc]
rw[add_left_comm b c]
rw[add_comm b d]
rfl
-- Level 3 / 9 : making life simple. example (a b c d e f g h : ℕ) : (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h := by
simp only [add_assoc, add_left_comm, add_comm]
Level 4 / 9 : the simplest approach. example (a b c d e f g h : ℕ) : (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h := by
simp only [add_assoc, add_left_comm, add_comm]
-- Level 5 / 9 : pred. example (a b : ℕ) (h : succ a = succ b) : a = b := by
rw[← pred_succ a]
rw[h]
rw[pred]
rfl
-- Level 6 / 9 : is_zero. theorem succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
intro h
rw[← is_zero_succ a]
rw[h]
trivial
-- Level 7 / 9 : An algorithm for equality. theorem succ_ne_succ (m n : ℕ) (h : m ≠ n) : succ m ≠ succ n := by
contrapose! h
apply succ_inj at h
exact h
-- Level 8 / 9 : decide. example : (20 : ℕ) + 20 = 40 := by
decide
-- Level 9 / 9 : decide again. example : (2 : ℕ) + 2 ≠ 5 := by
decide


-- World: ≤ World
-- Level 1 / 11 : The `use` tactic. theorem le_refl (x : ℕ) : x ≤ x := by
use 0
rw[add_zero]
rfl
-- Level 2 / 11 : 0 ≤ x
use x
rw[zero_add]
rfl
-- Level 3 / 11 : x ≤ succ x. theorem le_succ_self (x : ℕ) : x ≤ succ x := by
use 1
rw[succ_eq_add_one]
rfl
-- Level 4 / 11 : x ≤ y and y ≤ z implies x ≤ z. theorem le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
cases hxy with a ha
cases hyz with b hb
use a+b
rw[← add_assoc]
rw[ha] at hb
exact hb
-- Level 5 / 11 : x ≤ 0 → x = 0. theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by
cases hx with a ha
symm at ha
apply add_right_eq_zero at ha
exact ha
-- Level 6 / 11 : x ≤ y and y ≤ x implies x = y. theorem le_antisymm (x y : ℕ) (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
cases hxy with d hd
cases hyx with a ha
rw[ha,add_assoc] at hd
symm at hd
apply add_right_eq_self at hd
apply add_right_eq_zero at hd
rw[hd,add_zero] at ha
exact ha
-- Level 7 / 11 : Dealing with `or`. example (x y : ℕ) (h : x = 37 ∨ y = 42) : y = 42 ∨ x = 37 := by
cases h with hx hy
right
exact hx
left
exact hy
-- Level 8 / 11 : x ≤ y or y ≤ x. theorem le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by

10.1.2. Robo

World	key mathematical content	Lean tactics introduced	Boss level
Logo	propositional logic: ∧, ∨, ¬	rfl, left, right,tauto, …	–
Implis	propositional logic: ⇒, ⇔	apply, intro, revert, rw, …	A ⇒ B equivalent to ¬ A ∨ B
Saturn	elementary arithmetic, polynomials	ring, rw for equations	a well-known polynomial sums-of-squares formula
Quantus	predicate logic, even/odd numbers	use, obtain, decide, push_neg	Drinker’s paradox
Luna	inequalities	linarith, omega	–
Spinoza	proof structuring	suffices, by_contra, contrapose	–
Babylon	∑ notation, induction	induction'	sum of cubes
Piazza	basic set theory	ext, simp	–
Prado	prime numbers	–	exactly one even prime
Euklid	∏ notation	–	infinitely many primes
Vieta	maps (between types)	funext	another induction exercise
Epo	surjective maps, axiom of choice	choose	map surjective ⇔ has right inverse
Mono	injective maps	–	map injective ⇔ has left inverse
Iso	bijective maps	–	map bijective ⇔ has inverse
Samarkand	(pre)images of subsets	–	map surjective ⇔ induced contravariant map on powersets injective
Cantor	fixed points of maps	–	ℕ-valued sequences uncountable
Robotswana	matrices, trace	–	characterization of trace map
Ciao	(good-bye planet)	–	–

10.1.3. Set Theory Game

-- World: Subset World
-- Level 1 / 6 : The exact tactic. Suppose that x∈A. Then x∈A.
exact h
-- Level 2 / 6 : A subset hypothesis. Suppose A and B are sets, A⊆B, and x∈A. Then x∈B.
exact h1 h2
-- Level 3 / 6 : The have tactic. example (x : U) (A B C : Set U) (h1 : A ⊆ B) (h2 : B ⊆ C) (h3 : x ∈ A) : x ∈ C := by
have h4:x∈B:=h1 h3
exact h2 h4
-- Level 4 / 6 : Implication. example {x : U} {A B C : Set U} (h1 : A ⊆ B) (h2 : x ∈ B → x ∈ C) : x ∈ A → x ∈ C := by
intro h3
have h4:=h1 h3
have h5:=h2 h4
exact h5
-- Level 5 / 6 : Subset is reflexive. theorem Subset.refl (A : Set U) : A ⊆ A := by
intro h
intro g
exact g
-- Level 6 / 6 : Subset is transitive. theorem Subset.trans {A B C : Set U} (h1 : A ⊆ B) (h2 : B ⊆ C) : A ⊆ C := by
intro x
intro h3
have h4:=h1 h3
have h5:=h2 h4
exact h5

-- World: Complement World
-- Level 1 / 5 : Proof by contradiction. example {A B : Set U} {x : U} (h1 : x ∈ A) (h2 : x ∉ B) : ¬A ⊆ B := by
by_contra h3
have h4:=h3 h1
exact h2 h4
-- Level 2 / 5 : Definition of complement. theorem mem_compl_iff (A : Set U) (x : U) : x ∈ Aᶜ ↔ x ∉ A := by
rfl
-- Level 3 / 5 : Complement subsets from subsets. theorem compl_subset_compl_of_subset {A B : Set U} (h1 : A ⊆ B) : Bᶜ ⊆ Aᶜ := by
intro x h2
rw[mem_compl_iff A x]
rw[mem_compl_iff] at h2
by_contra
have h3:=h1 a
exact h2 h3
-- Level 4 / 5 : Complement of a complement.theorem compl_compl (A : Set U) : Aᶜᶜ = A := by
apply Subset.antisymm
intro h
intro g
rw[mem_compl_iff] at g
rw[mem_compl_iff] at g
push_neg at g
exact g
intro h
intro g
rw[mem_compl_iff]
rw[mem_compl_iff]
push_neg
exact g
-- Level 5 / 5 : Complement subsets equivalence. example (A B : Set U) : A ⊆ B ↔ Bᶜ ⊆ Aᶜ := by
apply Iff.intro
intro h
exact compl_subset_compl_of_subset h
intro h
apply compl_subset_compl_of_subset at h
rewrite[compl_compl,compl_compl] at h
exact h

-- World: Intersection World
-- Level 1 / 8 : And. example (x : U) (A B : Set U) (h : x ∈ A ∧ x ∈ B) : x ∈ A := by
exact h.left
-- Level 2 / 8 : Element of an intersection. example (x : U) (A B : Set U) (h : x ∈ A ∩ B) : x ∈ B := by
rw[mem_inter_iff] at h
exact h.right
-- Level 3 / 8 : Intersection is a subset. example (A B : Set U) : A ∩ B ⊆ A := by
intro x
intro h
rw[mem_inter_iff] at h
exact h.left
-- Level 4 / 8 : Proving a conjunction. example (x : U) (A B : Set U) (h1 : x ∈ A) (h2 : x ∈ B) : x ∈ A ∩ B := by
constructor
exact h1
exact h2
-- Level 5 / 8 : Subset of an intersection. example (A B C : Set U) (h1 : A ⊆ B) (h2 : A ⊆ C) : A ⊆ B ∩ C := by
intro x
intro h
constructor
exact h1 h
exact h2 h
-- Level 6 / 8 : Intersection subset of swap. theorem inter_subset_swap (A B : Set U) : A ∩ B ⊆ B ∩ A := by
intro x
intro h
rw[mem_inter_iff] at h
exact And.intro h.right h.left
-- Level 7 / 8 : Intersection is commutative. theorem inter_comm (A B : Set U) : A ∩ B = B ∩ A := by
apply Subset.antisymm
exact inter_subset_swap A B
exact inter_subset_swap B A
-- Level 8 / 8 : Intersection is associative. theorem inter_assoc (A B C : Set U) : (A ∩ B) ∩ C = A ∩ (B ∩ C) := by
ext x
constructor
intro h
constructor
exact h.left.left
constructor
exact h.left.right
exact h.right
intro h
constructor
constructor
exact h.left
exact h.right.left
exact h.right.right

-- World: Union World
-- Level 1 / 6 : Or. example (x : U) (A B : Set U) (h : x ∈ A) : x ∈ A ∨ x ∈ B := by
exact Or.inl h
-- Level 2 / 6 : Subset of a union. example (A B : Set U) : B ⊆ A ∪ B := by
intro x
intro h
exact Or.inr h
-- Level 3 / 6 : Proof by cases. example (A B C : Set U) (h1 : A ⊆ C) (h2 : B ⊆ C) : A ∪ B ⊆ C := by
intro x
intro h
rcases h
exact h1 h
exact h2 h
-- Level 4 / 6 : Union subset of swap. theorem union_subset_swap (A B : Set U) : A ∪ B ⊆ B ∪ A := by
intro x
intro h
rcases h
exact Or.inr h
exact Or.inl h
-- Level 5 / 6 : Union is commutative. theorem union_comm (A B : Set U) : A ∪ B = B ∪ A := by
apply Subset.antisymm
exact union_subset_swap A B
exact union_subset_swap B A
-- Level 6 / 6 : Union is associative. theorem union_assoc (A B C : Set U) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := by
ext x
constructor
intro h
rcases h
rcases h
left
exact h
right
left
exact h
right
right
exact h
intro h
rcases h
left
left
exact h
rcases h
left
right
exact h
right
exact h

10.1.4. Lean Intro to Logic

• This game teaches you how to solve logic puzzles.

• There are two types of worlds.

  • Normal Worlds : These teach you how to use the exact and have(and rw, in \(\iff\) world) tactic and theorems to complete the levels.

    • To create implications, use \(\lambda\)(fun) to prove them.

  • Redux Worlds : These how copies of the other worlds but you have to use different tactics to complete the levels.

    • Here for implications, you just use apply and intro tactics.

-- World: ∧ Tutorial: Party Invites
-- Level 1 / 8 : Exactly! It's in the premise. Exhibit evidence that you're planning a party. example (P : Prop)(todo_list : P) : P := by
exact todo_list
-- Level 2 / 8 : And Introduction. example (P S : Prop)(p: P)(s : S) : P ∧ S := by
exact and_intro p s
-- Level 3 / 8 : The Have Tactic. example (A I O U : Prop)(a : A)(i : I)(o : O)(u : U) : (A ∧ I) ∧ O ∧ U := by
have ai:=and_intro a i
have ou:=and_intro o u
exact and_intro ai ou
-- Level 4 / 8 : And Elimination. example (P S : Prop)(vm: P ∧ S) : P := by
have p:=vm.left
exact p
-- Level 5 / 8 : And Elimination. example (P Q : Prop)(h: P ∧ Q) : Q := by
have a:=h.right
exact a
-- Level 6 / 8 : Mix and Match. example (A I O U : Prop)(h1 : A ∧ I)(h2 : O ∧ U) : A ∧ U := by
exact and_intro h1.left h2.right
-- Level 7 / 8 : More Elimination. example (C L : Prop)(h: (L ∧ (((L ∧ C) ∧ L) ∧ L ∧ L ∧ L)) ∧ (L ∧ L) ∧ L) : C := by
have h_1:=h.left
have h_2:=h_1.right
have h_3:=h_2.left
have h_4:=h_3.left
have h_5:=h_4.right
exact h_5
-- Level 8 / 8 : Rearranging Boxes. example (A C I O P S U : Prop)(h: ((P ∧ S) ∧ A) ∧ ¬I ∧ (C ∧ ¬O) ∧ ¬U) : A ∧ C ∧ P ∧ S := by
have a:=h.left.right
have c:=h.right.right.left.left
have ps:=h.left.left
exact and_intro a (and_intro c ps)

-- World2: → Tutorial: Party Snacks
-- Level 1 / 9 : Cake Delivery Service. example (P C: Prop)(p: P)(bakery_service : P → C) : C := by
have a:=bakery_service p
exact a
-- Level 2 / 9 : Identity. example (C: Prop) : C → C := by
exact λ C ↦ C
-- Level 3 / 9 : Cake Form Swap. example (I S: Prop) : I ∧ S → S ∧ I := by
exact λ h : I ∧ S ↦ and_intro (and_right h) h.left
-- Level 4 / 9 : Chain Reasoning. example (C A S: Prop) (h1 : C → A) (h2 : A → S) : C → S := by
exact h2∘h1
-- Level 5 / 9 : Riffin Snacks. example (P Q R S T U: Prop) (p : P) (h1 : P → Q) (h2 : Q → R) (h3 : Q → T) (h4 : S → T) (h5 : T → U) : U := by
have h6:P→T:=h1≫h3
have h7:P→U:=h6≫h5
exact h7 p
-- Level 6 / 9 : and_imp. example (C D S: Prop) (h : C ∧ D → S) : C → D → S := by
exact λ c d ↦ h (and_intro c d)
-- Level 7 / 9 : and_imp2. example (C D S: Prop) (h : C → D → S) : C ∧ D → S := by
exact λ cd ↦ h cd.left cd.right
-- Level 8 / 9 : Distribute. example (C D S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by

10.1.5. Knights and Knaves Game

• This teachs you how to solve logic puzzles where you have to deduce who is a knight(truthteller) and who is a knave(liar).

-- World: Equational Reasoning
-- 1, A Number Equals Itself
rfl
-- 2, goal is true by assumption
exact h
-- 3, Substituting Variables By Their Values
rw[h]
rw[g]
-- 4, Divide both sides of an equation
exact Nat.mul_left_cancel four_pos h

-- World: Logic
-- 1, Intro
exact hP
-- 2, And, `∧`
constructor
assumption
assumption
-- 3, Or, `∨`
left
assumption
-- 4, Implication, `→`
exact hP
-- 5, Proving an implication, Implication as the goal
intro h
assumption
-- 6, Proof by `cases`
cases h
exact hPR h_1
exact hQR h_1
-- 7, Logical Equivalence, `↔`
exact PsameQ.mp hP
-- 8, Not Connective, ¬
unfold Not at hnP
exact hnP hP
-- 9, From `False`, anything follows.
contradiction
-- 10, `have`
have hQ:Q:=hPQ hP
exact hQR hQ
-- 11, `have` with `exact`
have hQ:Q:=hPQ hP
exact hQR hQ

-- World: Simplification
-- 1, `or_false`
simp[hnQ] at h
assumption
-- 2,
simp[h]
-- 3, `not_or`
simp[not_or] at h
assumption
-- 4, `not_and_or`
simp[←not_and_or]
simp[not_and_or] at h
assumption
-- 5, `by_contra`, `not_not`
simp[not_not] at hP
assumption

10.2. Tactics & Theorems

Categorize tactics by

• manipulate the goal

• manipulate the assumptions

• manipulate both/either

Tactics

• apply : This tactic applies theorems and assumptions at assumptions. This tactic is similar to rw.

• assumption : Searches for assumptions that can directly prove the goal.

• cases : Considers the cases for and & or statements and objects(similar to induction but without hypothesis).

• contradiction : This tactic proves statements that cannot be proved using other methods.

• decide : This tactic tries to solve goals by using algorithms.

• exact : Proves goals based on the theorems and assumptions written after it.

• have : Introduces an assumption that can be proved based on evidence(providing evidence to prove it is optional when using tactic).

• induction : Uses induction to prove the goal by considering base case then using a hypothesis to prove the other part.

• intro : Introduces a hypothesis(assumption) based on the goal if possible(similar to fun(\(\lambda\))).

• left : The goal or hypothesis changes from A or B to A(because A is on the left).

• revert : This is the opposite of intro.

• right : The goal or hypothesis changes from A or B to B(because B is on the right).

• rfl(reflexitivity) : This tactic proves all goals of the form \(X=X\)

• rw(rewrite) : This rewrites the goal.

  • Square brackets must be included.

  • Type the theorem in the square brackets.

  • By typing nth_rw (number), this tactic only rewrites the nth place where you can use the theorem or assumption.

• simp : This uses other tactics to try and simplify the goal or hypothesis.

• symm : \(a=b\) implies \(b=a\)

• tauto : This tactic proves all logic statements.

• trivial : This tactic proves goals of the form True.

• use : This tactic replaces the object after the \(\exist\)(exist symbol) with another object or number when there is an \(\exist\) in the proof.

Theorems

• add_assoc : \((a+b)+c=a+(b+c)\quad\)(In Lean, \(a+b+c\) means \((a+b)+c\).)

• add_comm : \(a+b=b+a\)

• add_succ : \(a+succ(b)=succ(a+b)\)

• add_zero : \(a+0=a\)

• mul_zero : \(a*0=0\)

• not_not : \(\neg\neg A=A\)

• one_ne_zero : \(1\ne0\)

• pow_one : \(a^1=a\)

• pow_two : \(a^2=a*a\)

• pow_zero : \(a^0=1\)

• succ_add : \(succ(a)+b=succ(a+b)\)

• succ_eq_add_one : \(succ(n)=n+1\)

• zero_add : \(0+a=a\)

• zero_mul : \(0*a=0\)

• zero_ne_one : \(0\ne1\)

• zero_pow_succ : \(0^n=0\quad\)(Where n is a successor(\(n\gt0\)).)

• zero_pow_zero : \(0^0=1\quad\)(In Lean, \(0^0\) is not undefined.)