Analysis I, Section 4.1

This file is a translation of Section 4.1 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.1" integers, Section_4_1.Int, as formal differences a —— b of natural numbers a b:ℕ, up to equivalence. (This is a quotient of a scaffolding type Section_4_1.PreInt, which consists of formal differences without any equivalence imposed.)
ring operations and order these integers, as well as an embedding of ℕ
Equivalence with the Mathlib integers _root_.Int (or ℤ), which we will use going forward.

namespace Section_4_1

structure PreInt where
  minuend : ℕ
  subtrahend : ℕ

Definition 4.1.1

instance declaration uses 'sorry'PreInt.instSetoid : Setoid PreInt where
  r a b := a.minuend + b.subtrahend = b.minuend + a.subtrahend
  iseqv := {
    refl := by⊢ ∀ (x : PreInt), x.minuend + x.subtrahend = x.minuend + x.subtrahend sorryAll goals completed! 🐙
    symm := by⊢ ∀ {x y : PreInt},
  x.minuend + y.subtrahend = y.minuend + x.subtrahend → y.minuend + x.subtrahend = x.minuend + y.subtrahend sorryAll goals completed! 🐙
    trans := by⊢ ∀ {x y z : PreInt},
  x.minuend + y.subtrahend = y.minuend + x.subtrahend →
    y.minuend + z.subtrahend = z.minuend + y.subtrahend → x.minuend + z.subtrahend = z.minuend + x.subtrahend
      -- This proof is written to follow the structure of the original text.
      intro ⟨ a,b ⟩ ⟨ c,d ⟩ ⟨ e,f ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:{ minuend := a, subtrahend := b }.minuend + { minuend := c, subtrahend := d }.subtrahend =
  { minuend := c, subtrahend := d }.minuend + { minuend := a, subtrahend := b }.subtrahendh2:{ minuend := c, subtrahend := d }.minuend + { minuend := e, subtrahend := f }.subtrahend =
  { minuend := e, subtrahend := f }.minuend + { minuend := c, subtrahend := d }.subtrahend⊢ { minuend := a, subtrahend := b }.minuend + { minuend := e, subtrahend := f }.subtrahend =
  { minuend := e, subtrahend := f }.minuend + { minuend := a, subtrahend := b }.subtrahend
      simp at h1 h2 ⊢a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + d⊢ a + f = e + b
      have h3 := congrArg₂ (· + ·) h1 h2a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:(fun x1 x2 => x1 + x2) (a + d) (c + f) = (fun x1 x2 => x1 + x2) (c + b) (e + d)⊢ a + f = e + b
      simp at h3a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:a + d + (c + f) = c + b + (e + d)⊢ a + f = e + b
      have : (a + f) + (c + d) = (e + b) + (c + d) := calc
        (a + f) + (c + d) = a + d + (c + f) := bya:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:a + d + (c + f) = c + b + (e + d)⊢ a + f + (c + d) = a + d + (c + f) abelAll goals completed! 🐙
        _ = c + b + (e + d) := h3
        _ = (e + b) + (c + d) := bya:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:a + d + (c + f) = c + b + (e + d)⊢ c + b + (e + d) = e + b + (c + d) abelAll goals completed! 🐙
      exact Nat.add_right_cancel thisAll goals completed! 🐙
    }

