The rationals

Analysis I, Section 4.2

This file is a translation of Section 4.2 of Analysis I to Lean 4. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Definition of the "Section 4.2" rationals, Section_4_2.Rat : TypeSection_4_2.Rat, as formal quotients Unknown identifier `a`sorry // sorry : Section_4_2.Rata // Unknown identifier `b`b of integers , up to equivalence. (This is a quotient of a scaffolding type Section_4_2.PreRat : TypeSection_4_2.PreRat, which consists of formal quotients without any equivalence imposed.)
Field operations and order on these rationals, as well as an embedding of ℕ and ℤ.
Equivalence with the Mathlib rationals Rat : Type_root_.Rat (or ℚ : Typeℚ), which we will use going forward.

Note: here (and in the sequel) we use Mathlib's natural numbers ℕ : Typeℕ and integers ℤ : Typeℤ rather than the Chapter 2 natural numbers and Section 4.1 integers.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Section_4_2

structure PreRat where
  numerator : ℤ
  denominator : ℤ
  nonzero : denominator ≠ 0

Exercise 4.2.1

instance declaration uses 'sorry'PreRat.instSetoid : Setoid PreRat where
  r a b := a.numerator * b.denominator = b.numerator * a.denominator
  iseqv := {
    refl := by⊢ ∀ (x : PreRat), x.numerator * x.denominator = x.numerator * x.denominator sorryAll goals completed! 🐙
    symm := by⊢ ∀ {x y : PreRat},
  x.numerator * y.denominator = y.numerator * x.denominator → y.numerator * x.denominator = x.numerator * y.denominator sorryAll goals completed! 🐙
    trans := by⊢ ∀ {x y z : PreRat},
  x.numerator * y.denominator = y.numerator * x.denominator →
    y.numerator * z.denominator = z.numerator * y.denominator →
      x.numerator * z.denominator = z.numerator * x.denominator sorryAll goals completed! 🐙
    }

@[simp]
theorem PreRat.eq (a b c d:ℤ) (hb: b ≠ 0) (hd: d ≠ 0) :
    (⟨ a,b,hb ⟩: PreRat) ≈ ⟨ c,d,hd ⟩ ↔ a * d = c * b := bya:ℤb:ℤc:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ { numerator := a, denominator := b, nonzero := hb } ≈ { numerator := c, denominator := d, nonzero := hd } ↔
  a * d = c * b rflAll goals completed! 🐙

abbrev Rat := Quotient PreRat.instSetoid

We give division a "junk" value of 0//1 if the denominator is zero

abbrev Rat.formalDiv (a b:ℤ) : Rat :=
  Quotient.mk PreRat.instSetoid (if h:b ≠ 0 then ⟨ a,b,h ⟩ else ⟨ 0, 1, bya:ℤb:ℤh:¬b ≠ 0⊢ 1 ≠ 0 decideAll goals completed! 🐙 ⟩)

infix:100 " // " => Rat.formalDiv

Definition 4.2.1 (Rationals)

theorem Rat.eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0): a // b = c // d ↔ a * d = c * b := bya:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a // b = c // d ↔ a * d = c * b
  simp [hb, hd, Setoid.r]All goals completed! 🐙

Definition 4.2.1 (Rationals)

theorem Rat.eq_diff (n:Rat) : ∃ a b, b ≠ 0 ∧ n = a // b := byn:Rat⊢ ∃ a b, b ≠ 0 ∧ n = a // b
  apply Quotient.ind _ nn:Rat⊢ ∀ (a : PreRat), ∃ a_1 b, b ≠ 0 ∧ ⟦a⟧ = a_1 // b; intro ⟨ a, b, h ⟩n:Rata:ℤb:ℤh:b ≠ 0⊢ ∃ a_1 b_1, b_1 ≠ 0 ∧ ⟦{ numerator := a, denominator := b, nonzero := h }⟧ = a_1 // b_1
  refine ⟨ a, b, h, ?_ ⟩n:Rata:ℤb:ℤh:b ≠ 0⊢ ⟦{ numerator := a, denominator := b, nonzero := h }⟧ = a // b
  simp [formalDiv, h]All goals completed! 🐙

