diff --git a/src/theorem-proving-in-lean/exercises-2.lean b/src/theorem-proving-in-lean/exercises-2.lean
index c5e1aac..f3ecacd 100644
--- a/src/theorem-proving-in-lean/exercises-2.lean
+++ b/src/theorem-proving-in-lean/exercises-2.lean
@@ -1,43 +1,33 @@
-/- Exercises 2.10
+/- Exercises 2
  -
  - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
--- Borrowed from the book.
-def double (x : ℕ) : ℕ := x + x
-def do_twice (f : ℕ → ℕ) (x : ℕ) : ℕ := f (f x)
-
 -- Exercise 1
 --
 -- Define the function `Do_Twice`, as described in Section 2.4.
-section ex_1
-def Do_Twice (f : (ℕ → ℕ) → (ℕ → ℕ)) (x : ℕ → ℕ)
-  : (ℕ → ℕ) :=
-f (f x)
-end ex_1
+namespace ex1
+
+def double (x : Nat) := x + x
+def doTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x)
+def doTwiceTwice (f : (Nat → Nat) → (Nat → Nat)) (x : Nat → Nat) := f (f x)
+
+#reduce doTwiceTwice doTwice double 2
+
+end ex1
 
 -- Exercise 2
 --
 -- Define the functions `curry` and `uncurry`, as described in Section 2.4.
-section ex_2
-def curry (α β γ : Type*) (f : α × β → γ)
-  : α → β → γ :=
-λ α β, f (α, β)
+namespace ex2
 
-def uncurry (α β γ : Type*) (f : α → β → γ)
-  : α × β → γ :=
-λ x, f x.1 x.2
-end ex_2
+def curry (f : α × β → γ) : (α → β → γ) :=
+  fun α β => f (α, β)
 
--- Borrowed from the book.
-universe u
-constant vec : Type u → ℕ → Type u
+def uncurry (f : α → β → γ) : (α × β → γ) :=
+  fun x => f x.1 x.2
 
-namespace vec
-constant empty : Π (α : Type u), vec α 0
-constant cons : Π (α : Type u) (n : ℕ), α → vec α n → vec α (n + 1)
-constant append : Π (α : Type u) (n m : ℕ), vec α m → vec α n → vec α (n + m)
-end vec
+end ex2
 
 -- Exercise 3
 --
@@ -48,23 +38,30 @@ end vec
 -- implicit arguments for parameters that can be inferred. Declare some
 -- variables and check some expressions involving the constants that you have
 -- declared.
-section ex_3
+namespace ex3
+
+universe u
+axiom vec : Type u → Nat → Type u
 
 namespace vec
-constant add :
-  Π {α : Type u} {n : ℕ}, vec α n → vec α n → vec α n
-constant reverse :
-  Π {α : Type u} {n : ℕ}, vec α n → vec α n
+
+axiom empty : ∀ (α : Type u), vec α 0
+axiom cons : ∀ (α : Type u) (n : Nat), α → vec α n → vec α (n + 1)
+axiom append : ∀ (α : Type u) (n m : Nat), vec α m → vec α n → vec α (n + m)
+axiom add : ∀ {α : Type u} {n : Nat}, vec α n → vec α n → vec α n
+axiom reverse : ∀ {α : Type u} {n : Nat}, vec α n → vec α n
+
 end vec
 
 -- Check results.
-variables a b : vec Prop 1
-variables c d : vec Prop 2
+variable (a b : vec Prop 1)
+variable (c d : vec Prop 2)
+
 #check vec.add a b
 -- #check vec.add a c
 #check vec.reverse a
 
-end ex_3
+end ex3
 
 -- Exercise 4
 --
@@ -74,23 +71,29 @@ end ex_3
 -- (using vec) multiplication of a matrix by a vector. Once again, declare some
 -- variables and check some expressions involving the constants that you have
 -- declared.
-constant matrix : Type u → ℕ → ℕ → Type u
+namespace ex4
 
-section ex_4
+universe u
+axiom matrix : Type u → Nat → Nat → Type u
 
 namespace matrix
-constant add : Π {α : Type u} {m n : ℕ}, matrix α m n → matrix α m n → matrix α m n
-constant mul : Π {α : Type u} {m n p : ℕ}, matrix α m n → matrix α n p → matrix α m p
-constant app : Π {α : Type u} {m n : ℕ}, matrix α m n → vec α n → vec α m
+
+axiom add : ∀ {α : Type u} {m n : Nat},
+  matrix α m n → matrix α m n → matrix α m n
+axiom mul : ∀ {α : Type u} {m n p : Nat},
+  matrix α m n → matrix α n p → matrix α m p
+axiom app : ∀ {α : Type u} {m n : Nat},
+  matrix α m n → ex3.vec α n → ex3.vec α m
+
 end matrix
 
-variables a b : matrix Prop 5 7
-variable c : matrix Prop 7 3
-variable d : vec Prop 3
+variable (a b : matrix Prop 5 7)
+variable (c : matrix Prop 7 3)
+variable (d : ex3.vec Prop 3)
 
 #check matrix.add a b
 -- #check matrix.add a c
 #check matrix.mul a c
 #check matrix.app c d
 
-end ex_4
+end ex4
diff --git a/src/theorem-proving-in-lean/exercises-3.lean b/src/theorem-proving-in-lean/exercises-3.lean
index 43fc767..3c94d41 100644
--- a/src/theorem-proving-in-lean/exercises-3.lean
+++ b/src/theorem-proving-in-lean/exercises-3.lean
@@ -1,4 +1,4 @@
-/- Exercises 3.7
+/- Exercises 3
  -
  - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
@@ -7,189 +7,153 @@
 --
 -- Prove the following identities, replacing the "sorry" placeholders with
 -- actual proofs.
-section ex_1
+namespace ex1
 
 open or
 
-variables p q r : Prop
+variable (p q r : Prop)
 
 -- Commutativity of ∧ and ∨
 example : p ∧ q ↔ q ∧ p :=
-  iff.intro
-    (assume ⟨p, q⟩, ⟨q, p⟩)
-    (assume ⟨q, p⟩, ⟨p, q⟩)
+  Iff.intro
+    (fun ⟨hp, hq⟩ => show q ∧ p from ⟨hq, hp⟩)
+    (fun ⟨hq, hp⟩ => show p ∧ q from ⟨hp, hq⟩)
+
 example : p ∨ q ↔ q ∨ p :=
-  iff.intro
-    (assume h, h.elim
-      (assume hp : p, inr hp)
-      (assume hq : q, inl hq))
-    (assume h, h.elim
-      (assume hq : q, inr hq)
-      (assume hp : p, inl hp))
+  Iff.intro
+    (fun h => h.elim Or.inr Or.inl)
+    (fun h => h.elim Or.inr Or.inl)
 
 -- Associativity of ∧ and ∨
 example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
-  iff.intro
-    (assume ⟨⟨p, q⟩, r⟩, ⟨p, q, r⟩)
-    (assume ⟨p, q, r⟩, ⟨⟨p, q⟩, r⟩)
+  Iff.intro
+    (fun ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, hq, hr⟩)
+    (fun ⟨hp, hq, hr⟩ => ⟨⟨hp, hq⟩, hr⟩)
+
 example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
-  iff.intro
-    (assume h₁, h₁.elim
-      (assume h₂, h₂.elim (assume p, inl p) (assume q, inr (inl q)))
-      (assume r, inr (inr r)))
-    (assume h₁, h₁.elim
-      (assume p, inl (inl p))
-      (assume h₂, h₂.elim (assume q, inl (inr q)) (assume r, inr r)))
+  Iff.intro
+    (fun h₁ => h₁.elim
+      (fun h₂ => h₂.elim Or.inl (Or.inr ∘ Or.inl))
+      (Or.inr ∘ Or.inr))
+    (fun h₁ => h₁.elim
+      (Or.inl ∘ Or.inl)
+      (fun h₂ => h₂.elim (Or.inl ∘ Or.inr) Or.inr))
 
 -- Distributivity
 example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
-  iff.intro
-    (assume ⟨hp, hqr⟩, hqr.elim
-      (assume hq, inl ⟨hp, hq⟩)
-      (assume hr, inr ⟨hp, hr⟩))
-    (assume h₁, h₁.elim
-      (assume ⟨hp, hq⟩, ⟨hp, inl hq⟩)
-      (assume ⟨hp, hr⟩, ⟨hp, inr hr⟩))
+  Iff.intro
+    (fun ⟨hp, hqr⟩ => hqr.elim (Or.inl ⟨hp, ·⟩) (Or.inr ⟨hp, ·⟩))
+    (fun h₁ => h₁.elim
+      (fun ⟨hp, hq⟩ => ⟨hp, Or.inl hq⟩)
+      (fun ⟨hp, hr⟩ => ⟨hp, Or.inr hr⟩))
+
 example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
