Аналіз I, Глава 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, unknown identifier 'Section_4_2.Int'Section_4_2.Int, as formal differences 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 differences 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.

namespace Section_4_2

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

Вправа 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

Визначення 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! 🐙

Визначення 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 Quot.ind _ nn:Rat⊢ ∀ (a : PreRat), ∃ a_1 b, b ≠ 0 ∧ Quot.mk (⇑PreRat.instSetoid) a = a_1 // b; intro ⟨ a, b, h ⟩n:Rata:ℤb:ℤh:b ≠ 0⊢ ∃ a_1 b_1, b_1 ≠ 0 ∧ Quot.mk ⇑PreRat.instSetoid { numerator := a, denominator := b, nonzero := h } = a_1 // b_1
  use a, bhn:Rata:ℤb:ℤh:b ≠ 0⊢ b ≠ 0 ∧ Quot.mk ⇑PreRat.instSetoid { numerator := a, denominator := b, nonzero := h } = a // b; refine ⟨ h, ?_ ⟩hn:Rata:ℤb:ℤh:b ≠ 0⊢ Quot.mk ⇑PreRat.instSetoid { numerator := a, denominator := b, nonzero := h } = a // b
  simp [formalDiv, h]hn:Rata:ℤb:ℤh:b ≠ 0⊢ Quot.mk ⇑PreRat.instSetoid { numerator := a, denominator := b, nonzero := h } =
  ⟦{ numerator := a, denominator := b, nonzero := ⋯ }⟧
  rflAll 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! 🐙

Лема 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 [Setoid.r, h1, h2, h1', h2'] at *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! 🐙
  )

Визначення 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_3 }).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_3 }).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_3 }).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_3 }).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_3 }).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_3 }).denominator
  all_goals simp [hb, hd]All goals completed! 🐙

Лема 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! 🐙)

Визначення 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_3 }).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_3 }).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_3 }).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_3 }).denominator
  all_goals simp [hb, hd]All goals completed! 🐙

Лема 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! 🐙)

Визначення 4.2.2 (Negation of rationals)

theorem Rat.neg_eq (a:ℤ) (hb: b ≠ 0) : - (a // b) = (-a) // b := byb:ℤa:ℤhb:b ≠ 0⊢ -a // b = (-a) // b
  convert Quotient.lift_mk _ _ _h.e'_3.h.e'_1.h.e'_3b:ℤa:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_3 }).numeratorh.e'_3.h.e'_2b:ℤa:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_3 }).denominator
  all_goals 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 : OfNat Rat n where
  ofNat := (n:ℤ) // 1

theorem Rat.coe_Int_eq (a:ℤ) : (a:Rat) = a // 1 := bya:ℤ⊢ ↑a = a // 1
  rflAll goals completed! 🐙

theorem Rat.coe_Nat_eq (n:ℕ) : (n:Rat) = n // 1 := byn:ℕ⊢ ↑n = ↑n // 1
  rflAll goals completed! 🐙

theorem Rat.of_Nat_eq (n:ℕ) : (ofNat(n):Rat) = (ofNat(n):Nat) // 1 := byn:ℕ⊢ OfNat.ofNat n = ↑(OfNat.ofNat n) // 1
  rflAll goals completed! 🐙

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

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

lemma Rat.neg_of_int (a:ℤ) : - (a:Rat) = (-a:ℤ) := bya:ℤ⊢ -↑a = ↑(-a)
  rflAll goals completed! 🐙

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:ℤ) (hb: b ≠ 0) : (a // b)⁻¹ = b // a := byb:ℤa:ℤhb:b ≠ 0⊢ (a // b)⁻¹ = b // a
  convert Quotient.lift_mk _ _ _h.e'_3.h.e'_1b:ℤa:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_3 }).denominatorh.e'_3.h.e'_2b:ℤa:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_3 }).numerator
  all_goals simp [hb]All goals completed! 🐙

@[simp]
theorem Rat.inv_zero : (0:Rat)⁻¹ = 0 := by⊢ 0⁻¹ = 0
  rflAll goals completed! 🐙