Decidability of equality. Hint: modify the proof of DecidableEq ℤ : TypeDecidableEq Int from the previous section. However, because formal division handles the case of zero denominator separately, it may be more convenient to avoid that operation and work directly with the Quotient.{u} {α : Sort u} (s : Setoid α) : Sort uQuotient API.

instance declaration uses 'sorry'Rat.decidableEq : DecidableEq Rat := by⊢ DecidableEq Rat
  sorryAll goals completed! 🐙

Lemma 4.2.3 (Addition well-defined)

instance Rat.add_inst : Add Rat where
  add := Quotient.lift₂ (fun ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ↦ (a*d+b*c) // (b*d)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreRat),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
          a₂ b₂
    intro ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ⟨ a', b', h1' ⟩ ⟨ c', d', h2' ⟩ h3 h4a:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:{ numerator := a, denominator := b, nonzero := h1 } ≈ { numerator := a', denominator := b', nonzero := h1' }h4:{ numerator := c, denominator := d, nonzero := h2 } ≈ { numerator := c', denominator := d', nonzero := h2' }⊢ (fun x x_1 =>
      match x with
      | { numerator := a, denominator := b, nonzero := h1 } =>
        match x_1 with
        | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
    { numerator := a, denominator := b, nonzero := h1 } { numerator := c, denominator := d, nonzero := h2 } =
  (fun x x_1 =>
      match x with
      | { numerator := a, denominator := b, nonzero := h1 } =>
        match x_1 with
        | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
    { numerator := a', denominator := b', nonzero := h1' } { numerator := c', denominator := d', nonzero := h2' }
    simp_all [Setoid.r]a:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ (a * d + b * c) * (b' * d') = (a' * d' + b' * c') * (b * d)
    calc
      _ = (a*b')*d*d' + b*b'*(c*d') := bya:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ (a * d + b * c) * (b' * d') = a * b' * d * d' + b * b' * (c * d') ringAll goals completed! 🐙
      _ = (a'*b)*d*d' + b*b'*(c'*d) := bya:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ a * b' * d * d' + b * b' * (c * d') = a' * b * d * d' + b * b' * (c' * d) rw [h3, h4]All goals completed! 🐙
      _ = _ := bya:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ a' * b * d * d' + b * b' * (c' * d) = (a' * d' + b' * c') * (b * d) ringAll goals completed! 🐙
  )

Definition 4.2.2 (Addition of rationals)

