internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝ : p < q ∨ p ≃ q
this : q < r ∨ q ≃ r
⊢ p ≤ r
Tactic:
match And.intro ‹p < q ∨ p ≃ q› ‹q < r ∨ q ≃ r› with
| (And.intro (Or.inl (_ : p < q)) (Or.inl (_ : q < r))) =>
  have : p < r := lt_trans ‹p < q› ‹q < r›
  have : p ≤ r := le_cases.mpr (Or.inl this)
  exact this
| (And.intro (Or.inl (_ : p < q)) (Or.inr (_ : q ≃ r))) =>
  have : p < r := trans_lt_eqv_lt ‹p < q› ‹q ≃ r›
  have : p ≤ r := le_cases.mpr (Or.inl this)
  exact this
| (And.intro (Or.inr (_ : p ≃ q)) (Or.inl (_ : q < r))) =>
  have : p < r := trans_eqv_lt_lt ‹p ≃ q› ‹q < r›
  have : p ≤ r := le_cases.mpr (Or.inl this)
  exact this
| (And.intro (Or.inr (_ : p ≃ q)) (Or.inr (_ : q ≃ r))) =>
  have : p ≃ r := eqv_trans ‹p ≃ q› ‹q ≃ r›
  have : p ≤ r := le_cases.mpr (Or.inr this)
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝ : p < q ∨ p ≃ q
this : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q < r
⊢ 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
this✝ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q < r
this : p < r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝¹ : p < q ∨ p ≃ q
this✝ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q < r
this : p < r
⊢ p ≤ r
Tactic:
have : p ≤ r := le_cases.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 q r : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q < r
this✝ : p < r
this : p ≤ r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q < r
this✝ : p < r
this : p ≤ r
⊢ p ≤ r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝ : p < q ∨ p ≃ q
this : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q ≃ r
⊢ p ≤ r
Tactic:
have : p < r := trans_lt_eqv_lt ‹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
this✝ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q ≃ r
this : p < r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝¹ : p < q ∨ p ≃ q
this✝ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q ≃ r
this : p < r
⊢ p ≤ r
Tactic:
have : p ≤ r := le_cases.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 q r : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q ≃ r
this✝ : p < r
this : p ≤ r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p < q
h✝ : q ≃ r
this✝ : p < r
this : p ≤ r
⊢ p ≤ r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝ : p < q ∨ p ≃ q
this : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q < r
⊢ p ≤ r
Tactic:
have : p < r := trans_eqv_lt_lt ‹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
this✝ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q < r
this : p < r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝¹ : p < q ∨ p ≃ q
this✝ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q < r
this : p < r
⊢ p ≤ r
Tactic:
have : p ≤ r := le_cases.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 q r : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q < r
this✝ : p < r
this : p ≤ r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q < r
this✝ : p < r
this : p ≤ r
⊢ p ≤ r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝ : p < q ∨ p ≃ q
this : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q ≃ r
⊢ p ≤ r
Tactic:
have : p ≃ r := eqv_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
this✝ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q ≃ r
this : p ≃ r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝¹ : p < q ∨ p ≃ q
this✝ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q ≃ r
this : p ≃ r
⊢ p ≤ r
Tactic:
have : p ≤ r := le_cases.mpr (Or.inr 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 r : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q ≃ r
this✝ : p ≃ r
this : p ≤ r
⊢ p ≤ r
Theorem: Lean4Axiomatic.Rational.le_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✝¹ : p ≤ q
x✝ : q ≤ r
this✝² : p < q ∨ p ≃ q
this✝¹ : q < r ∨ q ≃ r
h✝¹ : p ≃ q
h✝ : q ≃ r
this✝ : p ≃ r
this : p ≤ r
⊢ p ≤ r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_antisymm
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 → q ≤ p → p ≃ q
Tactic:
intro (_ : p ≤ q) (_ : q ≤ 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 : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ p
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
⊢ p ≃ q
Tactic:
have : p < q ∨ p ≃ q := le_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 : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ p
this : p < q ∨ p ≃ q
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
⊢ p ≃ q
Tactic:
match this with
| Or.inl (_ : p < q) =>
  have : q < p ∨ q ≃ p := le_cases.mp ‹q ≤ p›
  match this with
  | Or.inl (_ : q < p) =>
    let Tri := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
    have : Tri := AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
    have : ¬Tri := (order_trichotomy p q).atMostOne
    exact absurd ‹Tri› ‹¬Tri›
  | Or.inr (_ : q ≃ p) =>
    exact eqv_symm ‹q ≃ p›
| Or.inr (_ : p ≃ q) =>
  exact ‹p ≃ q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
h✝ : p < q
⊢ p ≃ q
Tactic:
have : q < p ∨ q ≃ p := le_cases.mp ‹q ≤ 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 : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝ : p < q
this : q < p ∨ q ≃ p
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝ : p < q
this : q < p ∨ q ≃ p
⊢ p ≃ q
Tactic:
match this with
| Or.inl (_ : q < p) =>
  let Tri := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
  have : Tri := AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
  have : ¬Tri := (order_trichotomy p q).atMostOne
  exact absurd ‹Tri› ‹¬Tri›
| Or.inr (_ : q ≃ p) =>
  exact eqv_symm ‹q ≃ p›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q < p
⊢ p ≃ q
Tactic:
let Tri := AA.TwoOfThree (p < q) (p ≃ q) (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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ p ≃ q
Tactic:
have : Tri := AA.TwoOfThree.oneAndThree ‹p < q› ‹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
x✝ : q ≤ p
this✝¹ : p < q ∨ p ≃ q
h✝¹ : p < q
this✝ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this : Tri
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this✝¹ : p < q ∨ p ≃ q
h✝¹ : p < q
this✝ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this : Tri
⊢ p ≃ q
Tactic:
have : ¬Tri := (order_trichotomy p q).atMostOne
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
x✝ : q ≤ p
this✝² : p < q ∨ p ≃ q
h✝¹ : p < q
this✝¹ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this✝ : Tri
this : ¬Tri
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this✝² : p < q ∨ p ≃ q
h✝¹ : p < q
this✝¹ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this✝ : Tri
this : ¬Tri
⊢ p ≃ q
Tactic:
exact absurd ‹Tri› ‹¬Tri›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q ≃ p
⊢ p ≃ q
Tactic:
exact eqv_symm ‹q ≃ p›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_antisymm
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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
h✝ : p ≃ q
⊢ p ≃ q
Tactic:
exact ‹p ≃ q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_lt_le_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 : ℚ
⊢ 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_lt_le_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
⊢ p < r
Tactic:
have : q < r ∨ q ≃ r := le_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_lt_le_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 : q < r ∨ q ≃ r
⊢ p < r
Tactic:
match this with
| Or.inl (_ : q < r) =>
  have : p < r := lt_trans ‹p < q› ‹q < r›
  exact this
| Or.inr (_ : q ≃ r) =>
  have : p < r := lt_substR_eqv ‹q ≃ r› ‹p < q›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_lt_le_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 : q < r ∨ q ≃ r
h✝ : q < r
⊢ 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✝ : q < r ∨ q ≃ r
h✝ : q < r
this : p < r
⊢ p < r
Theorem: Lean4Axiomatic.Rational.trans_lt_le_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✝ : q < r ∨ q ≃ r
h✝ : q < r
this : p < r
⊢ p < r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.trans_lt_le_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 : q < r ∨ q ≃ r
h✝ : q ≃ r
⊢ p < r
Tactic:
have : p < r := lt_substR_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_lt_le_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✝ : q < r ∨ q ≃ r
h✝ : q ≃ r
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 : ℚ
⊢ 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_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
⊢ p < r
Tactic:
have : p < q ∨ p ≃ q := le_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_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
⊢ p < r
Tactic:
match this with
| Or.inl (_ : p < q) =>
  have : p < r := lt_trans ‹p < q› ‹q < r›
  exact this
| Or.inr (_ : p ≃ q) =>
  have : p < r := lt_substL_eqv (eqv_symm ‹p ≃ q›) ‹q < r›
  exact this
Proof state after:
no goals