internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.trans_le_lt_lt
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 r : ℚ
x✝¹ : p ≤ q
x✝ : q < r
this : p < q ∨ p ≃ q
h✝ : p < q
⊢ p < r
Tactic:
have : p < r := lt_trans ‹p < q› ‹q < r›
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 r : ℚ
x✝¹ : p ≤ q
x✝ : q < r
this✝ : p < q ∨ p ≃ q
h✝ : p < q
this : p < r
⊢ p < r
Theorem: Lean4Axiomatic.Rational.trans_le_lt_lt
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 r : ℚ
x✝¹ : p ≤ q
x✝ : q < r
this✝ : p < q ∨ p ≃ q
h✝ : p < q
this : p < r
⊢ p < r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_le_lt_lt
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 r : ℚ
x✝¹ : p ≤ q
x✝ : q < r
this : p < q ∨ p ≃ q
h✝ : p ≃ q
⊢ p < r
Tactic:
have : p < r := lt_substL_eqv (eqv_symm ‹p ≃ q›) ‹q < r›
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 r : ℚ
x✝¹ : p ≤ q
x✝ : q < r
this✝ : p < q ∨ p ≃ q
h✝ : p ≃ q
this : p < r
⊢ p < r
Theorem: Lean4Axiomatic.Rational.trans_le_lt_lt
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 r : ℚ
x✝¹ : p ≤ q
x✝ : q < r
this✝ : p < q ∨ p ≃ q
h✝ : p ≃ q
this : p < r
⊢ p < r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.ge_trans
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 r : ℚ
⊢ p ≥ q → q ≥ r → p ≥ r
Tactic:
intro (_ : q ≤ p) (_ : r ≤ 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 r : ℚ
x✝¹ : q ≤ p
x✝ : r ≤ q
⊢ p ≥ r
Theorem: Lean4Axiomatic.Rational.ge_trans
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 r : ℚ
x✝¹ : q ≤ p
x✝ : r ≤ q
⊢ p ≥ r
Tactic:
show r ≤ p
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 r : ℚ
x✝¹ : q ≤ p
x✝ : r ≤ q
⊢ r ≤ p
Theorem: Lean4Axiomatic.Rational.ge_trans
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 r : ℚ
x✝¹ : q ≤ p
x✝ : r ≤ q
⊢ r ≤ p
Tactic:
exact le_trans ‹r ≤ q› ‹q ≤ p›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
⊢ p > q → q ≥ r → p > r
Tactic:
intro (_ : p > q) (_ : q ≥ r)
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
⊢ p > r
Tactic:
have : q > r ∨ q ≃ r := ge_cases.mp ‹q ≥ r›
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this : q > r ∨ q ≃ r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this : q > r ∨ q ≃ r
⊢ p > r
Tactic:
match this with
| Or.inl (_ : q > r) =>
  have : p > r := gt_trans ‹p > q› ‹q > r›
  exact this
| Or.inr (_ : q ≃ r) =>
  have : p > r := lt_substL_eqv ‹q ≃ r› ‹p > q›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this : q > r ∨ q ≃ r
h✝ : q > r
⊢ p > r
Tactic:
have : p > r := gt_trans ‹p > q› ‹q > r›
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this✝ : q > r ∨ q ≃ r
h✝ : q > r
this : p > r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this✝ : q > r ∨ q ≃ r
h✝ : q > r
this : p > r
⊢ p > r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this : q > r ∨ q ≃ r
h✝ : q ≃ r
⊢ p > r
Tactic:
have : p > r := lt_substL_eqv ‹q ≃ r› ‹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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this✝ : q > r ∨ q ≃ r
h✝ : q ≃ r
this : p > r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_gt_ge_gt
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 r : ℚ
x✝¹ : p > q
x✝ : q ≥ r
this✝ : q > r ∨ q ≃ r
h✝ : q ≃ r
this : p > r
⊢ p > r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
⊢ p ≥ q → q > r → p > r
Tactic:
intro (_ : p ≥ q) (_ : q > r)
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
⊢ p > r
Tactic:
have : p > q ∨ p ≃ q := ge_cases.mp ‹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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this : p > q ∨ p ≃ q
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this : p > q ∨ p ≃ q
⊢ p > r
Tactic:
match this with
| Or.inl (_ : p > q) =>
  have : p > r := gt_trans ‹p > q› ‹q > r›
  exact this
| Or.inr (_ : p ≃ q) =>
  have : p > r := lt_substR_eqv (eqv_symm ‹p ≃ q›) ‹q > r›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this : p > q ∨ p ≃ q
h✝ : p > q
⊢ p > r
Tactic:
have : p > r := gt_trans ‹p > q› ‹q > r›
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this✝ : p > q ∨ p ≃ q
h✝ : p > q
this : p > r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this✝ : p > q ∨ p ≃ q
h✝ : p > q
this : p > r
⊢ p > r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this : p > q ∨ p ≃ q
h✝ : p ≃ q
⊢ p > r
Tactic:
have : p > r := lt_substR_eqv (eqv_symm ‹p ≃ q›) ‹q > r›
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this✝ : p > q ∨ p ≃ q
h✝ : p ≃ q
this : p > r
⊢ p > r
Theorem: Lean4Axiomatic.Rational.trans_ge_gt_gt
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 r : ℚ
x✝¹ : p ≥ q
x✝ : q > r
this✝ : p > q ∨ p ≃ q
h✝ : p ≃ q
this : p > r
⊢ p > r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_max
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
Tactic:
have : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1) := sgn_trichotomy p
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 : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ sgn p ≤ 1
Tactic:
match this with
| AA.OneOfThree.first (_ : sgn p ≃ 0) =>
  have : (0 : ℤ) < 1 := Integer.zero_lt_one
  have : (0 : ℤ) ≤ 1 := Integer.le_iff_lt_or_eqv.mpr (Or.inl this)
  have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ 0›) this
  exact this