-  iff.intro
-    (assume h, h.elim
-      (assume hp, ⟨inl hp, inl hp⟩)
-      (assume ⟨hq, hr⟩, ⟨inr hq, inr hr⟩))
-    (assume ⟨h₁, h₂⟩, h₁.elim
-      (assume hp, inl hp)
-      (assume hq, h₂.elim (assume hp, inl hp) (assume hr, inr ⟨hq, hr⟩)))
+  Iff.intro
+    (fun h => h.elim
+      (fun hp => ⟨Or.inl hp, Or.inl hp⟩)
+      (fun ⟨hq, hr⟩ => ⟨Or.inr hq, Or.inr hr⟩))
+    (fun ⟨h₁, h₂⟩ => h₁.elim
+      Or.inl
+      (fun hq => h₂.elim Or.inl (fun hr => Or.inr ⟨hq, hr⟩)))
 
 -- Other properties
 example : (p → (q → r)) ↔ (p ∧ q → r) :=
-  iff.intro
-    (assume h ⟨hp, hq⟩, h hp hq)
-    (assume h hp hq, h ⟨hp, hq⟩)
+  Iff.intro
+    (fun h ⟨hp, hq⟩ => h hp hq)
+    (fun h hp hq => h ⟨hp, hq⟩)
 
 example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
-  iff.intro
-    (assume h,
-      have h₁ : p → r, from (assume hp, h (or.inl hp)),
-      have h₂ : q → r, from (assume hq, h (or.inr hq)),
-      ⟨h₁, h₂⟩)
-    (assume ⟨hpr, hqr⟩, assume hpq, hpq.elim hpr hqr)
+  Iff.intro
+    (fun h =>
+      have h₁ : p → r := h ∘ Or.inl
+      have h₂ : q → r := h ∘ Or.inr
+      show (p → r) ∧ (q → r) from ⟨h₁, h₂⟩)
+    (fun ⟨h₁, h₂⟩ h => h.elim h₁ h₂)
 
 example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
-  iff.intro
-    (assume h, and.intro
-      (assume hp, h (inl hp))
-      (assume hq, h (inr hq)))
-    (assume h₁ h₂, h₂.elim
-      (assume hp, have np : ¬p, from h₁.left, absurd hp np)
-      (assume hq, have nq : ¬q, from h₁.right, absurd hq nq))
+  Iff.intro
+    (fun h => ⟨h ∘ Or.inl, h ∘ Or.inr⟩)
+    (fun h₁ h₂ => h₂.elim (absurd · h₁.left) (absurd · h₁.right))
 
 example : ¬p ∨ ¬q → ¬(p ∧ q) :=
-  assume h₁ h₂,
-  h₁.elim
-    (assume np : ¬p, have hp : p, from h₂.left, absurd hp np)
-    (assume nq : ¬q, have hq : q, from h₂.right, absurd hq nq)
+  fun h₁ h₂ => h₁.elim (absurd h₂.left ·) (absurd h₂.right ·)
 
 example : ¬(p ∧ ¬p) :=
-  assume h,
-  have hp : p, from h.left,
-  have np : ¬p, from h.right,
-  absurd hp np
+  fun h => absurd h.left h.right
 
 example : p ∧ ¬q → ¬(p → q) :=
-  assume ⟨hp, nq⟩ hpq,
-  absurd (hpq hp) nq
+  fun ⟨hp, nq⟩ hpq => absurd (hpq hp) nq
 
 example : ¬p → (p → q) :=
-  assume np hp,
-  absurd hp np
+  fun np hp => absurd hp np
 
 example : (¬p ∨ q) → (p → q) :=
-  assume npq hp,
-  npq.elim
-    (assume np, absurd hp np)
-    (assume hq, hq)
+  fun npq hp => npq.elim (absurd hp ·) id
 
-example : p ∨ false ↔ p :=
-  iff.intro
-    (assume hpf, hpf.elim
-      (assume hp, hp)
-      (assume hf, false.elim hf))
-    (assume hp, inl hp)
+example : p ∨ False ↔ p :=
+  Iff.intro (fun hpf => hpf.elim id False.elim) Or.inl
 
-example : p ∧ false ↔ false :=
-  iff.intro
-    (assume ⟨hp, hf⟩, hf)
-    (assume hf, false.elim hf)
+example : p ∧ False ↔ False :=
+  Iff.intro (fun ⟨_, hf⟩ => hf) False.elim
 
 example : (p → q) → (¬q → ¬p) :=
-  assume hpq nq hp,
-  absurd (hpq hp) nq
+  fun hpq nq hp => absurd (hpq hp) nq
 
-end ex_1
+end ex1
 
 -- Example 2
 --
 -- Prove the following identities, replacing the “sorry” placeholders with
 -- actual proofs. These require classical reasoning.
-section ex_2
+namespace ex2
 
-open classical
+open Classical
 
-variables p q r s : Prop
+variable (p q r s : Prop)
 
 example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
-  assume h₁,
-  or.elim (h₁ hp)
-    (assume hr, or.inl (assume hp, hr))
-    (assume hs, or.inr (assume hp, hs))
+  fun h => (h hp).elim
+    (fun hr => Or.inl (fun _ => hr))
+    (fun hs => Or.inr (fun _ => hs))
 
 example : ¬(p ∧ q) → ¬p ∨ ¬q :=
-  assume npq,
-  or.elim (em p)
-    (assume hp, or.elim (em q)
-      (assume hq, false.elim (npq ⟨hp, hq⟩))
-      (assume nq, or.inr nq))
-    (assume np, or.inl np)
+  fun npq => (em p).elim
+    (fun hp => (em q).elim
+      (fun hq => False.elim (npq ⟨hp, hq⟩))
+      Or.inr)
+    Or.inl
 
 example : ¬(p → q) → p ∧ ¬q :=
-  assume h₁,
-  and.intro
-    (by_contradiction (
-      assume np,
-      h₁ (λ (hp : p), absurd hp np)
-    ))
-    (assume hq, h₁ (λ (hp : p), hq))
+  fun h =>
+    have lhs : p := byContradiction
+      fun np => h (fun (hp : p) => absurd hp np)
+    ⟨lhs, fun hq => h (fun _ => hq)⟩
 
 example : (p → q) → (¬p ∨ q) :=
-  assume hpq,
-  or.elim (em p)
-    (assume hp, or.inr (hpq hp))
-    (assume np, or.inl np)
+  fun hpq => (em p).elim (fun hp => Or.inr (hpq hp)) Or.inl
 
 example : (¬q → ¬p) → (p → q) :=
-  assume h₁ hp,
-  by_contradiction (assume nq, absurd hp (h₁ nq))
+  fun h hp => byContradiction
+    fun nq => absurd hp (h nq)
 
 example : p ∨ ¬p := em p
 
 example : (((p → q) → p) → p) :=
-  assume h₁,
-  by_contradiction (
-    assume np,
-    suffices hp : p, from absurd hp np,
-    h₁ (λ (hp : p), absurd hp np)
-  )
+  fun h => byContradiction
+    fun np =>
+      suffices hp : p from absurd hp np
+      h (fun (hp : p) => absurd hp np)
 
-end ex_2
+end ex2
 
 -- Example 3
 --
 -- Prove `¬(p ↔ ¬p)` without using classical logic.
-section ex_3
+namespace ex3
 
-variable p : Prop
+variable (p : Prop)
 
 example (hp : p) : ¬(p ↔ ¬p) :=
-  assume h,
-  absurd hp (iff.elim_left h (hp))
+  fun h => absurd hp (Iff.mp h hp)
 
-end ex_3
+end ex3
diff --git a/src/theorem-proving-in-lean/exercises-4.lean b/src/theorem-proving-in-lean/exercises-4.lean
index 2b850e6..2b53657 100644
--- a/src/theorem-proving-in-lean/exercises-4.lean
+++ b/src/theorem-proving-in-lean/exercises-4.lean
@@ -1,102 +1,94 @@
-/- Exercises 4.6
+/- Exercises 4
  -
  - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
-import data.int.basic
-import data.nat.basic
-import data.real.basic
 
 -- Exercise 1
 --
 -- Prove these equivalences. You should also try to understand why the reverse
 -- implication is not derivable in the last example.
-section ex_1
+namespace ex1
 