theorem Rat.add_eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0) :
    (a // b) + (c // d) = (a*d + b*c) // (b*d) := bya:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a // b + c // d = (a * d + b * c) // (b * d)
  convert Quotient.lift₂_mk _ _ _ _h.e'_3.h.e'_1.h.e'_5.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_5.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator <;>h.e'_3.h.e'_1.h.e'_5.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_5.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator simp [hb, hd]All goals completed! 🐙

Lemma 4.2.3 (Multiplication well-defined)

instance declaration uses 'sorry'Rat.mul_inst : Mul Rat where
  mul := Quotient.lift₂ (fun ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ↦ (a*c) // (b*d)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreRat),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * c) // (b * d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * c) // (b * d))
          a₂ b₂ sorryAll goals completed! 🐙)

Definition 4.2.2 (Multiplication of rationals)

theorem Rat.mul_eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0) :
    (a // b) * (c // d) = (a*c) // (b*d) := bya:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a // b * c // d = (a * c) // (b * d)
  convert Quotient.lift₂_mk _ _ _ _h.e'_3.h.e'_1.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator <;>h.e'_3.h.e'_1.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator simp [hb, hd]All goals completed! 🐙

Lemma 4.2.3 (Negation well-defined)

instance declaration uses 'sorry'Rat.neg_inst : Neg Rat where
  neg := Quotient.lift (fun ⟨ a, b, h1 ⟩ ↦ (-a) // b) (by⊢ ∀ (a b : PreRat),
  a ≈ b →
    (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => (-a) // b)
        a =
      (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => (-a) // b)
        b sorryAll goals completed! 🐙)

Definition 4.2.2 (Negation of rationals)

theorem Rat.neg_eq (a:ℤ) {b:ℤ} (hb: b ≠ 0) : - (a // b) = (-a) // b := bya:ℤb:ℤhb:b ≠ 0⊢ -a // b = (-a) // b
  convert Quotient.lift_mk _ _ _h.e'_3.h.e'_1.h.e'_3a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator <;>h.e'_3.h.e'_1.h.e'_3a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator simp [hb]All goals completed! 🐙

Embedding the integers in the rationals

instance Rat.instIntCast : IntCast Rat where
  intCast a := a // 1

instance Rat.instNatCast : NatCast Rat where
  natCast n := (n:ℤ) // 1

instance Rat.instOfNat {n:ℕ} : OfNat Rat n where
  ofNat := (n:ℤ) // 1

theorem Rat.coe_Int_eq (a:ℤ) : (a:Rat) = a // 1 := rfltheorem Rat.coe_Nat_eq (n:ℕ) : (n:Rat) = n // 1 := rfltheorem Rat.of_Nat_eq (n:ℕ) : (ofNat(n):Rat) = (ofNat(n):Nat) // 1 := rfl

natCast distributes over successor

theorem declaration uses 'sorry'Rat.natCast_succ (n: ℕ) : ((n + 1: ℕ): Rat) = (n: Rat) + 1 := byn:ℕ⊢ ↑(n + 1) = ↑n + 1 sorryAll goals completed! 🐙

intCast distributes over addition

lemma declaration uses 'sorry'Rat.intCast_add (a b:ℤ) : (a:Rat) + (b:Rat) = (a+b:ℤ) := bya:ℤb:ℤ⊢ ↑a + ↑b = ↑(a + b) sorryAll goals completed! 🐙

intCast distributes over multiplication

lemma declaration uses 'sorry'Rat.intCast_mul (a b:ℤ) : (a:Rat) * (b:Rat) = (a*b:ℤ) := bya:ℤb:ℤ⊢ ↑a * ↑b = ↑(a * b) sorryAll goals completed! 🐙

intCast commutes with negation

lemma Rat.intCast_neg (a:ℤ) : - (a:Rat) = (-a:ℤ) := rfl

theorem declaration uses 'sorry'Rat.coe_Int_inj : Function.Injective (fun n:ℤ ↦ (n:Rat)) := by⊢ Function.Injective fun n => ↑n sorryAll goals completed! 🐙

Whereas the book leaves the inverse of 0 undefined, it is more convenient in Lean to assign a "junk" value to this inverse; we arbitrarily choose this junk value to be 0.

instance declaration uses 'sorry'Rat.instInv : Inv Rat where
  inv := Quotient.lift (fun ⟨ a, b, h1 ⟩ ↦ b // a) (by⊢ ∀ (a b : PreRat),
  a ≈ b →
    (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => b // a)
        a =
      (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => b // a)
        b
    sorryAll goals completed! 🐙 -- hint: split into the `a=0` and `a≠0` cases
)

lemma Rat.inv_eq (a:ℤ) {b:ℤ} (hb: b ≠ 0) : (a // b)⁻¹ = b // a := bya:ℤb:ℤhb:b ≠ 0⊢ (a // b)⁻¹ = b // a
  convert Quotient.lift_mk _ _ _h.e'_3.h.e'_1a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numerator <;>h.e'_3.h.e'_1a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numerator simp [hb]All goals completed! 🐙

@[simp]
theorem Rat.inv_zero : (0:Rat)⁻¹ = 0 := rfl

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

instance declaration uses 'sorry'declaration uses 'sorry'Rat.addGroup_inst : AddGroup Rat :=
AddGroup.ofLeftAxioms (by⊢ ∀ (a b c : Rat), a + b + c = a + (b + c)
  -- this proof is written to follow the structure of the original text.
  intro x y zx:Raty:Ratz:Rat⊢ x + y + z = x + (y + z)
  obtain ⟨ a, b, hb, rfl ⟩ := eq_diff xintro.intro.introy:Ratz:Rata:ℤb:ℤhb:b ≠ 0⊢ a // b + y + z = a // b + (y + z)
  obtain ⟨ c, d, hd, rfl ⟩ := eq_diff yintro.intro.intro.intro.intro.introz:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0⊢ a // b + c // d + z = a // b + (c // d + z)
  obtain ⟨ e, f, hf, rfl ⟩ := eq_diff zintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0⊢ a // b + c // d + e // f = a // b + (c // d + e // f)
  have hbd : b*d ≠ 0 := Int.mul_ne_zero hb hdintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672⊢ a // b + c // d + e // f = a // b + (c // d + e // f)     -- can also use `observe hbd : b*d ≠ 0` here
  have hdf : d*f ≠ 0 := Int.mul_ne_zero hd hfintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672hdf:_fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38672 _fvar.38744⊢ a // b + c // d + e // f = a // b + (c // d + e // f)     -- can also use `observe hdf : d*f ≠ 0` here
  have hbdf : b*d*f ≠ 0 := Int.mul_ne_zero hbd hfintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672hdf:_fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38672 _fvar.38744hbdf:_fvar.38578 * _fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38859 _fvar.38744⊢ a // b + c // d + e // f = a // b + (c // d + e // f) -- can also use `observe hbdf : b*d*f ≠ 0` here
  rw [add_eq _ _ hb hd, add_eq _ _ hbd hf, add_eq _ _ hd hf,
      add_eq _ _ hb hdf, ←mul_assoc b, eq _ _ hbdf hbdf]intro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672hdf:_fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38672 _fvar.38744hbdf:_fvar.38578 * _fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38859 _fvar.38744⊢ ((a * d + b * c) * f + b * d * e) * (b * d * f) = (a * (d * f) + b * (c * f + d * e)) * (b * d * f)
  ringAll goals completed! 🐙
)
 (by⊢ ∀ (a : Rat), 0 + a = a sorryAll goals completed! 🐙) (by⊢ ∀ (a : Rat), -a + a = 0 sorryAll goals completed! 🐙)

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

instance declaration uses 'sorry'Rat.instAddCommGroup : AddCommGroup Rat where
  add_comm := by⊢ ∀ (a b : Rat), a + b = b + a sorryAll goals completed! 🐙

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.instCommMonoid : CommMonoid Rat where
  mul_comm := by⊢ ∀ (a b : Rat), a * b = b * a sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Rat), a * b * c = a * (b * c) sorryAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : Rat), 1 * a = a sorryAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : Rat), a * 1 = a sorryAll goals completed! 🐙

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.instCommRing : CommRing Rat where
  left_distrib := by⊢ ∀ (a b c : Rat), a * (b + c) = a * b + a * c sorryAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : Rat), (a + b) * c = a * c + b * c sorryAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : Rat), 0 * a = 0 sorryAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : Rat), a * 0 = 0 sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Rat), a * b * c = a * (b * c) sorryAll goals completed! 🐙
  -- Usually CommRing will generate a natCast instance and a proof for this.
  -- However, we are using a custom natCast for which `natCast_succ` cannot
  -- be proven automatically by `rfl`. Luckily we have proven it already.
  natCast_succ := natCast_succ