| AA.OneOfThree.second (_ : sgn p ≃ 1) =>
  have : (1 : ℤ) ≤ 1 := Integer.le_refl
  have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ 1›) this
  exact this
| AA.OneOfThree.third (_ : sgn p ≃ -1) =>
  have : (-1 : ℤ) < 0 := Integer.neg_one_lt_zero
  have : (0 : ℤ) < 1 := Integer.zero_lt_one
  have : (-1 : ℤ) < 1 := Integer.lt_trans ‹(-1 : ℤ) < 0› ‹(0 : ℤ) < 1›
  have : (-1 : ℤ) ≤ 1 := Integer.le_iff_lt_or_eqv.mpr (Or.inl this)
  have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ -1›) this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
⊢ sgn p ≤ 1
Tactic:
have : (0 : ℤ) < 1 := Integer.zero_lt_one
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 : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this : 0 < 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this : 0 < 1
⊢ sgn p ≤ 1
Tactic:
have : (0 : ℤ) ≤ 1 := Integer.le_iff_lt_or_eqv.mpr (Or.inl 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 : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this✝ : 0 < 1
this : 0 ≤ 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this✝ : 0 < 1
this : 0 ≤ 1
⊢ sgn p ≤ 1
Tactic:
have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ 0›) 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 : ℚ
this✝² : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this✝¹ : 0 < 1
this✝ : 0 ≤ 1
this : sgn p ≤ 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝² : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this✝¹ : 0 < 1
this✝ : 0 ≤ 1
this : sgn p ≤ 1
⊢ sgn p ≤ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
⊢ sgn p ≤ 1
Tactic:
have : (1 : ℤ) ≤ 1 := Integer.le_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 : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
this : 1 ≤ 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
this : 1 ≤ 1
⊢ sgn p ≤ 1
Tactic:
have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ 1›) 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 : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
this✝ : 1 ≤ 1
this : sgn p ≤ 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
this✝ : 1 ≤ 1
this : sgn p ≤ 1
⊢ sgn p ≤ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
⊢ sgn p ≤ 1
Tactic:
have : (-1 : ℤ) < 0 := Integer.neg_one_lt_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 : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this : -1 < 0
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this : -1 < 0
⊢ sgn p ≤ 1
Tactic:
have : (0 : ℤ) < 1 := Integer.zero_lt_one
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 : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝ : -1 < 0
this : 0 < 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝ : -1 < 0
this : 0 < 1
⊢ sgn p ≤ 1
Tactic:
have : (-1 : ℤ) < 1 := Integer.lt_trans ‹(-1 : ℤ) < 0› ‹(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 : ℚ
this✝² : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝¹ : -1 < 0
this✝ : 0 < 1
this : -1 < 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝² : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝¹ : -1 < 0
this✝ : 0 < 1
this : -1 < 1
⊢ sgn p ≤ 1
Tactic:
have : (-1 : ℤ) ≤ 1 := Integer.le_iff_lt_or_eqv.mpr (Or.inl 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 : ℚ
this✝³ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝² : -1 < 0
this✝¹ : 0 < 1
this✝ : -1 < 1
this : -1 ≤ 1
⊢ sgn p ≤ 1
Theorem: Lean4Axiomatic.Rational.sgn_max
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 : ℚ
this✝³ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝² : -1 < 0
this✝¹ : 0 < 1
this✝ : -1 < 1
this : -1 ≤ 1
⊢ sgn p ≤ 1
Tactic:
have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ -1›) 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 : ℚ
this✝⁴ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this✝³ : -1 < 0
this✝² : 0 < 1
this✝¹ : -1 < 1
this✝ : -1 ≤ 1
this : sgn p ≤ 1
⊢ sgn p ≤ 1