-variables (α : Type*) (p q : α → Prop)
+variable (α : Type _)
+variable (p q : α → Prop)
 
 example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
-  iff.intro
-    ( assume h,
-      and.intro
-        (assume x, and.left (h x))
-        (assume x, and.right (h x)))
-    (assume ⟨h₁, h₂⟩ x, ⟨h₁ x, h₂ x⟩)
+  Iff.intro
+    (fun h => ⟨fun x => And.left (h x), fun x => And.right (h x)⟩)
+    (fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩)
 
 example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
-  assume h₁ h₂ x,
-  have px : p x, from h₂ x,
-  h₁ x px
+  fun h₁ h₂ x =>
+    have px : p x := h₂ x
+    h₁ x px
 
 example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
-  assume h₁ x,
-  h₁.elim
-    (assume h₂, or.inl (h₂ x))
-    (assume h₂, or.inr (h₂ x))
+  fun h₁ x => h₁.elim
+    (fun h₂ => Or.inl (h₂ x))
+    (fun h₂ => Or.inr (h₂ x))
 
 -- The implication in the above example cannot be proven in the other direction
 -- because it may be the case predicate `p x` holds for certain values of `x`
 -- but not others that `q x` may hold for (and vice versa).
 
-end ex_1
+end ex1
 
 -- Exercise 2
 --
 -- It is often possible to bring a component of a formula outside a universal
 -- quantifier, when it does not depend on the quantified variable. Try proving
 -- these (one direction of the second of these requires classical logic).
-section ex_2
+namespace ex2
 
-variables (α : Type*) (p q : α → Prop)
-variable r : Prop
+variable (α : Type _)
+variable (p q : α → Prop)
+variable (r : Prop)
 
-example : α → ((∀ x : α, r) ↔ r) :=
-  assume ha,
-  iff.intro (assume h, h ha) (assume hr ha, hr)
+example : α → ((∀ _ : α, r) ↔ r) :=
+  fun a => Iff.intro (fun h => h a) (fun hr _ => hr)
 
--- Ensure we do not use classical logic in the first or third subproblems.
 section
 
-open classical
+open Classical
 
 example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
-  iff.intro
-    (assume h₁, or.elim (classical.em r)
-      (assume hr, or.inr hr)
-      (assume nr, or.inl (λ (x : α), or.elim (h₁ x)
-        (assume hp, hp)
-        (assume hr, absurd hr nr))))
-    (assume h₁, or.elim h₁
-      (assume h₂, (λ (x : α), or.inl (h₂ x)))
-      (assume hr, (λ (x : α), or.inr hr)))
+  Iff.intro
+    (fun h₁ => (em r).elim
+      Or.inr
+      (fun nr => Or.inl (fun x => (h₁ x).elim id (absurd · nr))))
+    (fun h₁ => h₁.elim
+      (fun h₂ x => Or.inl (h₂ x))
+      (fun hr _ => Or.inr hr))
+
 end
 
 example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
-  iff.intro
-    (assume h₁ hr hx, h₁ hx hr)
-    (assume h₁ hx hr, h₁ hr hx)
+  Iff.intro
+    (fun h hr hx => h hx hr)
+    (fun h hx hr => h hr hx)
 
-end ex_2
+end ex2
 
 -- Exercise 3
 --
 -- Consider the "barber paradox," that is, the claim that in a certain town
 -- there is a (male) barber that shaves all and only the men who do not shave
 -- themselves. Prove that this is a contradiction.
-section ex_3
+namespace ex3
 
-open classical
+open Classical
 
-variables (men : Type*) (barber : men)
+variable (men : Type _)
+variable (barber : men)
 variable (shaves : men → men → Prop)
 