instance Rat.instRatCast : RatCast Rat where
  ratCast q := q.num // q.den

theorem declaration uses 'sorry'Rat.ratCast_inj : Function.Injective (fun n:ℚ ↦ (n:Rat)) := by⊢ Function.Injective fun n => ↑n sorryAll goals completed! 🐙

theorem Rat.coe_Rat_eq (a:ℤ) {b:ℤ} (hb: b ≠ 0) : (a/b:ℚ) = a // b := bya:ℤb:ℤhb:b ≠ 0⊢ ↑(↑a / ↑b) = a // b
  set q := (a/b:ℚ)a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388⊢ ↑q = a // b
  set num :ℤ := q.numa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = a // b
  set den :ℤ := (q.den:ℤ)a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = a // b
  have hden : den ≠ 0 := bya:ℤb:ℤhb:b ≠ 0⊢ ↑(↑a / ↑b) = a // b simp [den, q.den_nz]All goals completed! 🐙
  change num // den = a // ba:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808⊢ num // den = a // b
  rw [eq _ _ hden hb]a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808⊢ num * b = a * den
  qifya:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808⊢ ↑num * ↑b = ↑a * ↑den
  have hq : num / den = q := Rat.num_div_den qa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑num * ↑b = ↑a * ↑den
  rwa [div_eq_div_iff]a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑num * ↑b = ↑a * ↑den⊢ ↑num * ↑b = ↑a * ↑denhba:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑den ≠ 0hda:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑b ≠ 0 at hq <;>hba:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑den ≠ 0hda:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑b ≠ 0 simp [hden, hb]All goals completed! 🐙