@[simp]
theorem PreInt.eq (a b c d:ℕ) : (⟨ a,b ⟩: PreInt) ≈ ⟨ c,d ⟩ ↔ a + d = c + b := bya:ℕb:ℕc:ℕd:ℕ⊢ { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b rflAll goals completed! 🐙

abbrev Int := Quotient PreInt.instSetoidabbrev Int.formalDiff (a b:ℕ) : Int := Quotient.mk PreInt.instSetoid ⟨ a,b ⟩infix:100 " —— " => Int.formalDiff

Definition 4.1.1 (Integers)

theorem Int.eq (a b c d:ℕ): a —— b = c —— d ↔ a + d = c + b := bya:ℕb:ℕc:ℕd:ℕ⊢ a —— b = c —— d ↔ a + d = c + b
  constructormpa:ℕb:ℕc:ℕd:ℕ⊢ a —— b = c —— d → a + d = c + bmpra:ℕb:ℕc:ℕd:ℕ⊢ a + d = c + b → a —— b = c —— d
  .mpa:ℕb:ℕc:ℕd:ℕ⊢ a —— b = c —— d → a + d = c + b exact Quotient.exactAll goals completed! 🐙
  intro hmpra:ℕb:ℕc:ℕd:ℕh:a + d = c + b⊢ a —— b = c —— d; exact Quotient.sound hAll goals completed! 🐙

Definition 4.1.1 (Integers)

theorem Int.eq_diff (n:Int) : ∃ a b, n = a —— b := byn:Int⊢ ∃ a b, n = a —— b
  apply Quot.ind _ nn:Int⊢ ∀ (a : PreInt), ∃ a_1 b, Quot.mk (⇑PreInt.instSetoid) a = a_1 —— b; intro ⟨ a, b ⟩n:Inta:ℕb:ℕ⊢ ∃ a_1 b_1, Quot.mk ⇑PreInt.instSetoid { minuend := a, subtrahend := b } = a_1 —— b_1
  use a, bhn:Inta:ℕb:ℕ⊢ Quot.mk ⇑PreInt.instSetoid { minuend := a, subtrahend := b } = a —— b; rflAll goals completed! 🐙

Lemma 4.1.3 (Addition well-defined)

instance Int.instAdd : Add Int where
  add := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a+c) —— (b+d) ) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
          a₂ b₂
    intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    simp [Setoid.r] at *a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + c + (b' + d') = a' + c' + (b + d)
    calc
      _ = (a+b') + (c+d') := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + c + (b' + d') = a + b' + (c + d') abelAll goals completed! 🐙
      _ = (a'+b) + (c'+d) := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + b' + (c + d') = a' + b + (c' + d) rw [h1,h2]All goals completed! 🐙
      _ = _ := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a' + b + (c' + d) = a' + c' + (b + d) abelAll goals completed! 🐙)

Definition 4.1.2 (Definition of addition)

theorem Int.add_eq (a b c d:ℕ) : a —— b + c —— d = (a+c)——(b+d) := Quotient.lift₂_mk _ _ _ _

Lemma 4.1.3 (Multiplication well-defined)

theorem Int.mul_congr_left (a b a' b' c d : ℕ) (h: a —— b = a' —— b') : (a*c+b*d) —— (a*d+b*c) = (a'*c+b'*d) —— (a'*d+b'*c) := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a —— b = a' —— b'⊢ (a * c + b * d) —— (a * d + b * c) = (a' * c + b' * d) —— (a' * d + b' * c)
  simp only [eq] at h ⊢a:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ a * c + b * d + (a' * d + b' * c) = a' * c + b' * d + (a * d + b * c)
  calc
    _ = c*(a+b') + d*(a'+b) := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ a * c + b * d + (a' * d + b' * c) = c * (a + b') + d * (a' + b) ringAll goals completed! 🐙
    _ = c*(a'+b) + d*(a+b') := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ c * (a + b') + d * (a' + b) = c * (a' + b) + d * (a + b') rw [h]All goals completed! 🐙
    _ = _ := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ c * (a' + b) + d * (a + b') = a' * c + b' * d + (a * d + b * c) ringAll goals completed! 🐙

Lemma 4.1.3 (Multiplication well-defined)