-example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) :
-  false :=
-    have b : shaves barber barber ↔ ¬ shaves barber barber, from h barber,
-    or.elim (classical.em (shaves barber barber))
-      (assume b', absurd b' (iff.elim_left b b'))
-      (assume b', absurd (iff.elim_right b b') b')
+example (h : ∀ x : men, shaves barber x ↔ ¬shaves x x) : False :=
+  have b : shaves barber barber ↔ ¬shaves barber barber := h barber
+  (em (shaves barber barber)).elim
+    (fun b' => absurd b' (Iff.mp b b'))
+    (fun b' => absurd (Iff.mpr b b') b')
 
-end ex_3
+end ex3
 
 -- Exercise 4
 --
@@ -108,162 +100,141 @@ end ex_3
 -- states that every odd number greater than `5` is the sum of three primes.
 -- Look up the definition of a Fermat prime or any of the other statements, if
 -- necessary.
-section ex_4
+namespace ex4
 
-def prime (n : ℕ) : Prop :=
-  n > 1 ∧ ∀ (m : ℕ), (1 < m ∧ m < n) → n % m ≠ 0
+def even (a : Nat) := ∃ b, a = 2 * b
 
-def infinitely_many_primes : Prop :=
-  ∀ (n : ℕ), (∃ (m : ℕ), m > n ∧ prime m)
+def odd (a : Nat) := ¬even a
 
-def Fermat_prime (n : ℕ) : Prop :=
-  ∃ (m : ℕ), n = 2^(2^m) + 1
+def prime (n : Nat) : Prop :=
+  n > 1 ∧ ∀ (m : Nat), (1 < m ∧ m < n) → n % m ≠ 0
 
-def infinitely_many_Fermat_primes : Prop :=
-  ∀ (n : ℕ), (∃ (m : ℕ), m > n ∧ Fermat_prime m)
+def infinitelyManyPrimes : Prop :=
+  ∀ (n : Nat), (∃ (m : Nat), m > n ∧ prime m)
 
-def goldbach_conjecture : Prop :=
-  ∀ (n : ℕ), even n ∧ n > 2 → (∃ (x y : ℕ), prime x ∧ prime y ∧ x + y = n)
+def FermatPrime (n : Nat) : Prop :=
+  ∃ (m : Nat), n = 2^(2^m) + 1
 
-def Goldbach's_weak_conjecture : Prop :=
-  ∀ (n : ℕ), odd n ∧ n > 5 → (∃ (x y z : ℕ), prime x ∧ prime y ∧ prime z ∧ x + y + z = n)
+def infinitelyManyFermatPrimes : Prop :=
+  ∀ (n : Nat), (∃ (m : Nat), m > n ∧ FermatPrime m)
 
-def Fermat's_last_theorem : Prop :=
-  ∀ (n : ℕ), n > 2 → (∀ (a b c : ℕ), a^n + b^n ≠ c^n)
+def GoldbachConjecture : Prop :=
+  ∀ (n : Nat), even n ∧ n > 2 →
+    ∃ (x y : Nat), prime x ∧ prime y ∧ x + y = n
 
-end ex_4
+def Goldbach'sWeakConjecture : Prop :=
+  ∀ (n : Nat), odd n ∧ n > 5 →
+    ∃ (x y z : Nat), prime x ∧ prime y ∧ prime z ∧ x + y + z = n
+
+def Fermat'sLastTheorem : Prop :=
+  ∀ (n : Nat), n > 2 → (∀ (a b c : Nat), a^n + b^n ≠ c^n)
+
+end ex4
 
 -- Exercise 5
 --
 -- Prove as many of the identities listed in Section 4.4 as you can.
-section ex_5
+namespace ex5
 
-open classical
+open Classical
 
-variables (α : Type*) (p q : α → Prop)
-variables r s : Prop
+variable (α : Type _)
+variable (p q : α → Prop)
+variable (r s : Prop)
 
-example : (∃ x : α, r) → r :=
-  assume ⟨hx, hr⟩,
-  hr
+example : (∃ _ : α, r) → r :=
+  fun ⟨_, hr⟩ => hr
 
-example (a : α) : r → (∃ x : α, r) :=
-  assume hr,
-  ⟨a, hr⟩
+example (a : α) : r → (∃ _ : α, r) :=
+  fun hr => ⟨a, hr⟩
 
 example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
-  iff.intro
-    (assume ⟨hx, ⟨hp, hr⟩⟩, ⟨⟨hx, hp⟩, hr⟩)
-    (assume ⟨⟨hx, hp⟩, hr⟩, ⟨hx, ⟨hp, hr⟩⟩)
+  Iff.intro
+    (fun ⟨hx, ⟨hp, hr⟩⟩ => ⟨⟨hx, hp⟩, hr⟩)
+    (fun ⟨⟨hx, hp⟩, hr⟩ => ⟨hx, ⟨hp, hr⟩⟩)
 
 example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
-  iff.intro
-    (assume ⟨hx, hpq⟩, hpq.elim
-      (assume hp, or.inl (⟨hx, hp⟩))
-      (assume hq, or.inr (⟨hx, hq⟩)))
-    (assume h, h.elim
-      (assume ⟨hx, hp⟩, ⟨hx, or.inl hp⟩)
-      (assume ⟨hx, hq⟩, ⟨hx, or.inr hq⟩))
+  Iff.intro
+    (fun ⟨hx, hpq⟩ => hpq.elim
+      (fun hp => Or.inl ⟨hx, hp⟩)
+      (fun hq => Or.inr ⟨hx, hq⟩))
+    (fun h => h.elim
+      (fun ⟨hx, hp⟩ => ⟨hx, Or.inl hp⟩)
+      (fun ⟨hx, hq⟩ => ⟨hx, Or.inr hq⟩))
 
-example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
-  iff.intro
-    (assume h ⟨hx, np⟩, np (h hx))
-    (assume h hx, classical.by_contradiction (assume np, h ⟨hx, np⟩))
+example : (∀ x, p x) ↔ ¬(∃ x, ¬p x) :=
+  Iff.intro
+    (fun h ⟨hx, np⟩ => np (h hx))
+    (fun h hx => byContradiction
+      fun np => h ⟨hx, np⟩)
 
-example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
-  iff.intro
-    (assume ⟨hx, hp⟩ h, absurd hp (h hx))
-    (assume h, classical.by_contradiction (
-      assume h',
-      h (λ (x : α), assume hp, h' ⟨x, hp⟩)
-    ))
+example : (∃ x, p x) ↔ ¬(∀ x, ¬p x) :=
+  Iff.intro
+    (fun ⟨hx, hp⟩ h => absurd hp (h hx))
+    (fun h => byContradiction
+      fun h' => h (fun (x : α) hp => h' ⟨x, hp⟩))
 
-example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
-  iff.intro
-    (assume h hx hp, h ⟨hx, hp⟩)
-    (assume h ⟨hx, hp⟩, absurd hp (h hx))
+example : (¬∃ x, p x) ↔ (∀ x, ¬p x) :=
+  Iff.intro
+    (fun h hx hp => h ⟨hx, hp⟩)
+    (fun h ⟨hx, hp⟩ => absurd hp (h hx))
 
-lemma forall_negation : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
-  iff.intro
-    (assume h, classical.by_contradiction (
-      assume h',
-      h (λ (x : α), classical.by_contradiction (
-        assume np,
-        h' ⟨x, np⟩
-      ))
-    ))
-    (assume ⟨hx, np⟩ h, absurd (h hx) np)
+theorem forall_negation : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
+  Iff.intro
+    (fun h => byContradiction
+      fun h' => h (fun (x : α) => byContradiction
+        fun np => h' ⟨x, np⟩))
+    (fun ⟨hx, np⟩ h => absurd (h hx) np)
 
-example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
+example : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
   forall_negation α p
 
 example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
-  iff.intro
-    (assume h ⟨hx, hp⟩, h hx hp)
-    (assume h hx hp, h ⟨hx, hp⟩)
+  Iff.intro
+    (fun h ⟨hx, hp⟩ => h hx hp)
+    (fun h hx hp => h ⟨hx, hp⟩)
 
 example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
-  iff.intro
-    (assume ⟨hx, hp⟩ h, hp (h hx))
-    (assume h₁, or.elim (classical.em (∀ x, p x))
-      (assume h₂, ⟨a, assume hp, h₁ h₂⟩)
-      (assume h₂,
-        have h₃ : (∃ x, ¬p x), from iff.elim_left (forall_negation α p) h₂,
+  Iff.intro
+    (fun ⟨hx, hp⟩ h => hp (h hx))
+    (fun h₁ => (em (∀ x, p x)).elim
+      (fun h₂ => ⟨a, fun _ => h₁ h₂⟩)
+      (fun h₂ =>
+        have h₃ : (∃ x, ¬p x) := Iff.mp (forall_negation α p) h₂
         match h₃ with
-          ⟨hx, hp⟩ := ⟨hx, (assume hp', absurd hp' hp)⟩
-        end))
+        | ⟨hx, hp⟩ => ⟨hx, fun hp' => absurd hp' hp⟩))
 
 example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
-  iff.intro
-    (assume ⟨hx, hrp⟩ hr, ⟨hx, hrp hr⟩)
-    (assume h, or.elim (classical.em r)
-      (assume hr, match h hr with
-        ⟨hx, hp⟩ := ⟨hx, (assume hr, hp)⟩
-      end)
-      (assume nr, ⟨a, (assume hr, absurd hr nr)⟩))
+  Iff.intro
+    (fun ⟨hx, hrp⟩ hr => ⟨hx, hrp hr⟩)
+    (fun h => (em r).elim
+      (fun hr => match h hr with
+                 | ⟨hx, hp⟩ => ⟨hx, fun _ => hp⟩)
+      (fun nr => ⟨a, fun hr => absurd hr nr⟩))
 
-end ex_5
+end ex5
 
 -- Exercise 6
 --
 -- Give a calculational proof of the theorem `log_mul` below.
-section ex_6
+namespace ex6
 
-variables log exp : real → real
-variable log_exp_eq : ∀ x, log (exp x) = x
-variable exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x
-variable exp_pos : ∀ x, exp x > 0
-variable exp_add : ∀ x y, exp (x + y) = exp x * exp y
+variable (log exp : Float → Float)
+variable (log_exp_eq : ∀ x, log (exp x) = x)
+variable (exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x)
+variable (exp_pos : ∀ x, exp x > 0)
+variable (exp_add : ∀ x y, exp (x + y) = exp x * exp y)
 
--- this ensures the assumptions are available in tactic proofs
-include log_exp_eq exp_log_eq exp_pos exp_add
+example (x y z : Float) : exp (x + y + z) = exp x * exp y * exp z :=
+  by rw [exp_add, exp_add]
 
-example (x y z : real) :
-  exp (x + y + z) = exp x * exp y * exp z :=
-by rw [exp_add, exp_add]
+example (y : Float) (h : y > 0) : exp (log y) = y := exp_log_eq h
 
-example (y : real) (h : y > 0) : exp (log y) = y :=
-exp_log_eq h
-
-theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) :
+theorem log_mul {x y : Float} (hx : x > 0) (hy : y > 0) :
   log (x * y) = log x + log y :=
-calc log (x * y) = log (x * exp (log y)) : by rw (exp_log_eq hy)
-             ... = log (exp (log x) * exp (log y)) : by rw (exp_log_eq hx)
-             ... = log (exp (log x + log y)) : by rw exp_add
-             ... = log x + log y : by rw log_exp_eq
+calc log (x * y) = log (x * exp (log y)) := by rw [exp_log_eq hy]
+               _ = log (exp (log x) * exp (log y)) := by rw [exp_log_eq hx]
+               _ = log (exp (log x + log y)) := by rw [exp_add]
+               _ = log x + log y := by rw [log_exp_eq]
 
-end ex_6
-
--- Exercise 7
---
--- Prove the theorem below, using only the ring properties of ℤ enumerated in
--- Section 4.2 and the theorem `sub_self.`
-section ex_7
-#check sub_self
-
-example (x : ℤ) : x * 0 = 0 :=
-calc x * 0 = x * (x - x) : by rw (sub_self x)
-       ... = x * x - x * x : by rw (mul_sub x x x)
-       ... = 0 : by rw (sub_self (x * x))
-
-end ex_7
+end ex6
diff --git a/src/theorem-proving-in-lean/exercises-5.lean b/src/theorem-proving-in-lean/exercises-5.lean
index 355afe8..d1a1ec8 100644
--- a/src/theorem-proving-in-lean/exercises-5.lean
+++ b/src/theorem-proving-in-lean/exercises-5.lean
@@ -1,499 +1,453 @@
-/- Exercises 5.8
+/- Exercises 5
  -
  - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
-import tactic.rcases
-
 -- Exercise 1
 --
 -- Go back to the exercises in Chapter 3 and Chapter 4 and redo as many as you
 -- can now with tactic proofs, using also `rw` and `simp` as appropriate.
-section ex_1_3_1
+namespace ex1
 
-variables p q r : Prop
+-- Exercises 3.1
+
+section ex3_1
+
+variable (p q r : Prop)
 
 -- Commutativity of ∧ and ∨
-example : p ∧ q ↔ q ∧ p :=
-begin
-  split,
-  { rintro ⟨p, q⟩, exact ⟨q, p⟩ },
-  { rintro ⟨q, p⟩, exact ⟨p, q⟩ },
-end
+example : p ∧ q ↔ q ∧ p := by
+  apply Iff.intro
+  · intro ⟨hp, hq⟩
+    exact ⟨hq, hp⟩
+  · intro ⟨hq, hp⟩
+    exact ⟨hp, hq⟩
 
-example : p ∨ q ↔ q ∨ p :=
-begin
-  split,
-  { rintro (p | q),
-    { exact or.inr p },
-    { exact or.inl q },
-  },
-  { rintro (q | p),
-    { exact or.inr q },
-    { exact or.inl p },
-  },
-end
+example : p ∨ q ↔ q ∨ p := by
+  apply Iff.intro
+  · intro
+    | Or.inl hp => exact Or.inr hp
+    | Or.inr hq => exact Or.inl hq
+  · intro
+    | Or.inl hq => exact Or.inr hq
+    | Or.inr hp => exact Or.inl hp
 
 -- Associativity of ∧ and ∨
-example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
-begin
-  split,
-  { rintro ⟨⟨p, q⟩, r⟩, exact ⟨p, q, r⟩ },
-  { rintro ⟨p, q, r⟩, exact ⟨⟨p, q⟩, r⟩ },
-end
+example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
+  apply Iff.intro
+  · intro ⟨⟨hp, hq⟩, hr⟩
+    exact ⟨hp, hq, hr⟩
+  · intro ⟨hp, hq, hr⟩
+    exact ⟨⟨hp, hq⟩, hr⟩
 
-example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
-begin
-  split,
-  { rintro ((p | q) | r),
-    { exact or.inl p },
-    { exact or.inr (or.inl q) },
-    { exact or.inr (or.inr r) },
-  },
-  { rintro (p | q | r),
-    { exact or.inl (or.inl p) },
-    { exact or.inl (or.inr q) },
-    { exact or.inr r },
-  },
-end
+example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
+  apply Iff.intro
+  · intro
+    | Or.inl (Or.inl hp) => exact Or.inl hp
+    | Or.inl (Or.inr hq) => exact Or.inr (Or.inl hq)
+    | Or.inr         hr  => exact Or.inr (Or.inr hr)
+  · intro
+    | Or.inl         hp  => exact Or.inl (Or.inl hp)
+    | Or.inr (Or.inl hq) => exact Or.inl (Or.inr hq)
+    | Or.inr (Or.inr hr) => exact Or.inr hr
 
 -- Distributivity
-example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
-begin
-  split,
-  { rintro ⟨p, (q | r)⟩,
-    { exact or.inl ⟨p, q⟩ },
-    { exact or.inr ⟨p, r⟩ },
-  },
-  { rintro (⟨p, q⟩ | ⟨p, r⟩),
-    { exact ⟨p, or.inl q⟩ },
-    { exact ⟨p, or.inr r⟩ },
-  },
-end
+example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
+  apply Iff.intro
+  · intro
+    | ⟨hp, Or.inl hq⟩ => exact Or.inl ⟨hp, hq⟩
+    | ⟨hp, Or.inr hr⟩ => exact Or.inr ⟨hp, hr⟩
+  · intro
+    | Or.inl ⟨hp, hq⟩ => exact ⟨hp, Or.inl hq⟩
+    | Or.inr ⟨hp, hr⟩ => exact ⟨hp, Or.inr hr⟩
 
-example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
-begin
-  split,
-  { rintro (p | ⟨q, r⟩),
-    { exact ⟨or.inl p, or.inl p⟩ },
-    { exact ⟨or.inr q, or.inr r⟩ },
-  },
-  { rintro ⟨(p | q), (p | r)⟩;
-    exact or.inl p <|> exact or.inr ⟨q, r⟩,
-  },
-end
+example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
+  apply Iff.intro
+  · intro
+    | Or.inl      hp  => exact ⟨Or.inl hp, Or.inl hp⟩
+    | Or.inr ⟨hq, hr⟩ => exact ⟨Or.inr hq, Or.inr hr⟩
+  · intro
+    | ⟨Or.inl hp,         _⟩ => exact Or.inl hp
+    | ⟨Or.inr  _, Or.inl hp⟩ => exact Or.inl hp
+    | ⟨Or.inr hq, Or.inr hr⟩ => exact Or.inr ⟨hq, hr⟩
 
 -- Other properties
-example : (p → (q → r)) ↔ (p ∧ q → r) :=
-begin
-  split,
-  { rintros h ⟨hp, hq⟩, exact h hp hq },
-  { intros h hp hq, exact h ⟨hp, hq⟩ },
-end
+example : (p → (q → r)) ↔ (p ∧ q → r) := by
+  apply Iff.intro
+  · intro h ⟨hp, hq⟩
+    exact h hp hq
+  · intro h hp hq
+    exact h ⟨hp, hq⟩
 
-example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
-begin
-  split,
-  { intros h₁,
-    split,
-    { intro p, exact h₁ (or.inl p) },
-    { intro q, exact h₁ (or.inr q) },
-  },
-  { rintros ⟨hp, hq⟩ h,
-    apply or.elim h,
-    { intro p, exact hp p },
-    { intro q, exact hq q },
-  },
-end
+example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := by
+  apply Iff.intro
+  · intro h
+    apply And.intro
+    · intro hp
+      exact h (Or.inl hp)
+    · intro hq
+      exact h (Or.inr hq)
+  · intro ⟨hpr, hqr⟩ h
+    apply Or.elim h
+    · intro hp
+      exact hpr hp
+    · intro hq
+      exact hqr hq
 
-example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
-begin
-  split,
-  { intro h,
-    split,
-    { intro hp, apply h, exact or.inl hp },
-    { intro hq, apply h, exact or.inr hq },
-  },
-  { rintros ⟨np, nq⟩ (p | q),
-    { apply np, assumption },
-    { apply nq, assumption },
-  },
-end
+example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
+  apply Iff.intro
+  · intro h
+    apply And.intro
+    · intro hp
+      exact h (Or.inl hp)
+    · intro hq
+      exact h (Or.inr hq)
+  · intro ⟨np, nq⟩
+    intro
+    | Or.inl hp => exact absurd hp np
+    | Or.inr hq => exact absurd hq nq
 
-example : ¬p ∨ ¬q → ¬(p ∧ q) :=
-begin
-  rintro (np | nq) ⟨hp, hq⟩,
-  { apply np, assumption },
-  { apply nq, assumption },
-end
+example : ¬p ∨ ¬q → ¬(p ∧ q) := by
+  intro
+  | Or.inl np => intro h; exact absurd h.left np
+  | Or.inr nq => intro h; exact absurd h.right nq
 
-example : ¬(p ∧ ¬p) :=
-begin
-  rintro ⟨hp, np⟩,
+example : ¬(p ∧ ¬p) := by
+  intro ⟨hp, np⟩
   exact absurd hp np
-end
 
-example : p ∧ ¬q → ¬(p → q) :=
-begin
-  rintro ⟨hp, nq⟩ hpq,
-  apply nq,
-  exact hpq hp
-end
+example : p ∧ ¬q → ¬(p → q) := by
+  intro ⟨hp, nq⟩ h
+  exact absurd (h hp) nq
 
-example : ¬p → (p → q) :=
-begin
-  intros np hp,
-  exact absurd hp np,
-end
+example : ¬p → (p → q) := by
+  intro np hp
+  exact absurd hp np
 
-example : (¬p ∨ q) → (p → q) :=
-begin
-  rintros (np | hq) hp,
-  { exact absurd hp np },
-  { exact hq },
-end
+example : (¬p ∨ q) → (p → q) := by
+  intro
+  | Or.inl np => intro hp; exact absurd hp np
+  | Or.inr hq => exact fun _ => hq
 
-example : p ∨ false ↔ p :=
-begin
-  split,
-  { rintro (hp | hf),
-    { exact hp },
-    { exact false.elim hf },
-  },
-  { intro hp,
-    exact or.inl hp,
-  },
-end
+example : p ∨ False ↔ p := by
+  apply Iff.intro
+  · intro
+    | Or.inl hp => exact hp
+    | Or.inr ff => exact False.elim ff
+  · intro hp
+    exact Or.inl hp
 
-example : p ∧ false ↔ false :=
-begin
-  split,
-  { rintro ⟨hp, hf⟩, assumption },
-  { intro hf, exact false.elim hf },
-end
+example : p ∧ False ↔ False := by
+  apply Iff.intro
+  · intro ⟨_, ff⟩
+    exact ff
+  · intro ff
+    exact False.elim ff
 
-example : (p → q) → (¬q → ¬p) :=
-begin
-  rintro hpq nq hp,
-  apply nq,
-  exact absurd (hpq hp) nq,
-end
+example : (p → q) → (¬q → ¬p) := by
+  intro hpq nq hp
+  exact absurd (hpq hp) nq
 
-end ex_1_3_1
+end ex3_1
 
-section ex_1_3_2
+-- Exercises 3.2
 
-open classical
+section ex3_2
 
-variables p q r s : Prop
+open Classical
 
-example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
-begin
-  intro h,
-  apply or.elim (h hp),
-  { intro hr, exact or.inl (assume hp, hr) },
-  { intro hs, exact or.inr (assume hp, hs) }
-end
+variable (p q r s : Prop)
 
-example : ¬(p ∧ q) → ¬p ∨ ¬q :=
-begin
-  intro h₁,
-  apply or.elim (classical.em p),
-  { intro hp,
-    apply or.elim (classical.em q),
-    { assume hq, exact false.elim (h₁ ⟨hp, hq⟩) },
-    { assume nq, exact or.inr nq },
-  },
-  { intro np,
-    exact or.inl np,
-  },
-end
+example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) := by
+  intro h
+  apply (h hp).elim
+  · intro hr
+    exact Or.inl (fun _ => hr)
+  · intro hs
+    exact Or.inr (fun _ => hs)
 
-example : ¬(p → q) → p ∧ ¬q :=
-begin
-  intro h₁,
-  split,
-  { by_contradiction np, apply h₁, intro hp, exact absurd hp np },
-  { intro hq, apply h₁, intro hp, exact hq },
-end
+example : ¬(p ∧ q) → ¬p ∨ ¬q := by
+  intro h
+  apply (em p).elim
+  · intro hp
+    apply (em q).elim
+    · intro hq
+      exact False.elim (h ⟨hp, hq⟩)
+    · intro nq
+      exact Or.inr nq
+  · intro np
+    exact Or.inl np
 
-example : (p → q) → (¬p ∨ q) :=
-begin
-  intro hpq,
-  apply or.elim (classical.em p),
-  { assume hp, exact or.inr (hpq hp) },
-  { assume np, exact or.inl np },
-end
+example : ¬(p → q) → p ∧ ¬q := by
+  intro h
+  apply And.intro
+  · apply byContradiction
+    intro np
+    apply h
+    intro hp
+    exact absurd hp np
+  · intro hq
+    apply h
+    intro _
+    exact hq
 
-example : (¬q → ¬p) → (p → q) :=
-begin
-  intros hqp hp,
-  by_contradiction nq,
-  exact absurd hp (hqp nq),
-end
+example : (p → q) → (¬p ∨ q) := by
+  intro hpq
+  apply (em p).elim
+  · intro hp
+    exact Or.inr (hpq hp)
+  · intro np
+    exact Or.inl np
 
-example : p ∨ ¬p :=
-by apply classical.em
+example : (¬q → ¬p) → (p → q) := by
+  intro hqp hp
+  apply byContradiction
+  intro nq
+  exact absurd hp (hqp nq)
 
-example : (((p → q) → p) → p) :=
-begin
-  intro h,
-  apply or.elim (classical.em p),
-  { intro hp, assumption },
-  { intro np, apply h, intro hp, exact absurd hp np },
-end
+example : p ∨ ¬p := by apply em
 
-end ex_1_3_2
+example : (((p → q) → p) → p) := by
+  intro h
+  apply (em p).elim
+  · intro hp
+    exact hp
+  · intro np
+    apply h
+    intro hp
+    exact absurd hp np
 
-section ex_1_3_3
+end ex3_2
 
-variable p : Prop
+-- Exercises 3.3
 
-example (hp : p) : ¬(p ↔ ¬p) :=
-begin
-  intro h₁,
-  cases h₁ with h₂,
-  exact absurd hp (h₂ hp),
-end
+section ex3_3
 
-end ex_1_3_3
+variable (p : Prop)
 
-section ex_1_4_1
+example (hp : p) : ¬(p ↔ ¬p) := by
+  intro h
+  exact absurd hp (h.mp hp)
 
-variables (α : Type*) (p q : α → Prop)
+end ex3_3
 
-example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
-begin
-  split,
-  { intro h,
-    split,
-    { intro hx, exact and.left (h hx) },
-    { intro hx, exact and.right (h hx) },
-  },
-  { intros h hx,
-    have hl : ∀ (x : α), p x, from and.left h,
-    have hr : ∀ (x : α), q x, from and.right h,
-    exact ⟨hl hx, hr hx⟩
-  },
-end
+-- Exercises 4.1
 
-example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
-begin
-  intros h₁ h₂ hx,
+section ex4_1
+
+variable (α : Type _)
+variable (p q : α → Prop)
+
+example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
+  apply Iff.intro
+  · intro h
+    apply And.intro
+    · intro hx; exact And.left (h hx)
+    · intro hx; exact And.right (h hx)
+  · intro h hx
+    have lhs : ∀ (x : α), p x := And.left h
+    have rhs : ∀ (x : α), q x := And.right h
+    exact ⟨lhs hx, rhs hx⟩
+
+example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := by
+  intro h₁ h₂ hx
   exact h₁ hx (h₂ hx)
-end
 
-example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
-begin
-  rintro (h₁ | h₂),
-  { intro hx, exact or.inl (h₁ hx) },
-  { intro hx, exact or.inr (h₂ hx) },
-end
+example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := by
+  intro
+  | Or.inl h => intro hx; exact Or.inl (h hx)
+  | Or.inr h => intro hx; exact Or.inr (h hx)
 
-end ex_1_4_1
+end ex4_1
 
-section ex_1_4_2
+-- Exercises 4.2
 
-variables (α : Type*) (p q : α → Prop)
-variable r : Prop
+section ex4_2
 
-example : α → ((∀ x : α, r) ↔ r) :=
-begin
-  intro hα,
-  split,
-  { intro hαr, apply hαr, exact hα },
-  { intros hr hα, exact hr },
-end
+variable (α : Type _)
+variable (p q : α → Prop)
+variable (r : Prop)
+
+example : α → ((∀ _ : α, r) ↔ r) := by
+  intro ha
+  apply Iff.intro
+  · intro har
+    apply har
+    exact ha
+  · intro hr _
+    exact hr
 
 section
 
-open classical
+open Classical
 
-example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
-begin
-  split,
-  { intro h₁,
-    apply or.elim (classical.em r),
-    { intro hr, exact or.inr hr },
-    { intro nr,
-      exact or.inl begin
-        intro hx,
-        have h₂ : p hx ∨ r, from h₁ hx,
-        apply or.elim h₂,
-        { intro hp, exact hp },
-        { intro hr, exact absurd hr nr },
-      end
-    },
-  },
-  { assume h₁ hx,
-    apply or.elim h₁,
-    { assume h₂, exact or.inl (h₂ hx) },
-    { assume hr, exact or.inr hr },
-  },
-end
+example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := by
+  apply Iff.intro
+  · intro h
+    apply (em r).elim
+    · intro hr
+      exact Or.inr hr
+    · intro nr
+      apply Or.inl
+      · intro hx
+        apply (h hx).elim
+        · exact id
+        · intro hr
+          exact absurd hr nr
+  · intro h₁ hx
+    apply h₁.elim
+    · intro h₂
+      exact Or.inl (h₂ hx)
+    · intro hr
+      exact Or.inr hr
 
 end
 
-example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
-begin
-  split,
-  { intros h hr hx, exact h hx hr },
-  { intros h hx hr, exact h hr hx },
-end
+example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
+  apply Iff.intro
+  · intro h hr hx
+    exact h hx hr
+  · intro h hx hr
+    exact h hr hx
 
-end ex_1_4_2
+end ex4_2
 
-section ex_1_4_3
+-- Exercises 4.3
 
-open classical
+section ex4_3
 
-variables (men : Type*) (barber : men)
+open Classical
+
+variable (men : Type _)
+variable (barber : men)
 variable (shaves : men → men → Prop)
 
-example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) :
-  false :=
-begin
-  apply or.elim (classical.em (shaves barber barber)),
-  { intro hb,
-    apply iff.elim_left (h barber) hb,
-    exact hb,
-  },
-  { intro nb,
-    have s, from iff.elim_right (h barber) nb,
-    exact absurd s nb
-  },
-end
+example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := by
+  apply (em (shaves barber barber)).elim
+  · intro hb
+    exact absurd hb ((h barber).mp hb)
+  · intro nb
+    exact absurd ((h barber).mpr nb) nb
 
-end ex_1_4_3
+end ex4_3
 
-section ex_1_4_5
+-- Exercises 4.5
 
-open classical
+section ex4_5
 
-variables (α : Type*) (p q : α → Prop)
-variables r s : Prop
+open Classical
 
-example : (∃ x : α, r) → r :=
-begin
-  rintro ⟨hx, hr⟩,
-  exact hr,
-end
+variable (α : Type _)
+variable (p q : α → Prop)
+variable (r s : Prop)
 
-example (a : α) : r → (∃ x : α, r) :=
-begin
-  intro hr,
+example : (∃ _ : α, r) → r := by
+  intro ⟨_, hr⟩
+  exact hr
+
+example (a : α) : r → (∃ _ : α, r) := by
+  intro hr
   exact ⟨a, hr⟩
-end
 
-example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
-begin
-  split,
-  { rintro ⟨hx, ⟨hp, hr⟩⟩, exact ⟨⟨hx, hp⟩, hr⟩ },
-  { rintro ⟨⟨hx, hp⟩, hr⟩, exact ⟨hx, ⟨hp, hr⟩⟩ },
-end
+example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := by
+  apply Iff.intro
+  · intro ⟨hx, hp, hr⟩
+    exact ⟨⟨hx, hp⟩, hr⟩
+  · intro ⟨⟨hx, hp⟩, hr⟩
+    exact ⟨hx, hp, hr⟩
 
-example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
-begin
-  split,
-  { rintro ⟨hx, (hp | hq)⟩,
-    { exact or.inl ⟨hx, hp⟩ },
-    { exact or.inr ⟨hx, hq⟩ },
-  },
-  { rintro (⟨hx, hp⟩ | ⟨hx, hq⟩),
-    { exact ⟨hx, or.inl hp⟩ },
-    { exact ⟨hx, or.inr hq⟩ },
-  },
-end
+example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) := by
+  apply Iff.intro
+  · intro
+    | ⟨hx, Or.inl hp⟩ => exact Or.inl ⟨hx, hp⟩
+    | ⟨hx, Or.inr hq⟩ => exact Or.inr ⟨hx, hq⟩
+  · intro
+    | Or.inl ⟨hx, hp⟩ => exact ⟨hx, Or.inl hp⟩
+    | Or.inr ⟨hx, hq⟩ => exact ⟨hx, Or.inr hq⟩
 
-example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
-begin
-  split,
-  { rintros ha ⟨hx, np⟩, exact absurd (ha hx) np },
-  { intros he hx, by_contradiction np, exact he ⟨hx, np⟩ },
-end
+example : (∀ x, p x) ↔ ¬(∃ x, ¬p x) := by
+  apply Iff.intro
+  · intro ha ⟨hx, np⟩
+    exact absurd (ha hx) np
+  · intro he hx
+    apply byContradiction
+    intro np
+    exact he ⟨hx, np⟩
 
-example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
-begin
-  split,
-  { rintro ⟨hx, hp⟩ h, exact absurd hp (h hx) },
-  { intro h₁,
-    by_contradiction h₂,
-    apply h₁,
-    intros hx hp,
-    exact h₂ ⟨hx, hp⟩,
-  },
-end
-
-example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
-begin
-  split,
-  { intros h hx hp,
-    exact h ⟨hx, hp⟩
-  },
-  { rintros h ⟨hx, hp⟩,
+example : (∃ x, p x) ↔ ¬(∀ x, ¬p x) := by
+  apply Iff.intro
+  · intro ⟨hx, hp⟩ h
     exact absurd hp (h hx)
-  },
-end
+  · intro h₁
+    apply byContradiction
+    intro h₂
+    apply h₁
+    intro hx hp
+    exact h₂ ⟨hx, hp⟩
 
-lemma forall_negation : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
-begin
-  split,
-  { intro h₁,
-    by_contradiction h₂,
-    exact h₁ (λ (x : α), begin
-      by_contradiction np,
-      exact h₂ ⟨x, np⟩
-    end)
-  },
-  { rintros ⟨hx, np⟩ h, exact absurd (h hx) np },
-end
-
-example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := forall_negation α p
-
-example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
-begin
-  split,
-  { rintros h ⟨hx, hp⟩, exact h hx hp },
-  { intros h hx hp,
+example : (¬∃ x, p x) ↔ (∀ x, ¬p x) := by
+  apply Iff.intro
+  · intro h hx hp
     exact h ⟨hx, hp⟩
-  },
-end
+  · intro h ⟨hx, hp⟩
+    exact absurd hp (h hx)
 
-example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
-begin
-  split,
-  { rintros ⟨hx, hp⟩ h, apply hp, exact h hx },
-  { intro h₁,
-    apply or.elim (classical.em (∀ x, p x)),
-    { intro h₂, exact ⟨a, (assume hp, h₁ h₂)⟩ },
-    { intro h₂,
-      have h₃ : (∃ x, ¬p x), from iff.elim_left (forall_negation α p) h₂,
-      exact let ⟨hx, hp⟩ := h₃ in ⟨hx, (assume hp', absurd hp' hp)⟩,
-    },
-  },
-end
+theorem forall_negation : (¬∀ x, p x) ↔ (∃ x, ¬p x) := by
+  apply Iff.intro
+  · intro h₁
+    apply byContradiction
+    intro h₂
+    exact h₁ (fun (x : α) => by
+      apply byContradiction
+      intro np
+      exact h₂ ⟨x, np⟩)
+  · intro ⟨hx, np⟩ h
+    exact absurd (h hx) np
 
-example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
-begin
-  split,
-  { rintros ⟨hx, h⟩ hr, exact ⟨hx, h hr⟩ },
-  { intro h,
-    apply or.elim (classical.em r),
-    { intro hr,
-      exact let ⟨hx, hp⟩ := h hr in ⟨hx, (assume hr, hp)⟩
-    },
-    { intro nr, exact ⟨a, (assume hr, absurd hr nr)⟩ },
-  },
-end
+example : (¬∀ x, p x) ↔ (∃ x, ¬p x) := forall_negation α p
 
-end ex_1_4_5
+example : (∀ x, p x → r) ↔ (∃ x, p x) → r := by
+  apply Iff.intro
+  · intro h ⟨hx, hp⟩
+    exact h hx hp
+  · intro h hx hp
+    exact h ⟨hx, hp⟩
+
+example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := by
+  apply Iff.intro
+  · intro ⟨hx, hp⟩ h
+    apply hp
+    exact h hx
+  · intro h₁
+    apply (em (∀ x, p x)).elim
+    · intro h₂
+      exact ⟨a, fun _ => h₁ h₂⟩
+    · intro h₂
+      have ⟨hx, np⟩ : (∃ x, ¬p x) := (forall_negation α p).mp h₂
+      exact ⟨hx, fun hp => absurd hp np⟩
+
+example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) := by
+  apply Iff.intro
+  · intro ⟨hx, h⟩ hr
+    exact ⟨hx, h hr⟩
+  · intro h
+    apply (em r).elim
+    · intro hr
+      have ⟨hx, hp⟩ := h hr
+      exact ⟨hx, fun _ => hp⟩
+    · intro nr
+      exact ⟨a, fun hr => absurd hr nr⟩
+
+end ex4_5
+
+end ex1
 
 -- Exercise 2
 --
 -- Use tactic combinators to obtain a one line proof of the following:
-section ex_2
+namespace ex2
 
 example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
-by simp *
+by simp [*]
 
-end ex_2
+end ex2
diff --git a/src/theorem-proving-in-lean/exercises-7.lean b/src/theorem-proving-in-lean/exercises-7.lean
index 57c053d..472090e 100644
--- a/src/theorem-proving-in-lean/exercises-7.lean
+++ b/src/theorem-proving-in-lean/exercises-7.lean
@@ -1,8 +1,7 @@
-/- Exercises 7.10
+/- Exercises 7
  -
  - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
-import data.nat.basic
 
 -- Exercise 1
 --
@@ -15,41 +14,63 @@ import data.nat.basic
 -- Since many of these are already defined in Lean’s core library, you should
 -- work within a namespace named hide, or something like that, in order to avoid
 -- name clashes.
-namespace ex_1
+namespace ex1
 
 -- As defined in the book.
-inductive nat : Type
-| zero : nat
-| succ : nat → nat
+inductive Nat where
+  | zero : Nat
+  | succ : Nat → Nat
 
-def add (m n : nat) : nat :=
-nat.rec_on n m (λ k ak, nat.succ ak)
+namespace Nat
 
-theorem add_zero (m : nat) : add m nat.zero = m := rfl
-theorem add_succ (m n : nat) : add m n.succ = (add m n).succ := rfl
+def add (m n : Nat) : Nat :=
+  match n with
+  | Nat.zero => m
+  | Nat.succ n => Nat.succ (add m n)
 
