Theorem: Lean4Axiomatic.Integer.order_trichotomy (Lean4Axiomatic/Integer/Order.lean)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ AA.ExactlyOneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have abTri
  : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
  := Signed.trichotomy (a - b)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.ExactlyOneOfThree (a < b) (a ≃ b) (a > b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.ExactlyOneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
apply AA.ExactlyOneOfThree.mk
State after:
case atLeastOne
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)

case atMostOne
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
case atLeastOne =>
  show AA.OneOfThree (a < b) (a ≃ b) (a > b)
  match abTri.atLeastOne with
  | AA.OneOfThree.first (_ : a - b ≃ 0) =>
    have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
    exact AA.OneOfThree.second ‹a ≃ b›
  | AA.OneOfThree.second (_ : Positive (a - b)) =>
    have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
    exact AA.OneOfThree.third ‹a > b›
  | AA.OneOfThree.third (_ : Negative (a - b)) =>
    have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
    exact AA.OneOfThree.first ‹a < b›
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
Tactic:
case atMostOne =>
  intro (_ : AA.TwoOfThree (a < b) (a ≃ b) (a > b))
  show False
  let ab := a - b
  have abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab) :=
    match ‹AA.TwoOfThree (a < b) (a ≃ b) (a > b)› with
    | AA.TwoOfThree.oneAndTwo (_ : a < b) (_ : a ≃ b) =>
      have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
      have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
      AA.TwoOfThree.oneAndThree ‹ab ≃ 0› ‹Negative ab›
    | AA.TwoOfThree.oneAndThree (_ : a < b) (_ : a > b) =>
      have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
      have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
      AA.TwoOfThree.twoAndThree ‹Positive ab› ‹Negative ab›
    | AA.TwoOfThree.twoAndThree (_ : a ≃ b) (_ : a > b) =>
      have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
      have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
      AA.TwoOfThree.oneAndTwo ‹ab ≃ 0› ‹Positive ab›
  have abNotTwo
    : ¬ AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
    := abTri.atMostOne
  exact absurd abTwo abNotTwo
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
match abTri.atLeastOne with
| AA.OneOfThree.first (_ : a - b ≃ 0) =>
  have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
  exact AA.OneOfThree.second ‹a ≃ b›
| AA.OneOfThree.second (_ : Positive (a - b)) =>
  have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
  exact AA.OneOfThree.third ‹a > b›
| AA.OneOfThree.third (_ : Negative (a - b)) =>
  have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
  exact AA.OneOfThree.first ‹a < b›
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
a✝ : a - b ≃ 0
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
a✝ : a - b ≃ 0
this : a ≃ b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
a✝ : a - b ≃ 0
this : a ≃ b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
exact AA.OneOfThree.second ‹a ≃ b›
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
b✝ : Positive (a - b)
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
b✝ : Positive (a - b)
this : a > b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
b✝ : Positive (a - b)
this : a > b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
exact AA.OneOfThree.third ‹a > b›
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
c✝ : Negative (a - b)
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
c✝ : Negative (a - b)
this : a < b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
c✝ : Negative (a - b)
this : a < b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
exact AA.OneOfThree.first ‹a < b›
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
Tactic:
intro (_ : AA.TwoOfThree (a < b) (a ≃ b) (a > b))
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False
Tactic:
let ab := a - b
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
⊢ False

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
⊢ False
Tactic:
have abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab) :=
  match ‹AA.TwoOfThree (a < b) (a ≃ b) (a > b)› with
  | AA.TwoOfThree.oneAndTwo (_ : a < b) (_ : a ≃ b) =>
    have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
    have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
    AA.TwoOfThree.oneAndThree ‹ab ≃ 0› ‹Negative ab›
  | AA.TwoOfThree.oneAndThree (_ : a < b) (_ : a > b) =>
    have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
    have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
    AA.TwoOfThree.twoAndThree ‹Positive ab› ‹Negative ab›
  | AA.TwoOfThree.twoAndThree (_ : a ≃ b) (_ : a > b) =>
    have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
    have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
    AA.TwoOfThree.oneAndTwo ‹ab ≃ 0› ‹Positive ab›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
Tactic:
have abNotTwo
  : ¬ AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
  := abTri.atMostOne
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
abNotTwo : ¬AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
abNotTwo : ¬AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
Tactic:
exact absurd abTwo abNotTwo
State after:
no goals