diff --git a/quantifiers_and_equality.lean b/quantifiers_and_equality.lean
new file mode 100644
index 0000000..59eee11
--- /dev/null
+++ b/quantifiers_and_equality.lean
@@ -0,0 +1,147 @@
+--
+-- 4. Quantifiers and Equality
+--
+
+-- The Universal Quantifier
+
+example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y :=
+  fun h : ∀ x : α, p x ∧ q x =>
+  fun y : α =>
+  show p y from (h y).left
+
+variable (α : Type) (r : α → α → Prop)
+variable (trans_r : ∀ {x y z}, r x y → r y z → r x z)
+
+variable (a b c : α)
+variable (hab : r a b) (hbc : r b c)
+
+#check trans_r
+#check @trans_r
+#check trans_r hab
+#check trans_r hab hbc
+
+-- Equality
+
+#check Eq.refl
+#check Eq.symm
+#check Eq.trans
+
+universe u
+#check @Eq.refl.{u}
+#check @Eq.symm.{u}
+#check @Eq.trans.{u}
+
+variable (a b c d : α)
+variable (hab : a = b) (hcb : c = b) (hcd : c = d)
+
+example : a = d :=
+  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
+example : a = d := (hab.trans hcb.symm).trans hcd
+
+variable (α β : Type)
+
+example (f : α → β) (a : α) : (fun x => f x) a = f a := Eq.refl _
+example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl
+
+example (α : Type) (a b : α) (p : α → Prop)
+        (h1 : a = b) (h2 : p a) : p b :=
+  Eq.subst h1 h2
+
+example (α : Type) (a b : α) (p : α → Prop)
+        (h1 : a = b) (h2 : p a) : p b :=
+  h1 ▸ h2
+
+variable (α : Type)
+variable (a b : α)
+variable (f g : α → Nat)
+variable (h₁ : a = b)
+variable (h₂ : f = g)
+
+example : f a = f b := congrArg f h₁
+example : f a = g a := congrFun h₂ a
+
+variable (a : Nat) in
+example : a + 0 = a := Nat.add_zero a
+
+-- Calculational Proofs
+variable (a b c d : Nat) in
+variable (h1 : a = b) in
+variable (h2 : b = c + 1) in
+variable (h3 : c = d) in
+variable (h4 : e = 1 + d) in
+theorem T : a = e :=
+  calc
+    a = b     := h1
+    _ = c + 1 := h2
+    _ = d + 1 := congrArg Nat.succ h3
+    _ = 1 + d := Nat.add_comm d 1
+    _ = e     := h4.symm
+
+-- The Existential Quantifier
+example : ∃ x : Nat, x > 0 :=
+  have h : 1 > 0 := Nat.zero_lt_succ 0
+  Exists.intro 1 h
+
+variable (α : Type) (p q : α → Prop) in
+example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
+  Exists.elim h
+    fun w =>
+    fun hw : p w ∧ q w => 
+    Exists.intro w ⟨hw.right, hw.left⟩
+
+#check @Exists.elim.{u}
+
+#check Sigma
+
+variable (α : Type) (p q : α → Prop) in
+example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
+  match h with
+  | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩
+
+
+-- More on the Proof Language
+variable (f : Nat → Nat)
+variable (h : ∀ x : Nat, f x ≤ f (x + 1))
+
+example : f 0 ≤ f 3 :=
+  have : f 0 ≤ f 1 := h 0
+  have : f 0 ≤ f 2 := Nat.le_trans (by assumption) (h 1)
+  show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2)
+
+example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
+  fun _ : f 0 ≥ f 1 =>
+  fun _ : f 1 ≥ f 2 =>
+  have : f 0 ≥ f 2 := Nat.le_trans ‹f 1 ≥ f 2› ‹f 0 ≥ f 1›
+  have : f 0 ≤ f 2 := Nat.le_trans (h 0) (h 1)
+  show f 0 = f 2 from Nat.le_antisymm this ‹f 0 ≥ f 2›
+
+-- Exercises
+variable (α : Type) (p q : α → Prop)
+
+example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
+  have h1 : (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x :=
+    fun h =>
+      have h11 : ∀ (x : α), p x :=
+        fun x : α => (h x).left
+      have h12 : ∀ (x : α), q x :=
+        fun x : α => (h x).right
+      And.intro h11 h12
+  have h2 : ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x :=
+    fun h =>
+      fun x : α =>
+        ⟨h.left x, h.right x⟩
+  Iff.intro h1 h2
+example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
+  fun h1 =>
+  fun h2 =>
+  fun x : α =>
+    show q x from (h1 x) (h2 x)
+
+example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
+  fun h =>
+    h.elim
+      (fun hp =>
+        fun x => Or.inl (hp x))
+      (fun hq =>
+        fun x => Or.inr (hq x))
+
diff --git a/tactics.lean b/tactics.lean
new file mode 100644
index 0000000..b40a5f3
--- /dev/null
+++ b/tactics.lean
@@ -0,0 +1,9 @@
+--
+-- 5. Tactics
+--
+
+--
+theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
+  apply And.intro
+  exact hp
+  exact { left := hq, right := hp }