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

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
let spq := sgn (p - q)
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
have : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1) := sgn_trichotomy (p - q)
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
have : AA.OneOfThree (p ≃ q) (p > q) (p < q) :=
  this.map eqv_sgn.mpr gt_sgn.mpr lt_sgn.mpr
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝ : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : AA.OneOfThree (p ≃ q) (p > q) (p < q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝ : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : AA.OneOfThree (p ≃ q) (p > q) (p < q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
have atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q) := this.rotR
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝ : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝ : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
have : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1) :=
  Integer.signs_distinct
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝¹ : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this✝ : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
this : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝¹ : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this✝ : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
this : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
have : ¬AA.TwoOfThree (p ≃ q) (p > q) (p < q) :=
  mt (AA.TwoOfThree.map eqv_sgn.mp gt_sgn.mp lt_sgn.mp) this
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝² : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this✝¹ : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
this✝ : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : ¬AA.TwoOfThree (p ≃ q) (p > q) (p < q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝² : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this✝¹ : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
this✝ : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : ¬AA.TwoOfThree (p ≃ q) (p > q) (p < q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
have atMostOne : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  mt AA.TwoOfThree.rotL this
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝² : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this✝¹ : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
this✝ : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : ¬AA.TwoOfThree (p ≃ q) (p > q) (p < q)
atMostOne : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
spq : ℤ := sgn (p - q)
this✝² : AA.OneOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this✝¹ : AA.OneOfThree (p ≃ q) (p > q) (p < q)
atLeastOne : AA.OneOfThree (p < q) (p ≃ q) (p > q)
this✝ : ¬AA.TwoOfThree (spq ≃ 0) (spq ≃ 1) (spq ≃ -1)
this : ¬AA.TwoOfThree (p ≃ q) (p > q) (p < q)
atMostOne : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ AA.ExactlyOneOfThree (p < q) (p ≃ q) (p > q)
Tactic:
exact AA.ExactlyOneOfThree.mk atLeastOne atMostOne
State after:
no goals