Default definition of division

instance Rat.instDivInvMonoid : DivInvMonoid Rat where

theorem Rat.div_eq (q r:Rat) : q/r = q * r⁻¹ := byq:Ratr:Rat⊢ q / r = q * r⁻¹ rflAll goals completed! 🐙

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

instance declaration uses 'sorry'declaration uses 'sorry'Rat.instField : Field Rat where
  exists_pair_ne := by⊢ ∃ x y, x ≠ y sorryAll goals completed! 🐙
  mul_inv_cancel := by⊢ ∀ (a : Rat), a ≠ 0 → a * a⁻¹ = 1 sorryAll goals completed! 🐙
  inv_zero := rfl
  ratCast_def := by⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
    intro qq:ℚ⊢ ↑q = ↑q.num / ↑q.den
    set num := q.numq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = ↑num / ↑q.den
    set den := q.denq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = ↑num / ↑den
    have hden : (den:ℤ) ≠ 0 := by⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den simp [den, q.den_nz]All goals completed! 🐙
    rw [← Rat.num_div_den q]q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑(↑q.num / ↑q.den) = ↑num / ↑den
    convert coe_Rat_eq _ hdenh.e'_3q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑num / ↑den = q.num // ↑den
    rw [coe_Int_eq, coe_Nat_eq, div_eq, inv_eq, mul_eq, eq]h.e'_3q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ num * 1 * ↑den = q.num * (1 * ↑den)h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 * ↑den ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0 <;>h.e'_3q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ num * 1 * ↑den = q.num * (1 * ↑den)h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 * ↑den ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0 simp [num, den, q.den_nz]All goals completed! 🐙
  qsmul := _
  nnqsmul := _