theorem Int.mul_congr_right (a b c d c' d' : ℕ) (h: c —— d = c' —— d') : (a*c+b*d) —— (a*d+b*c) = (a*c'+b*d') —— (a*d'+b*c') := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c —— d = c' —— d'⊢ (a * c + b * d) —— (a * d + b * c) = (a * c' + b * d') —— (a * d' + b * c')
  simp only [eq] at h ⊢a:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * c + b * d + (a * d' + b * c') = a * c' + b * d' + (a * d + b * c)
  calc
    _ = a*(c+d') + b*(c'+d) := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * c + b * d + (a * d' + b * c') = a * (c + d') + b * (c' + d) ringAll goals completed! 🐙
    _ = a*(c'+d) + b*(c+d') := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * (c + d') + b * (c' + d) = a * (c' + d) + b * (c + d') rw [h]All goals completed! 🐙
    _ = _ := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * (c' + d) + b * (c + d') = a * c' + b * d' + (a * d + b * c) ringAll goals completed! 🐙

Lemma 4.1.3 (Multiplication well-defined)

theorem Int.mul_congr {a b c d a' b' c' d' : ℕ} (h1: a —— b = a' —— b') (h2: c —— d = c' —— d') :
  (a*c+b*d) —— (a*d+b*c) = (a'*c'+b'*d') —— (a'*d'+b'*c') := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a —— b = a' —— b'h2:c —— d = c' —— d'⊢ (a * c + b * d) —— (a * d + b * c) = (a' * c' + b' * d') —— (a' * d' + b' * c')
  rw [mul_congr_left a b a' b' c d h1, mul_congr_right a' b' c d c' d' h2]All goals completed! 🐙

instance Int.instMul : Mul Int where
  mul := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a * c + b * d) —— (a * d + b * c)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
          a₂ b₂
    intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    simp at h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    convert mul_congr _ _convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' <;>convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' simpaAll goals completed! 🐙
    )

Definition 4.1.2 (Multiplication of integers)

theorem Int.mul_eq (a b c d:ℕ) : a —— b * c —— d = (a*c+b*d) —— (a*d+b*c) := Quotient.lift₂_mk _ _ _ _

instance Int.instOfNat {n:ℕ} : OfNat Int n where
  ofNat := n —— 0

instance Int.instNatCast : NatCast Int where
  natCast n := n —— 0

theorem Int.ofNat_eq (n:ℕ) : ofNat(n) = n —— 0 := rfltheorem Int.natCast_eq (n:ℕ) : (n:Int) = n —— 0 := rfl

@[simp]
theorem Int.natCast_ofNat (n:ℕ) : ((ofNat(n):ℕ): Int) = ofNat(n) := byn:ℕ⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n rflAll goals completed! 🐙

@[simp]
theorem Int.ofNat_inj (n m:ℕ) :
    (ofNat(n) : Int) = (ofNat(m) : Int) ↔ ofNat(n) = ofNat(m) := byn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
      simp only [ofNat_eq, eq, add_zero]n:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m
      rflAll goals completed! 🐙

@[simp]
theorem Int.natCast_inj (n m:ℕ) :
    (n : Int) = (m : Int) ↔ n = m := byn:ℕm:ℕ⊢ ↑n = ↑m ↔ n = m
      simp only [natCast_eq, eq, add_zero]All goals completed! 🐙

example : 3 = 3 —— 0 := by⊢ 3 = 3 —— 0 rflAll goals completed! 🐙

example : 3 = 4 —— 1 := by⊢ 3 = 4 —— 1
  rw [Int.ofNat_eq, Int.eq]All goals completed! 🐙

Definition 4.1.4 (Negation of integers) / Exercise 4.1.2

instance declaration uses 'sorry'Int.instNeg : Neg Int where
  neg := Quotient.lift (fun ⟨ a, b ⟩ ↦ b —— a) (by⊢ ∀ (a b : PreInt),
  a ≈ b →
    (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => b —— a)
        a =
      (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => b —— a)
        b
    sorryAll goals completed! 🐙)

