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.Int, as formal differences a // b of integers a b:ℤ, up to equivalence. (This is a quotient of a scaffolding type Section_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 _root_.Rat (or ℚ), which we will use going forward.

namespace Section_4_2structure 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 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! 🐙

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 [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! 🐙 )

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_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! 🐙

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_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! 🐙

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:ℤ) (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 // 1instance Rat.instNatCast : NatCast Rat where natCast n := (n:ℤ) // 1instance Rat.instOfNat : OfNat Rat n where ofNat := (n:ℤ) // 1theorem 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! 🐙

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: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! 🐙)

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'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.dentheorem 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 wheretheorem 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 := 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! 🐙

(Not from textbook) 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! 🐙

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 z:Rat) : x > y ∨ x < y ∨ x = y := byx:Raty:Ratz: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).isPos := byx:Raty:Rat⊢ x < y ↔ (y - x).isPos 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) The order is decidable. This exercise is only recommended for Lean experts. Alternatively, one can establish this fact in classical logic via classical; exact Classical.decRel _

instance declaration uses 'sorry'Rat.decidableRel : DecidableRel (· ≤ · : Rat → Rat → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2 sorryAll 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_le := 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'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