Theorem: Lean4Axiomatic.Rational.le_trans (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 r : ℚ
⊢ p ≤ q → q ≤ r → p ≤ r
Tactic:
intro (_ : p ≤ q) (_ : q ≤ r)
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

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›
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

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:
have : q < r ∨ q ≃ r := le_cases.mp ‹q ≤ r›
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
⊢ p ≤ r

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
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 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›
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

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)
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

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
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 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›
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

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)
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

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
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 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›
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

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)
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

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
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 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›
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

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)
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

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
State after:
no goals