-theorem zero_add (n : nat) : add nat.zero n = n :=
-nat.rec_on n
-  (add_zero nat.zero)
-  (assume n ih,
-    show add nat.zero (nat.succ n) = nat.succ n, from calc
-      add nat.zero (nat.succ n) = nat.succ (add nat.zero n) : add_succ nat.zero n
-                            ... = nat.succ n : by rw ih)
+instance : Add Nat where
+  add := add
+
+theorem addZero (m : Nat) : m + Nat.zero = m :=
+  rfl
+
+theorem addSucc (m n : Nat) : m + n.succ = (m + n).succ :=
+  rfl
+
+theorem zeroAdd (n : Nat) : Nat.zero + n = n :=
+Nat.recOn (motive := fun x => Nat.zero + x = x)
+  n
+  (show Nat.zero + Nat.zero = Nat.zero from rfl)
+  (fun (n : Nat) (ih : Nat.zero + n = n) =>
+    show Nat.zero + n.succ = n.succ from
+    calc
+      Nat.zero + n.succ = (Nat.zero + n).succ := addSucc Nat.zero n
+                      _ = n.succ := by rw [ih])
 
 -- Additional definitions.
-def mul (m n : nat) : nat :=
-nat.rec_on n nat.zero (λ k ak, add m ak)
+def mul (m n : Nat) : Nat := sorry
 
