internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.ge_sgn
Proof 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✝ : sgn (p - q) ≄ -1
⊢ sgn (q - p) ≄ 1
Tactic:
intro (_ : sgn (q - p) ≃ 1)
Proof 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✝¹ : sgn (p - q) ≄ -1
x✝ : sgn (q - p) ≃ 1
⊢ False
Theorem: Lean4Axiomatic.Rational.ge_sgn
Proof 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✝¹ : sgn (p - q) ≄ -1
x✝ : sgn (q - p) ≃ 1
⊢ False
Tactic:
have : sgn (p - q) ≃ -1 := calc
  sgn (p - q)    ≃ _ := sgn_subst (eqv_symm neg_sub)
  sgn (-(q - p)) ≃ _ := sgn_compat_neg
  (-sgn (q - p)) ≃ _ := AA.subst₁ ‹sgn (q - p) ≃ 1›
  (-1)           ≃ _ := Rel.refl
Proof 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✝¹ : sgn (p - q) ≄ -1
x✝ : sgn (q - p) ≃ 1
this : sgn (p - q) ≃ -1
⊢ False
Theorem: Lean4Axiomatic.Rational.ge_sgn
Proof 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✝¹ : sgn (p - q) ≄ -1
x✝ : sgn (q - p) ≃ 1
this : sgn (p - q) ≃ -1
⊢ False
Tactic:
exact absurd ‹sgn (p - q) ≃ -1› ‹sgn (p - q) ≄ -1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
⊢ p ≥ 0 ↔ sgn p ≄ -1
Tactic:
apply Iff.intro
Proof 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 : ℚ
⊢ p ≥ 0 → sgn p ≄ -1

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 : ℚ
⊢ sgn p ≄ -1 → p ≥ 0
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
⊢ p ≥ 0 → sgn p ≄ -1
Tactic:
case mp =>
  intro (_ : p ≥ 0)
  show sgn p ≄ -1
  have : sgn (p - 0) ≄ -1 := ge_sgn.mp ‹p ≥ 0›
  have : sgn (p - 0) ≃ sgn p := sgn_subst sub_zero
  have : sgn p ≄ -1 := AA.neqv_substL this ‹sgn (p - 0) ≄ -1›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
⊢ sgn p ≄ -1 → p ≥ 0
Tactic:
case mpr =>
  intro (_ : sgn p ≄ -1)
  show p ≥ 0
  have : sgn p ≃ sgn (p - 0) := sgn_subst (eqv_symm sub_zero)
  have : sgn (p - 0) ≄ -1 := AA.neqv_substL this ‹sgn p ≄ -1›
  have : p ≥ 0 := ge_sgn.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
