From a28a8cfa5787ac84a045c6ee2d98e6d79df459e6 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 1 Mar 2024 20:53:34 +0100
Subject: [PATCH] fix: Update examples to work with latest Lean nightly

---
 axioms_and_computation.md   |  5 +++--
 propositions_and_proofs.md  |  4 ++--
 quantifiers_and_equality.md | 28 +++++++++-------------------
 3 files changed, 14 insertions(+), 23 deletions(-)

diff --git a/axioms_and_computation.md b/axioms_and_computation.md
index c11ac6f1..4285b10d 100644
--- a/axioms_and_computation.md
+++ b/axioms_and_computation.md
@@ -735,7 +735,7 @@ private theorem mem_swap {a : α} :
 private theorem mem_respects
       : {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
   | (a₁, a₂), (b₁, b₂), a, Or.inl ⟨a₁b₁, a₂b₂⟩ => by simp_all
-  | (a₁, a₂), (b₁, b₂), a, Or.inr ⟨a₁b₂, a₂b₁⟩ => by simp_all; apply mem_swap
+  | (a₁, a₂), (b₁, b₂), a, Or.inr ⟨a₁b₂, a₂b₁⟩ => by simp_all; rw [mem_swap]
 
 def mem (a : α) (u : UProd α) : Prop :=
   Quot.liftOn u (fun p => mem_fn a p) (fun p₁ p₂ e => mem_respects a e)
@@ -1100,10 +1100,11 @@ theorem linv_comp_self {f : α → β} [Inhabited α]
     have ex  : ∃ a₁ : α, f a₁ = f a := ⟨a, rfl⟩
     have feq : f (choose ex) = f a  := choose_spec ex
     calc linv f (f a)
-      _ = choose ex := dif_pos ex
+      _ = choose ex := by simp
       _ = a         := inj feq
 ```
 
+
 From a classical point of view, ``linv`` is a function. From a
 constructive point of view, it is unacceptable; because there is no
 way to implement such a function in general, the construction is not
diff --git a/propositions_and_proofs.md b/propositions_and_proofs.md
index 18a22de7..403ea0c1 100644
--- a/propositions_and_proofs.md
+++ b/propositions_and_proofs.md
@@ -43,10 +43,10 @@ constant of such a type.
 #   proof : p
 #check Proof   -- Proof : Prop → Type
 
-axiom and_comm (p q : Prop) : Proof (Implies (And p q) (And q p))
+axiom and_commutative (p q : Prop) : Proof (Implies (And p q) (And q p))
 
 variable (p q : Prop)
-#check and_comm p q     -- Proof (Implies (And p q) (And q p))
+#check and_commutative p q     -- Proof (Implies (And p q) (And q p))
 ```
 
 In addition to axioms, however, we would also need rules to build new
diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md
index a092eb99..ca68ff96 100644
--- a/quantifiers_and_equality.md
+++ b/quantifiers_and_equality.md
@@ -477,40 +477,30 @@ of the `Trans` type class. Type classes are introduced later, but the following
 small example demonstrates how to extend the `calc` notation using new `Trans` instances.
 
 ```lean
-def divides (x y : Nat) : Prop :=
+def Divides (x y : Nat) : Prop :=
   ∃ k, k*x = y
 
-def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z :=
+def Divides_trans (h₁ : Divides x y) (h₂ : Divides y z) : Divides x z :=
   let ⟨k₁, d₁⟩ := h₁
   let ⟨k₂, d₂⟩ := h₂
   ⟨k₁ * k₂, by rw [Nat.mul_comm k₁ k₂, Nat.mul_assoc, d₁, d₂]⟩
 
-def divides_mul (x : Nat) (k : Nat) : divides x (k*x) :=
+def Divides_mul (x : Nat) (k : Nat) : Divides x (k*x) :=
   ⟨k, rfl⟩
 
-instance : Trans divides divides divides where
-  trans := divides_trans
+instance : Trans Divides Divides Divides where
+  trans := Divides_trans
 
-example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
+example (h₁ : Divides x y) (h₂ : y = z) : Divides x (2*z) :=
   calc
-    divides x y     := h₁
+    Divides x y     := h₁
     _ = z           := h₂
-    divides _ (2*z) := divides_mul ..
+    Divides _ (2*z) := Divides_mul ..
 
-infix:50 " ∣ " => divides
-
-example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
-  calc
-    x ∣ y   := h₁
-    _ = z   := h₂
-    _ ∣ 2*z := divides_mul ..
 ```
 
 The example above also makes it clear that you can use `calc` even if you
-do not have an infix notation for your relation. Finally we remark that
-the vertical bar `∣` in the example above is the unicode one. We use
-unicode to make sure we do not overload the ASCII `|` used in the
-`match .. with` expression.
+do not have an infix notation for your relation.
 
 With ``calc``, we can write the proof in the last section in a more
 natural and perspicuous way.