-def pred (n : nat) : nat :=
-nat.cases_on n nat.zero id
+-- def mul (m n : nat) : nat :=
+-- nat.rec_on n nat.zero (λ k ak, add m ak)
 
-def sub (m n : nat) : nat :=
-nat.rec_on n m (λ k ak, pred ak)
+def pred (n : Nat) : Nat := sorry
 
-def exp (m n : nat) : nat :=
-nat.rec_on n (nat.zero.succ) (λ k ak, mul m ak)
+-- def pred (n : nat) : nat :=
+-- nat.cases_on n nat.zero id
 
-end ex_1
+def sub (m n : Nat) : Nat := sorry
+
+-- def sub (m n : nat) : nat :=
+-- nat.rec_on n m (λ k ak, pred ak)
+
+def exp (m n : Nat) : Nat := sorry
+
+-- def exp (m n : nat) : nat :=
+-- nat.rec_on n (nat.zero.succ) (λ k ak, mul m ak)
+
+end Nat
+
+end ex1
 
 -- Exercise 2
 --
@@ -59,46 +80,45 @@ end ex_1
 -- a. `length (s ++ t) = length s + length t`
 -- b. `length (reverse t) = length t`
 -- c. `reverse (reverse t) = t`
-section ex_2
+namespace ex2
 
