Theorem: Lean4Axiomatic.Rational.max_le_both (Lean4Axiomatic/Rational/MinMax.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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
⊢ p ≤ r → q ≤ r → Ordered.max p q ≤ r
Tactic:
intro (_ : p ≤ r) (_ : 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
⊢ Ordered.max p q ≤ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
⊢ Ordered.max p q ≤ r
Tactic:
have : max p q ≃ p ∨ max p q ≃ q := max_cases
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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
⊢ Ordered.max p q ≤ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
⊢ Ordered.max p q ≤ r
Tactic:
match this with
| Or.inl (_ : max p q ≃ p) =>
  have : max p q ≤ r := le_substL_eqv (eqv_symm ‹max p q ≃ p›) ‹p ≤ r›
  exact this
| Or.inr (_ : max p q ≃ q) =>
  have : max p q ≤ r := le_substL_eqv (eqv_symm ‹max p q ≃ q›) ‹q ≤ r›
  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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
⊢ Ordered.max p q ≤ r
Tactic:
have : max p q ≤ r := le_substL_eqv (eqv_symm ‹max p q ≃ p›) ‹p ≤ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this : Ordered.max p q ≤ r
⊢ Ordered.max p q ≤ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this : Ordered.max p q ≤ r
⊢ Ordered.max p q ≤ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ q
⊢ Ordered.max p q ≤ r
Tactic:
have : max p q ≤ r := le_substL_eqv (eqv_symm ‹max p q ≃ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ q
this : Ordered.max p q ≤ r
⊢ Ordered.max p q ≤ 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 ℚ
inst✝ : MinMax ℚ
p q r : ℚ
x✝¹ : p ≤ r
x✝ : q ≤ r
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ q
this : Ordered.max p q ≤ r
⊢ Ordered.max p q ≤ r
Tactic:
exact this
State after:
no goals