theorem Int.neg_eq (a b:ℕ) : -(a —— b) = b —— a := rflexample : -(3 —— 5) = 5 —— 3 := by⊢ -3 —— 5 = 5 —— 3 rflAll goals completed! 🐙abbrev Int.isPos (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = nabbrev Int.isNeg (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = -n

Lemma 4.1.5 (trichotomy of integers )

theorem Int.trichotomous (x:Int) : x = 0 ∨ x.isPos ∨ x.isNeg := byx:Int⊢ x = 0 ∨ x.isPos ∨ x.isNeg
  -- This proof is slightly modified from that in the original text.
  obtain ⟨ a, b, rfl ⟩ := eq_diff xintro.introa:ℕb:ℕ⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNeg
  have := _root_.trichotomous (r := LT.lt) a bintro.introa:ℕb:ℕthis:a < b ∨ a = b ∨ b < a⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNeg
  rcases this with h_lt | h_eq | h_gtintro.intro.inla:ℕb:ℕh_lt:a < b⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNegintro.intro.inr.inla:ℕb:ℕh_eq:a = b⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNegintro.intro.inr.inra:ℕb:ℕh_gt:b < a⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNeg
  .intro.intro.inla:ℕb:ℕh_lt:a < b⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNeg obtain ⟨ c,rfl ⟩ := Nat.exists_eq_add_of_lt h_ltintro.intro.inl.introa:ℕc:ℕh_lt:a < a + c + 1⊢ a —— (a + c + 1) = 0 ∨ (a —— (a + c + 1)).isPos ∨ (a —— (a + c + 1)).isNeg
    rightintro.intro.inl.intro.ha:ℕc:ℕh_lt:a < a + c + 1⊢ (a —— (a + c + 1)).isPos ∨ (a —— (a + c + 1)).isNeg; rightintro.intro.inl.intro.h.ha:ℕc:ℕh_lt:a < a + c + 1⊢ (a —— (a + c + 1)).isNeg; refine ⟨ c+1, ?_, ?_ ⟩intro.intro.inl.intro.h.h.refine_1a:ℕc:ℕh_lt:a < a + c + 1⊢ c + 1 > 0intro.intro.inl.intro.h.h.refine_2a:ℕc:ℕh_lt:a < a + c + 1⊢ a —— (a + c + 1) = -↑(c + 1)
    .intro.intro.inl.intro.h.h.refine_1a:ℕc:ℕh_lt:a < a + c + 1⊢ c + 1 > 0 linarithAll goals completed! 🐙
    simp_rw [natCast_eq, neg_eq, eq]intro.intro.inl.intro.h.h.refine_2a:ℕc:ℕh_lt:a < a + c + 1⊢ a + (c + 1) = 0 + (a + c + 1)
    abelAll goals completed! 🐙
  .intro.intro.inr.inla:ℕb:ℕh_eq:a = b⊢ a —— b = 0 ∨ (a —— b).isPos ∨ (a —— b).isNeg leftintro.intro.inr.inl.ha:ℕb:ℕh_eq:a = b⊢ a —— b = 0; simp_rw [h_eq, ofNat_eq, eq, add_zero, zero_add]All goals completed! 🐙
  obtain ⟨ c, rfl ⟩ := Nat.exists_eq_add_of_lt h_gtintro.intro.inr.inr.introb:ℕc:ℕh_gt:b < b + c + 1⊢ (b + c + 1) —— b = 0 ∨ ((b + c + 1) —— b).isPos ∨ ((b + c + 1) —— b).isNeg
  rightintro.intro.inr.inr.intro.hb:ℕc:ℕh_gt:b < b + c + 1⊢ ((b + c + 1) —— b).isPos ∨ ((b + c + 1) —— b).isNeg; leftintro.intro.inr.inr.intro.h.hb:ℕc:ℕh_gt:b < b + c + 1⊢ ((b + c + 1) —— b).isPos; refine ⟨ c+1, ?_, ?_ ⟩intro.intro.inr.inr.intro.h.h.refine_1b:ℕc:ℕh_gt:b < b + c + 1⊢ c + 1 > 0intro.intro.inr.inr.intro.h.h.refine_2b:ℕc:ℕh_gt:b < b + c + 1⊢ (b + c + 1) —— b = ↑(c + 1)
  .intro.intro.inr.inr.intro.h.h.refine_1b:ℕc:ℕh_gt:b < b + c + 1⊢ c + 1 > 0 linarithAll goals completed! 🐙
  simp_rw [natCast_eq, eq]intro.intro.inr.inr.intro.h.h.refine_2b:ℕc:ℕh_gt:b < b + c + 1⊢ b + c + 1 + 0 = c + 1 + b
  abelAll goals completed! 🐙

Lemma 4.1.5 (trichotomy of integers)

theorem Int.not_pos_zero (x:Int) : x = 0 ∧ x.isPos → False := byx:Int⊢ x = 0 ∧ x.isPos → False
  rintro ⟨ rfl, ⟨ n, hn, hn' ⟩ ⟩intro.intro.intron:ℕhn:n > 0hn':0 = ↑n⊢ False
  simp [←natCast_ofNat] at hn'intro.intro.intron:ℕhn:n > 0hn':0 = n⊢ False
  linarithAll goals completed! 🐙

Lemma 4.1.5 (trichotomy of integers)

theorem Int.not_neg_zero (x:Int) : x = 0 ∧ x.isNeg → False := byx:Int⊢ x = 0 ∧ x.isNeg → False
  rintro ⟨ rfl, ⟨ n, hn, hn' ⟩ ⟩intro.intro.intron:ℕhn:n > 0hn':0 = -↑n⊢ False
  simp_rw [←natCast_ofNat, natCast_eq, neg_eq, eq] at hn'intro.intro.intron:ℕhn:n > 0hn':0 + n = 0 + 0⊢ False
  linarithAll goals completed! 🐙

Lemma 4.1.5 (trichotomy of integers)

theorem Int.not_pos_neg (x:Int) : x.isPos ∧ x.isNeg → False := byx:Int⊢ x.isPos ∧ x.isNeg → False
  rintro ⟨ ⟨ n, hn, rfl ⟩, ⟨ m, hm, hm' ⟩ ⟩intro.intro.intro.intro.intron:ℕhn:n > 0m:ℕhm:m > 0hm':↑n = -↑m⊢ False
  simp_rw [natCast_eq, neg_eq, eq] at hm'intro.intro.intro.intro.intron:ℕhn:n > 0m:ℕhm:m > 0hm':n + m = 0 + 0⊢ False
  linarithAll goals completed! 🐙

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instAddGroup : AddGroup Int :=
AddGroup.ofLeftAxioms (by⊢ ∀ (a b c : Int), a + b + c = a + (b + c) sorryAll goals completed! 🐙) (by⊢ ∀ (a : Int), 0 + a = a sorryAll goals completed! 🐙) (by⊢ ∀ (a : Int), -a + a = 0 sorryAll goals completed! 🐙)

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

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

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instCommMonoid : CommMonoid Int where
  mul_comm := by⊢ ∀ (a b : Int), a * b = b * a sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Int), a * b * c = a * (b * c)
    -- This proof is written to follow the structure of the original text.
    intro x y zx:Inty:Intz:Int⊢ x * y * z = x * (y * z)
    obtain ⟨ a, b, rfl ⟩ := eq_diff xintro.introy:Intz:Inta:ℕb:ℕ⊢ a —— b * y * z = a —— b * (y * z)
    obtain ⟨ c, d, rfl ⟩ := eq_diff yintro.intro.intro.introz:Inta:ℕb:ℕc:ℕd:ℕ⊢ a —— b * c —— d * z = a —— b * (c —— d * z)
    obtain ⟨ e, f, rfl ⟩ := eq_diff zintro.intro.intro.intro.intro.introa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ a —— b * c —— d * e —— f = a —— b * (c —— d * e —— f)
    simp_rw [mul_eq]intro.intro.intro.intro.intro.introa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ ((a * c + b * d) * e + (a * d + b * c) * f) —— ((a * c + b * d) * f + (a * d + b * c) * e) =
  (a * (c * e + d * f) + b * (c * f + d * e)) —— (a * (c * f + d * e) + b * (c * e + d * f))
    congr 1intro.intro.intro.intro.intro.intro.e_aa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * e + (a * d + b * c) * f = a * (c * e + d * f) + b * (c * f + d * e)intro.intro.intro.intro.intro.intro.e_ba:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * f + (a * d + b * c) * e = a * (c * f + d * e) + b * (c * e + d * f)
    .intro.intro.intro.intro.intro.intro.e_aa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * e + (a * d + b * c) * f = a * (c * e + d * f) + b * (c * f + d * e) ringAll goals completed! 🐙
    ringAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : Int), 1 * a = a sorryAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : Int), a * 1 = a sorryAll goals completed! 🐙

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instCommRing : CommRing Int where
  left_distrib := by⊢ ∀ (a b c : Int), a * (b + c) = a * b + a * c sorryAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : Int), (a + b) * c = a * c + b * c sorryAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : Int), 0 * a = 0 sorryAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : Int), a * 0 = 0 sorryAll goals completed! 🐙