Твердження 4.2.4 (laws of algebra) / Вправа 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)
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  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:b * d ≠ 0⊢ a // b + c // d + e // f = a // b + (c // d + e // f)
  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:b * d ≠ 0hdf:d * f ≠ 0⊢ a // b + c // d + e // f = a // b + (c // d + e // f)
  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:b * d ≠ 0hdf:d * f ≠ 0hbdf:b * d * f ≠ 0⊢ a // b + c // d + e // f = a // b + (c // d + e // f)

  rw [add_eq _ _ hb hd, add_eq _ _ hbd hf, add_eq _ _ hd hf,
      add_eq _ _ hb hdf, ←mul_assoc b d f, eq _ _ hbdf hbdf]intro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:b * d ≠ 0hdf:d * f ≠ 0hbdf:b * d * f ≠ 0⊢ ((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! 🐙)

Твердження 4.2.4 (laws of algebra) / Вправа 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! 🐙

Твердження 4.2.4 (laws of algebra) / Вправа 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! 🐙

Твердження 4.2.4 (laws of algebra) / Вправа 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'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! 🐙
  natCast_succ := by⊢ ∀ (n : ℕ), ↑(n + 1) = ↑n + 1 sorryAll goals completed! 🐙

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

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:ℚ := ↑a / ↑b⊢ ↑q = a // b
  set num :ℤ := q.numa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.num⊢ ↑q = a // b
  set den :ℤ := (q.den:ℤ)a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.den⊢ ↑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:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0⊢ num // den = a // b
  rw [eq _ _ hden hb]a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0⊢ num * b = a * den
  qifya:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0⊢ ↑num * ↑b = ↑a * ↑den
  have hq : num / den = q := Rat.num_div_den qa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0hq:↑num / ↑den = q⊢ ↑num * ↑b = ↑a * ↑den
  rw [div_eq_div_iff _ _] at hqa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0hq:↑num * ↑b = ↑a * ↑den⊢ ↑num * ↑b = ↑a * ↑dena:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0hq:↑num / ↑den = q⊢ ↑den ≠ 0a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0hq:↑num / ↑den = q⊢ ↑b ≠ 0
  .a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0hq:↑num * ↑b = ↑a * ↑den⊢ ↑num * ↑b = ↑a * ↑den exact hqAll goals completed! 🐙
  .a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑a / ↑bnum:ℤ := q.numden:ℤ := ↑q.denhden:den ≠ 0hq:↑num / ↑den = q⊢ ↑den ≠ 0 simp [hden]All goals completed! 🐙
  simp [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! 🐙

Твердження 4.2.4 (laws of algebra) / Вправа 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 := by⊢ 0⁻¹ = 0 rflAll goals completed! 🐙
  ratCast_def := by⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
    intro qq:ℚ⊢ ↑q = ↑q.num / ↑q.den
    set num := q.numq:ℚnum:ℤ := q.num⊢ ↑q = ↑num / ↑q.den
    set den := q.denq:ℚnum:ℤ := q.numden:ℕ := q.den⊢ ↑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:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ ↑(↑q.num / ↑q.den) = ↑num / ↑den
    convert coe_Rat_eq _ hdenh.e'_3q:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ ↑num / ↑den = q.num // ↑den
    rw [coe_Int_eq, coe_Nat_eq, div_eq, inv_eq, mul_eq, eq]h.e'_3q:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ num * 1 * ↑den = q.num * (1 * ↑den)h.e'_3.hbq:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ 1 * ↑den ≠ 0h.e'_3.hdq:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ 1 ≠ 0h.e'_3.hdq:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ 1 ≠ 0
    .h.e'_3q:ℚnum:ℤ := q.numden:ℕ := q.denhden:↑den ≠ 0⊢ num * 1 * ↑den = q.num * (1 * ↑den) simp [num]All goals completed! 🐙
    all_goals simp [hden, 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' := by⊢ ↑0 = 0 rflAll goals completed! 🐙
  map_one' := by⊢ ↑1 = 1 rflAll goals completed! 🐙
  map_add' := by⊢ ∀ (x y : ℤ), ↑(x + y) = ↑x + ↑y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : ℤ), ↑(x * y) = ↑x * ↑y sorryAll goals completed! 🐙

(Не із книги) The textbook rationals are isomorphic (as a field) to the Mathlib rationals.

def declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.equiv_rat : ℚ ≃+* Rat where
  toFun n := (n:Rat)
  invFun := by⊢ Rat → ℚ sorryAll goals completed! 🐙
  map_add' := by⊢ ∀ (x y : ℚ), ↑(x + y) = ↑x + ↑y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : ℚ), ↑(x * y) = ↑x * ↑y sorryAll goals completed! 🐙
  left_inv := by⊢ Function.LeftInverse sorry fun n => ↑n sorryAll goals completed! 🐙
  right_inv := by⊢ Function.RightInverse sorry fun n => ↑n sorryAll goals completed! 🐙

Визначення 4.2.6 (positivity)

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

Визначення 4.2.6 (negativity)

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

Лема 4.2.7 (trichotomy of rationals) / Вправа 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! 🐙

Лема 4.2.7 (trichotomy of rationals) / Вправа 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! 🐙

Лема 4.2.7 (trichotomy of rationals) / Вправа 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! 🐙

Лема 4.2.7 (trichotomy of rationals) / Вправа 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! 🐙

Визначення 4.2.8 (Ordering of the rationals)

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

Визначення 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! 🐙

Твердження 4.2.9(a) (order trichotomy) / Вправа 4.2.5

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

Твердження 4.2.9(a) (order trichotomy) / Вправа 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! 🐙

Твердження 4.2.9(a) (order trichotomy) / Вправа 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! 🐙

Твердження 4.2.9(a) (order trichotomy) / Вправа 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! 🐙

Твердження 4.2.9(b) (order is anti-symmetric) / Вправа 4.2.5

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

Твердження 4.2.9(c) (order is transitive) / Вправа 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! 🐙

Твердження 4.2.9(d) (addition preserves order) / Вправа 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! 🐙

Твердження 4.2.9(e) (positive multiplication preserves order) / Вправа 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! 🐙

(Не із книги) 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 divisionwhen 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! 🐙

(Не із книги) 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_le := sorry
  le_antisymm := sorry
  le_total := sorry
  toDecidableLE := decidableRel

(Не із книги) 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! 🐙

Вправа 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'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 := sorry
  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! 🐙

end Section_4_2