declaration uses 'sorry'example : (3//4) / (5//6) = 9 // 10 := by⊢ 3 // 4 / 5 // 6 = 9 // 10 sorryAll goals completed! 🐙

def declaration uses 'sorry'declaration uses 'sorry'Rat.coe_int_hom : ℤ →+* Rat where
  toFun n := (n:Rat)
  map_zero' := rfl
  map_one' := rfl
  map_add' := by⊢ ∀ (x y : ℤ), ↑(x + y) = ↑x + ↑y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : ℤ), ↑(x * y) = ↑x * ↑y sorryAll goals completed! 🐙

Definition 4.2.6 (positivity)

def Rat.isPos (q:Rat) : Prop := ∃ a b:ℤ, a > 0 ∧ b > 0 ∧ q = a/b

Definition 4.2.6 (negativity)

def Rat.isNeg (q:Rat) : Prop := ∃ r:Rat, r.isPos ∧ q = -r

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem declaration uses 'sorry'Rat.trichotomous (x:Rat) : x = 0 ∨ x.isPos ∨ x.isNeg := byx:Rat⊢ x = 0 ∨ x.isPos ∨ x.isNeg sorryAll goals completed! 🐙

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem declaration uses 'sorry'Rat.not_zero_and_pos (x:Rat) : ¬(x = 0 ∧ x.isPos) := byx:Rat⊢ ¬(x = 0 ∧ x.isPos) sorryAll goals completed! 🐙

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem declaration uses 'sorry'Rat.not_zero_and_neg (x:Rat) : ¬(x = 0 ∧ x.isNeg) := byx:Rat⊢ ¬(x = 0 ∧ x.isNeg) sorryAll goals completed! 🐙

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem declaration uses 'sorry'Rat.not_pos_and_neg (x:Rat) : ¬(x.isPos ∧ x.isNeg) := byx:Rat⊢ ¬(x.isPos ∧ x.isNeg) sorryAll goals completed! 🐙

Definition 4.2.8 (Ordering of the rationals)

instance Rat.instLT : LT Rat where
  lt x y := (x-y).isNeg

Definition 4.2.8 (Ordering of the rationals)

instance Rat.instLE : LE Rat where
  le x y := (x < y) ∨ (x = y)

theorem Rat.lt_iff (x y:Rat) : x < y ↔ (x-y).isNeg := byx:Raty:Rat⊢ x < y ↔ (x - y).isNeg rflAll goals completed! 🐙

theorem Rat.le_iff (x y:Rat) : x ≤ y ↔ (x < y) ∨ (x = y) := byx:Raty:Rat⊢ x ≤ y ↔ x < y ∨ x = y rflAll goals completed! 🐙

theorem declaration uses 'sorry'Rat.gt_iff (x y:Rat) : x > y ↔ (x-y).isPos := byx:Raty:Rat⊢ x > y ↔ (x - y).isPos sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Rat.ge_iff (x y:Rat) : x ≥ y ↔ (x > y) ∨ (x = y) := byx:Raty:Rat⊢ x ≥ y ↔ x > y ∨ x = y sorryAll goals completed! 🐙

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.trichotomous' (x y:Rat) : x > y ∨ x < y ∨ x = y := byx:Raty:Rat⊢ x > y ∨ x < y ∨ x = y sorryAll goals completed! 🐙

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.not_gt_and_lt (x y:Rat) : ¬ (x > y ∧ x < y):= byx:Raty:Rat⊢ ¬(x > y ∧ x < y) sorryAll goals completed! 🐙

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.not_gt_and_eq (x y:Rat) : ¬ (x > y ∧ x = y):= byx:Raty:Rat⊢ ¬(x > y ∧ x = y) sorryAll goals completed! 🐙

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.not_lt_and_eq (x y:Rat) : ¬ (x < y ∧ x = y):= byx:Raty:Rat⊢ ¬(x < y ∧ x = y) sorryAll goals completed! 🐙

Proposition 4.2.9(b) (order is anti-symmetric) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.antisymm (x y:Rat) : x < y ↔ y > x := byx:Raty:Rat⊢ x < y ↔ y > x sorryAll goals completed! 🐙

Proposition 4.2.9(c) (order is transitive) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.lt_trans {x y z:Rat} (hxy: x < y) (hyz: y < z) : x < z := byx:Raty:Ratz:Rathxy:x < yhyz:y < z⊢ x < z sorryAll goals completed! 🐙

Proposition 4.2.9(d) (addition preserves order) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.add_lt_add_right {x y:Rat} (z:Rat) (hxy: x < y) : x + z < y + z := byx:Raty:Ratz:Rathxy:x < y⊢ x + z < y + z sorryAll goals completed! 🐙

Proposition 4.2.9(e) (positive multiplication preserves order) / Exercise 4.2.5

theorem declaration uses 'sorry'Rat.mul_lt_mul_right {x y z:Rat} (hxy: x < y) (hz: z.isPos) : x * z < y * z := byx:Raty:Ratz:Rathxy:x < yhz:z.isPos⊢ x * z < y * z sorryAll goals completed! 🐙

(Not from textbook) Establish the decidability of this order.

instance declaration uses 'sorry'declaration uses 'sorry'Rat.decidableRel : DecidableRel (·≤ ·: Rat → Rat → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
  intro n mn:Ratm:Rat⊢ Decidable ((fun x1 x2 => x1 ≤ x2) n m)
  have : ∀ (n:PreRat) (m: PreRat),
      Decidable (Quotient.mk PreRat.instSetoid n ≤ Quotient.mk PreRat.instSetoid m) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
    intro ⟨ a,b,hb ⟩ ⟨ c,d,hd ⟩n:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
    -- at this point, the goal is morally `Decidable(a//b ≤ c//d)`, but there are technical
    -- issues due to the junk value of formal division when the denominator vanishes.
    -- It may be more convenient to avoid formal division and work directly with `Quotient.mk`.
    cases (0:ℤ).decLe (b*d) with
      | isTrue hbd =>isTruen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
        cases (a * d).decLe (b * c) with
          | isTrue h =>isTrue.isTruen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:a * d ≤ b * c⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isTrueisTrue.isTrue.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:a * d ≤ b * c⊢ ⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
          | isFalse h =>isTrue.isFalsen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:¬a * d ≤ b * c⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isFalseisTrue.isFalse.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:¬a * d ≤ b * c⊢ ¬⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
      | isFalse hbd =>isFalsen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
        cases (b * c).decLe (a * d) with
          | isTrue h =>isFalse.isTruen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:b * c ≤ a * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isTrueisFalse.isTrue.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:b * c ≤ a * d⊢ ⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
          | isFalse h =>isFalse.isFalsen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:¬b * c ≤ a * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isFalseisFalse.isFalse.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:¬b * c ≤ a * d⊢ ¬⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
  exact Quotient.recOnSubsingleton₂ n m thisAll goals completed! 🐙

(Not from textbook) Rat has the structure of a linear ordering.

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.instLinearOrder : LinearOrder Rat where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_ge := sorry
  le_antisymm := sorry
  le_total := sorry
  toDecidableLE := decidableRel

(Not from textbook) Rat has the structure of a strict ordered ring.

instance declaration uses 'sorry'Rat.instIsStrictOrderedRing : IsStrictOrderedRing Rat where
  add_le_add_left := by⊢ ∀ (a b : Rat), a ≤ b → ∀ (c : Rat), c + a ≤ c + b sorryAll goals completed! 🐙
  add_le_add_right := by⊢ ∀ (a b : Rat), a ≤ b → ∀ (c : Rat), a + c ≤ b + c sorryAll goals completed! 🐙
  mul_lt_mul_of_pos_left := by⊢ ∀ (a b c : Rat), a < b → 0 < c → c * a < c * b sorryAll goals completed! 🐙
  mul_lt_mul_of_pos_right := by⊢ ∀ (a b c : Rat), a < b → 0 < c → a * c < b * c sorryAll goals completed! 🐙
  le_of_add_le_add_left := by⊢ ∀ (a b c : Rat), a + b ≤ a + c → b ≤ c sorryAll goals completed! 🐙
  zero_le_one := by⊢ 0 ≤ 1 sorryAll goals completed! 🐙

Exercise 4.2.6

theorem declaration uses 'sorry'Rat.mul_lt_mul_right_of_neg (x y z:Rat) (hxy: x < y) (hz: z.isNeg) : x * z > y * z := byx:Raty:Ratz:Rathxy:x < yhz:z.isNeg⊢ x * z > y * z
  sorryAll goals completed! 🐙

Not in textbook: create an equivalence between Rat and ℚ. This requires some familiarity with the API for Mathlib's version of the rationals.

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.equivRat : Rat ≃ ℚ where
  toFun := Quotient.lift (fun ⟨ a, b, h ⟩ ↦ a / b) (by⊢ ∀ (a b : PreRat),
  a ≈ b →
    (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h } => ↑a / ↑b)
        a =
      (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h } => ↑a / ↑b)
        b
    sorryAll goals completed! 🐙)
  invFun := fun n: ℚ ↦ (n:Rat)
  left_inv n := sorry
  right_inv n := sorry

Not in textbook: equivalence preserves order

abbrev declaration uses 'sorry'Rat.equivRat_order : Rat ≃o ℚ where
  toEquiv := equivRat
  map_rel_iff' := by⊢ ∀ {a b : Rat}, equivRat a ≤ equivRat b ↔ a ≤ b sorryAll goals completed! 🐙

Not in textbook: equivalence preserves ring operations

abbrev declaration uses 'sorry'declaration uses 'sorry'Rat.equivRat_ring : Rat ≃+* ℚ where
  toEquiv := equivRat
  map_add' := by⊢ ∀ (x y : Rat), equivRat.toFun (x + y) = equivRat.toFun x + equivRat.toFun y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : Rat), equivRat.toFun (x * y) = equivRat.toFun x * equivRat.toFun y sorryAll goals completed! 🐙

(Not from textbook) The textbook rationals are isomorphic (as a field) to the Mathlib rationals.

def Rat.equivRat_ring_symm : ℚ ≃+* Rat := Rat.equivRat_ring.symm

end Section_4_2