Definition of subtraction

theorem Int.sub_eq (a b:Int) : a - b = a + (-b) := bya:Intb:Int⊢ a - b = a + -b rflAll goals completed! 🐙

theorem declaration uses 'sorry'Int.sub_eq_formal_sub (a b:ℕ) : (a:Int) - (b:Int) = a —— b := bya:ℕb:ℕ⊢ ↑a - ↑b = a —— b sorryAll goals completed! 🐙

Proposition 4.1.8 (No zero divisors) / Exercise 4.1.5

theorem declaration uses 'sorry'Int.mul_eq_zero {a b:Int} (h: a * b = 0) : a = 0 ∨ b = 0 := bya:Intb:Inth:a * b = 0⊢ a = 0 ∨ b = 0 sorryAll goals completed! 🐙

Corollary 4.1.9 (Cancellation law) / Exercise 4.1.6

theorem declaration uses 'sorry'Int.mul_right_cancel₀ (a b c:Int) (h: a*c = b*c) (hc: c ≠ 0) : a = b := bya:Intb:Intc:Inth:a * c = b * chc:c ≠ 0⊢ a = b sorryAll goals completed! 🐙

Definition 4.1.10 (Ordering of the integers)

instance Int.instLE : LE Int where
  le n m := ∃ a:ℕ, m = n + a

