Theorem: Lean4Axiomatic.Rational.min_max_comm (Lean4Axiomatic/Rational/Metric.lean)

State before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
⊢ Ordered.min p r ≤ q ∧ q ≤ Ordered.max p r → Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p
Tactic:
intro (And.intro (_ : min p r ≤ q) (_ : q ≤ max p r))
State after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
left✝ : Ordered.min p r ≤ q
right✝ : q ≤ Ordered.max p r
⊢ Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p

State before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
left✝ : Ordered.min p r ≤ q
right✝ : q ≤ Ordered.max p r
⊢ Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p
Tactic:
have : min r p ≤ q := le_substL_eqv min_comm ‹min p r ≤ q›
State after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
left✝ : Ordered.min p r ≤ q
right✝ : q ≤ Ordered.max p r
this : Ordered.min r p ≤ q
⊢ Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p

State before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
left✝ : Ordered.min p r ≤ q
right✝ : q ≤ Ordered.max p r
this : Ordered.min r p ≤ q
⊢ Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p
Tactic:
have : q ≤ max r p := le_substR_eqv max_comm ‹q ≤ max p r›
State after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
left✝ : Ordered.min p r ≤ q
right✝ : q ≤ Ordered.max p r
this✝ : Ordered.min r p ≤ q
this : q ≤ Ordered.max r p
⊢ Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p

State before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q r : ℚ
left✝ : Ordered.min p r ≤ q
right✝ : q ≤ Ordered.max p r
this✝ : Ordered.min r p ≤ q
this : q ≤ Ordered.max r p
⊢ Ordered.min r p ≤ q ∧ q ≤ Ordered.max r p
Tactic:
exact And.intro ‹min r p ≤ q› ‹q ≤ max r p›
State after:
no goals