Theorem: Lean4Axiomatic.Rational.le_cases (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 : ℚ
⊢ p ≤ q ↔ p < q ∨ p ≃ q
Tactic:
apply Iff.intro
State after:
case mp
ℕ ℤ ℚ : 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 : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q

case mpr
ℕ ℤ ℚ : 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 : ℚ
⊢ 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 : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q
Tactic:
case mp =>
  intro (_ : p ≤ q)
  show p < q ∨ p ≃ q
  have : AA.OneOfThree (p < q) (p ≃ q) (p > q) :=
    (order_trichotomy p q).atLeastOne
  match this with
  | AA.OneOfThree.first (_ : p < q) =>
    have : p < q ∨ p ≃ q := Or.inl ‹p < q›
    exact this
  | AA.OneOfThree.second (_ : p ≃ q) =>
    have : p < q ∨ p ≃ q := Or.inr ‹p ≃ q›
    exact this
  | AA.OneOfThree.third (_ : p > q) =>
    have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹p > q›
    have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
    exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
State after:
no goals

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 : ℚ
⊢ p < q ∨ p ≃ q → p ≤ q
Tactic:
case mpr =>
  intro (_ : p < q ∨ p ≃ q)
  show p ≤ q
  have : sgn (p - q) ≄ 1 := by
    intro (_ : sgn (p - q) ≃ 1)
    show False
    have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
    have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      (order_trichotomy p q).atMostOne
    match ‹p < q ∨ p ≃ q› with
    | Or.inl (_ : p < q) =>
      have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
        AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
      exact absurd two not_two
    | Or.inr (_ : p ≃ q) =>
      have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
        AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
      exact absurd two not_two
  have : p ≤ q := le_sgn.mpr this
  exact this
State after:
no goals

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 : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q
Tactic:
intro (_ : 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 : ℚ
x✝ : 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 : ℚ
x✝ : p ≤ q
⊢ p < q ∨ p ≃ q
Tactic:
have : AA.OneOfThree (p < q) (p ≃ q) (p > q) :=
  (order_trichotomy p q).atLeastOne
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 : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (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 : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
⊢ p < q ∨ p ≃ q
Tactic:
match this with
| AA.OneOfThree.first (_ : p < q) =>
  have : p < q ∨ p ≃ q := Or.inl ‹p < q›
  exact this
| AA.OneOfThree.second (_ : p ≃ q) =>
  have : p < q ∨ p ≃ q := Or.inr ‹p ≃ q›
  exact this
| AA.OneOfThree.third (_ : p > q) =>
  have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹p > q›
  have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
  exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
State after:
no goals

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 : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
a✝ : p < q
⊢ p < q ∨ p ≃ q
Tactic:
have : p < q ∨ p ≃ q := Or.inl ‹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 : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
a✝ : p < q
this : p < q ∨ 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 : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
a✝ : p < q
this : p < q ∨ p ≃ q
⊢ p < q ∨ p ≃ q
Tactic:
exact this
State after:
no goals

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 : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
b✝ : p ≃ q
⊢ p < q ∨ p ≃ q
Tactic:
have : p < q ∨ p ≃ q := Or.inr ‹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 : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
b✝ : p ≃ q
this : p < q ∨ 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 : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
b✝ : p ≃ q
this : p < q ∨ p ≃ q
⊢ p < q ∨ p ≃ q
Tactic:
exact this
State after:
no goals

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 : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
⊢ p < q ∨ p ≃ q
Tactic:
have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹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 : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this : sgn (p - q) ≃ 1
⊢ 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 : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this : sgn (p - q) ≃ 1
⊢ p < q ∨ p ≃ q
Tactic:
have : sgn (p - q) ≄ 1 := le_sgn.mp ‹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 : ℚ
x✝ : p ≤ q
this✝¹ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this✝ : sgn (p - q) ≃ 1
this : sgn (p - q) ≄ 1
⊢ 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 : ℚ
x✝ : p ≤ q
this✝¹ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this✝ : sgn (p - q) ≃ 1
this : sgn (p - q) ≄ 1
⊢ p < q ∨ p ≃ q
Tactic:
exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
State after:
no goals

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 : ℚ
⊢ p < q ∨ p ≃ q → p ≤ q
Tactic:
intro (_ : p < q ∨ 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 : ℚ
x✝ : 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 : ℚ
x✝ : p < q ∨ p ≃ q
⊢ p ≤ q
Tactic:
have : sgn (p - q) ≄ 1 := by
  intro (_ : sgn (p - q) ≃ 1)
  show False
  have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
  have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    (order_trichotomy p q).atMostOne
  match ‹p < q ∨ p ≃ q› with
  | Or.inl (_ : p < q) =>
    have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
    exact absurd two not_two
  | Or.inr (_ : p ≃ q) =>
    have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
    exact absurd two not_two
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 : ℚ
x✝ : p < q ∨ p ≃ q
this : sgn (p - q) ≄ 1
⊢ 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 : ℚ
x✝ : p < q ∨ p ≃ q
this : sgn (p - q) ≄ 1
⊢ p ≤ q
Tactic:
have : p ≤ q := le_sgn.mpr 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 : ℚ
x✝ : p < q ∨ p ≃ q
this✝ : sgn (p - q) ≄ 1
this : 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 : ℚ
x✝ : p < q ∨ p ≃ q
this✝ : sgn (p - q) ≄ 1
this : p ≤ q
⊢ p ≤ q
Tactic:
exact this
State after:
no goals

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 : ℚ
x✝ : p < q ∨ p ≃ q
⊢ sgn (p - q) ≄ 1
Tactic:
intro (_ : sgn (p - q) ≃ 1)
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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
⊢ False

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
⊢ False
Tactic:
have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
⊢ False

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
⊢ False
Tactic:
have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  (order_trichotomy p q).atMostOne
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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Tactic:
match ‹p < q ∨ p ≃ q› with
| Or.inl (_ : p < q) =>
  have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
  exact absurd two not_two
| Or.inr (_ : p ≃ q) =>
  have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
  exact absurd two not_two
State after:
no goals

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p < q
⊢ False
Tactic:
have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  AA.TwoOfThree.oneAndThree ‹p < q› ‹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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p < q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p < q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Tactic:
exact absurd two not_two
State after:
no goals

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p ≃ q
⊢ False
Tactic:
have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p ≃ q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False

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 : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p ≃ q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Tactic:
exact absurd two not_two
State after:
no goals