Definition 4.1.10 (Ordering of the integers)

instance Int.instLT : LT Int where
  lt n m := (∃ a:ℕ, m = n + a) ∧ n ≠ m

theorem Int.le_iff (n m:Int) : n ≤ m ↔ ∃ a:ℕ, m = n + a := byn:Intm:Int⊢ n ≤ m ↔ ∃ a, m = n + ↑a rflAll goals completed! 🐙

theorem Int.lt_iff (n m:Int): n < m ↔ (∃ a:ℕ, m = n + a) ∧ n ≠ m := byn:Intm:Int⊢ n < m ↔ (∃ a, m = n + ↑a) ∧ n ≠ m rflAll goals completed! 🐙

Lemma 4.1.11(a) (Properties of order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.gt_iff (a b:Int) : a > b ↔ ∃ n:ℕ, n ≠ 0 ∧ a = b + n := bya:Intb:Int⊢ a > b ↔ ∃ n, n ≠ 0 ∧ a = b + ↑n sorryAll goals completed! 🐙

Lemma 4.1.11(b) (Addition preserves order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.add_gt_add_right {a b:Int} (c:Int) (h: a > b) : a+c > b+c := bya:Intb:Intc:Inth:a > b⊢ a + c > b + c sorryAll goals completed! 🐙

Lemma 4.1.11(c) (Positive multiplication preserves order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.mul_lt_mul_of_pos_left {a b c:Int} (hab : a > b) (hc: c > 0) : a*c > b*c := bya:Intb:Intc:Inthab:a > bhc:c > 0⊢ a * c > b * c sorryAll goals completed! 🐙

Lemma 4.1.11(d) (Negation reverses order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.neg_gt_neg {a b:Int} (h: a > b) : -a < -b := bya:Intb:Inth:a > b⊢ -a < -b sorryAll goals completed! 🐙

Lemma 4.1.11(e) (Order is transitive) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.gt_trans {a b c:Int} (hab: a > b) (hbc: b > c) : a > c := bya:Intb:Intc:Inthab:a > bhbc:b > c⊢ a > c sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.trichotomous' (a b c:Int) : a > b ∨ a < b ∨ a = b := bya:Intb:Intc:Int⊢ a > b ∨ a < b ∨ a = b sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.not_gt_and_lt (a b:Int) : ¬ (a > b ∧ a < b):= bya:Intb:Int⊢ ¬(a > b ∧ a < b) sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.not_gt_and_eq (a b:Int) : ¬ (a > b ∧ a = b):= bya:Intb:Int⊢ ¬(a > b ∧ a = b) sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.not_lt_and_eq (a b:Int) : ¬ (a < b ∧ a = b):= bya:Intb:Int⊢ ¬(a < b ∧ a = b) 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'Int.decidableRel : DecidableRel (· ≤ · : Int → Int → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
  sorryAll goals completed! 🐙

(Not from textbook) Int 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'Int.instLinearOrder : LinearOrder Int where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_le := sorry
  le_antisymm := sorry
  le_total := sorry
  toDecidableLE := decidableRel

Exercise 4.1.3

theorem declaration uses 'sorry'Int.neg_one_mul (a:Int) : -1 * a = -a := bya:Int⊢ -1 * a = -a sorryAll goals completed! 🐙

Exercise 4.1.8

theorem declaration uses 'sorry'Int.no_induction : ∃ P: Int → Prop, P 0 ∧ ∀ n, P n → P (n+1) ∧ ¬ ∀ n, P n := by⊢ ∃ P, P 0 ∧ ∀ (n : Int), P n → P (n + 1) ∧ ¬∀ (n : Int), P n sorryAll goals completed! 🐙

Exercise 4.1.9

theorem declaration uses 'sorry'Int.sq_nonneg (n:Int) : n*n ≥ 0 := byn:Int⊢ n * n ≥ 0 sorryAll goals completed! 🐙

Exercise 4.1.9

theorem declaration uses 'sorry'Int.sq_nonneg' (n:Int) : ∃ (m:Nat), n*n = m := byn:Int⊢ ∃ m, n * n = ↑m sorryAll goals completed! 🐙

Not in textbook: create an equivalence between Int and ℤ. This requires some familiarity with the API for Mathlib's version of the integers.

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.equivInt : Int ≃ ℤ where
  toFun := Quotient.lift (fun ⟨ a, b ⟩ ↦ a - b) (by⊢ ∀ (a b : PreInt),
  a ≈ b →
    (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => ↑a - ↑b)
        a =
      (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => ↑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'Int.equivInt_order : Int ≃o ℤ where
  toEquiv := equivInt
  map_rel_iff' := by⊢ ∀ {a b : Int}, equivInt a ≤ equivInt b ↔ a ≤ b sorryAll goals completed! 🐙

Not in textbook: equivalence preserves ring operations

abbrev declaration uses 'sorry'declaration uses 'sorry'Int.equivInt_ring : Int ≃+* ℤ where
  toEquiv := equivInt
  map_add' := by⊢ ∀ (x y : Int), equivInt.toFun (x + y) = equivInt.toFun x + equivInt.toFun y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : Int), equivInt.toFun (x * y) = equivInt.toFun x * equivInt.toFun y sorryAll goals completed! 🐙

end Section_4_1