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