⊢ p ≥ 0 → sgn p ≄ -1
Tactic:
intro (_ : p ≥ 0)
Proof 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 : ℚ
x✝ : p ≥ 0
⊢ sgn p ≄ -1
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : p ≥ 0
⊢ sgn p ≄ -1
Tactic:
have : sgn (p - 0) ≄ -1 := ge_sgn.mp ‹p ≥ 0›
Proof 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 : ℚ
x✝ : p ≥ 0
this : sgn (p - 0) ≄ -1
⊢ sgn p ≄ -1
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : p ≥ 0
this : sgn (p - 0) ≄ -1
⊢ sgn p ≄ -1
Tactic:
have : sgn (p - 0) ≃ sgn p := sgn_subst sub_zero
Proof 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 : ℚ
x✝ : p ≥ 0
this✝ : sgn (p - 0) ≄ -1
this : sgn (p - 0) ≃ sgn p
⊢ sgn p ≄ -1
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : p ≥ 0
this✝ : sgn (p - 0) ≄ -1
this : sgn (p - 0) ≃ sgn p
⊢ sgn p ≄ -1
Tactic:
have : sgn p ≄ -1 := AA.neqv_substL this ‹sgn (p - 0) ≄ -1›
Proof 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 : ℚ
x✝ : p ≥ 0
this✝¹ : sgn (p - 0) ≄ -1
this✝ : sgn (p - 0) ≃ sgn p
this : sgn p ≄ -1
⊢ sgn p ≄ -1
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : p ≥ 0
this✝¹ : sgn (p - 0) ≄ -1
this✝ : sgn (p - 0) ≃ sgn p
this : sgn p ≄ -1
⊢ sgn p ≄ -1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
⊢ sgn p ≄ -1 → p ≥ 0
Tactic:
intro (_ : sgn p ≄ -1)
Proof 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 : ℚ
x✝ : sgn p ≄ -1
⊢ p ≥ 0
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : sgn p ≄ -1
⊢ p ≥ 0
Tactic:
have : sgn p ≃ sgn (p - 0) := sgn_subst (eqv_symm sub_zero)
Proof 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 : ℚ
x✝ : sgn p ≄ -1
this : sgn p ≃ sgn (p - 0)
⊢ p ≥ 0
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : sgn p ≄ -1
this : sgn p ≃ sgn (p - 0)
⊢ p ≥ 0
Tactic:
have : sgn (p - 0) ≄ -1 := AA.neqv_substL this ‹sgn p ≄ -1›
Proof 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 : ℚ
x✝ : sgn p ≄ -1
this✝ : sgn p ≃ sgn (p - 0)
this : sgn (p - 0) ≄ -1
⊢ p ≥ 0
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : sgn p ≄ -1
this✝ : sgn p ≃ sgn (p - 0)
this : sgn (p - 0) ≄ -1
⊢ p ≥ 0
Tactic:
have : p ≥ 0 := ge_sgn.mpr this
Proof 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 : ℚ
x✝ : sgn p ≄ -1
this✝¹ : sgn p ≃ sgn (p - 0)
this✝ : sgn (p - 0) ≄ -1
this : p ≥ 0
⊢ p ≥ 0
Theorem: Lean4Axiomatic.Rational.ge_zero_sgn
Proof 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 : ℚ
x✝ : sgn p ≄ -1
this✝¹ : sgn p ≃ sgn (p - 0)
this✝ : sgn (p - 0) ≄ -1
this : p ≥ 0
⊢ p ≥ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Rational.order_trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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 ↔ sgn (p - q) ≃ 1
Tactic:
apply Iff.intro
Proof 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 → sgn (p - q) ≃ 1

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 : ℚ
⊢ sgn (p - q) ≃ 1 → ¬p ≤ q
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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 → sgn (p - q) ≃ 1
Tactic:
case mp =>
  intro (_ : ¬(p ≤ q))
  show sgn (p - q) ≃ 1
  have : ¬(sgn (p - q) ≄ 1) := mt le_sgn.mpr ‹¬(p ≤ q)›
  have : sgn (p - q) ≃ 1 := Decidable.of_not_not this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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 : ℚ
⊢ sgn (p - q) ≃ 1 → ¬p ≤ q
Tactic:
case mpr =>
  intro (_ : sgn (p - q) ≃ 1) (_ : p ≤ q)
  show False
  have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
  exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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 → sgn (p - q) ≃ 1
Tactic:
intro (_ : ¬(p ≤ q))
Proof 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
⊢ sgn (p - q) ≃ 1
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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
⊢ sgn (p - q) ≃ 1
Tactic:
have : ¬(sgn (p - q) ≄ 1) := mt le_sgn.mpr ‹¬(p ≤ q)›
Proof 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 : ¬sgn (p - q) ≄ 1
⊢ sgn (p - q) ≃ 1
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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 : ¬sgn (p - q) ≄ 1
⊢ sgn (p - q) ≃ 1
Tactic:
have : sgn (p - q) ≃ 1 := Decidable.of_not_not this
Proof 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✝ : ¬sgn (p - q) ≄ 1
this : sgn (p - q) ≃ 1
⊢ sgn (p - q) ≃ 1
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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✝ : ¬sgn (p - q) ≄ 1
this : sgn (p - q) ≃ 1
⊢ sgn (p - q) ≃ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof 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 : ℚ
⊢ sgn (p - q) ≃ 1 → ¬p ≤ q
Tactic:
intro (_ : sgn (p - q) ≃ 1) (_ : p ≤ q)
Proof 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✝¹ : sgn (p - q) ≃ 1
x✝ : p ≤ q
⊢ False