-open list
+open List
 
-variable {α : Type*}
+variable {α : Type _}
 
--- Additional theorems.
-theorem length_sum (s t : list α) : length (s ++ t) = length s + length t :=
-list.rec_on s
-  (by rw [nil_append, length, zero_add])
-  (assume hd tl ih, by rw [
-    length,
-    cons_append,
-    length,
-    ih,
-    add_assoc,
-    add_comm t.length,
-    add_assoc
-  ])
+-- theorem length_sum (s t : list α) : length (s ++ t) = length s + length t :=
+-- list.rec_on s
+--   (by rw [nil_append, length, zero_add])
+--   (assume hd tl ih, by rw [
+--     length,
+--     cons_append,
+--     length,
+--     ih,
+--     add_assoc,
+--     add_comm t.length,
+--     add_assoc
+--   ])
+-- 
+-- lemma cons_reverse (hd : α) (tl : list α)
+--   : reverse (hd :: tl) = reverse tl ++ [hd] :=
+-- sorry
+-- 
+-- theorem length_reverse (t : list α) : length (reverse t) = length t :=
+-- list.rec_on t
+--   (by unfold reverse reverse_core)
+--   (assume hd tl ih, begin
+--     unfold length,
+--     rw cons_reverse,
+--     rw length_sum,
+--     unfold length,
+--     rw zero_add,
+--     rw ih,
+--   end)
+-- 
+-- theorem reverse_reverse (t : list α) : reverse (reverse t) = t :=
+-- list.rec_on t rfl (assume hd tl ih, sorry)
 
-lemma cons_reverse (hd : α) (tl : list α)
-  : reverse (hd :: tl) = reverse tl ++ [hd] :=
-sorry
-
-theorem length_reverse (t : list α) : length (reverse t) = length t :=
-list.rec_on t
-  (by unfold reverse reverse_core)
-  (assume hd tl ih, begin
-    unfold length,
-    rw cons_reverse,
-    rw length_sum,
-    unfold length,
-    rw zero_add,
-    rw ih,
-  end)
-
-theorem reverse_reverse (t : list α) : reverse (reverse t) = t :=
-list.rec_on t rfl (assume hd tl ih, sorry)
-
-end ex_2
+end ex2
 
 -- Exercise 3
 --
@@ -112,27 +132,27 @@ end ex_2
 --
 -- Recursively define a function that evaluates any such term with respect to an
 -- assignment of values to the variables.
-namespace ex_3
+namespace ex3
 
-inductive foo : Type*
-| const : ℕ → foo
-| var : ℕ → foo
-| plus : foo → foo → foo
-| times : foo → foo → foo
+-- inductive foo : Type*
+-- | const : ℕ → foo
+-- | var : ℕ → foo
+-- | plus : foo → foo → foo
+-- | times : foo → foo → foo
+-- 
+-- def value_at : ℕ → list ℕ → ℕ
+-- | 0       vs := list.head vs
+-- | i       [] := default
+-- | (i + 1) vs := value_at i (list.tail vs)
+-- 
+-- -- The provided "variables" are supplied in a 0-indexed list.
+-- def eval_foo : foo → list ℕ → ℕ
+-- | (foo.const n) vs := n
+-- | (foo.var n) vs := value_at n vs
+-- | (foo.plus m n) vs := eval_foo m vs + eval_foo n vs
+-- | (foo.times m n) vs := eval_foo m vs * eval_foo n vs
 
-def value_at : ℕ → list ℕ → ℕ
-| 0       vs := list.head vs
-| i       [] := default
-| (i + 1) vs := value_at i (list.tail vs)
-
--- The provided "variables" are supplied in a 0-indexed list.
-def eval_foo : foo → list ℕ → ℕ
-| (foo.const n) vs := n
-| (foo.var n) vs := value_at n vs
-| (foo.plus m n) vs := eval_foo m vs + eval_foo n vs
-| (foo.times m n) vs := eval_foo m vs * eval_foo n vs
-
-end ex_3
+end ex3
 
 -- Exercise 4
 --
@@ -140,35 +160,35 @@ end ex_3
 -- the type of such formulas: an evaluation function, functions that measure the
 -- complexity of a formula, and a function that substitutes another formula for
 -- a given variable.
-namespace ex_4
+namespace ex4
 
-inductive foo : Type*
-| tt : foo
-| ff : foo
-| and : foo → foo → foo
-| or : foo → foo → foo
+-- inductive foo : Type*
+-- | tt : foo
+-- | ff : foo
+-- | and : foo → foo → foo
+-- | or : foo → foo → foo
+-- 
+-- def eval_foo : foo → bool
+-- | foo.tt := true
+-- | foo.ff := false
+-- | (foo.and lhs rhs) := eval_foo lhs ∧ eval_foo rhs
+-- | (foo.or lhs rhs) := eval_foo lhs ∨ eval_foo rhs
+-- 
+-- def complexity_foo : foo → ℕ
+-- | foo.tt := 1
+-- | foo.ff := 1
+-- | (foo.and lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
+-- | (foo.or lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
+--
+-- def substitute : foo → foo := sorry
 
-def eval_foo : foo → bool
-| foo.tt := true
-| foo.ff := false
-| (foo.and lhs rhs) := eval_foo lhs ∧ eval_foo rhs
-| (foo.or lhs rhs) := eval_foo lhs ∨ eval_foo rhs
-
-def complexity_foo : foo → ℕ
-| foo.tt := 1
-| foo.ff := 1
-| (foo.and lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
-| (foo.or lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
-
-def substitute : foo → foo := sorry
-
-end ex_4
+end ex4
 
 -- Exercise 5
 --
 -- Simulate the mutual inductive definition of `even` and `odd` described in
 -- Section 7.9 with an ordinary inductive type, using an index to encode the
 -- choice between them in the target type.
-section ex_5
+namespace ex5
 
-end ex_5
+end ex5