Theorem: Lean4Axiomatic.Rational.max_le (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 : ℚ
⊢ Ordered.max p q ≃ q ↔ p ≤ q
Tactic:
apply Iff.intro
State after:
case mp
ℕ ℤ ℚ : 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 : ℚ
⊢ Ordered.max p q ≃ q → p ≤ q

case mpr
ℕ ℤ ℚ : 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 : ℚ
⊢ p ≤ q → Ordered.max p q ≃ q

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 : ℚ
⊢ Ordered.max p q ≃ q → p ≤ q
Tactic:
case mp =>
  intro (_ : max p q ≃ q)
  show p ≤ q
  have : p ≤ max p q := max_leL
  have : p ≤ q := le_substR_eqv ‹max p q ≃ q› ‹p ≤ max p q›
  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 : ℚ
⊢ p ≤ q → Ordered.max p q ≃ q
Tactic:
case mpr =>
  intro (_ : p ≤ q)
  show max p q ≃ q
  have : max p q ≃ p ∨ max p q ≃ q := max_cases
  match this with
  | Or.inl (_ : max p q ≃ p) =>
    have : q ≤ max p q := max_leR
    have : q ≤ p := le_substR_eqv ‹max p q ≃ p› ‹q ≤ max p q›
    have : p ≃ q := le_antisymm ‹p ≤ q› ‹q ≤ p›
    have : max p q ≃ q := eqv_trans ‹max p q ≃ p› ‹p ≃ q›
    exact this
  | Or.inr (_ : max p q ≃ q) =>
    have := ‹max p q ≃ q›
    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 : ℚ
⊢ Ordered.max p q ≃ q → p ≤ q
Tactic:
intro (_ : max p q ≃ 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 : ℚ
x✝ : Ordered.max p q ≃ q
⊢ p ≤ q

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 : ℚ
x✝ : Ordered.max p q ≃ q
⊢ p ≤ q
Tactic:
have : p ≤ max p q := max_leL
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 : ℚ
x✝ : Ordered.max p q ≃ q
this : p ≤ Ordered.max p q
⊢ p ≤ q

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 : ℚ
x✝ : Ordered.max p q ≃ q
this : p ≤ Ordered.max p q
⊢ p ≤ q
Tactic:
have : p ≤ q := le_substR_eqv ‹max p q ≃ q› ‹p ≤ max 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 : ℚ
x✝ : Ordered.max p q ≃ q
this✝ : p ≤ Ordered.max p q
this : p ≤ q
⊢ p ≤ q

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 : ℚ
x✝ : Ordered.max p q ≃ q
this✝ : p ≤ Ordered.max p q
this : p ≤ q
⊢ p ≤ q
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 : ℚ
⊢ p ≤ q → Ordered.max p q ≃ q
Tactic:
intro (_ : 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 : ℚ
x✝ : p ≤ q
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
⊢ Ordered.max p q ≃ q
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 : ℚ
x✝ : p ≤ q
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q
Tactic:
match this with
| Or.inl (_ : max p q ≃ p) =>
  have : q ≤ max p q := max_leR
  have : q ≤ p := le_substR_eqv ‹max p q ≃ p› ‹q ≤ max p q›
  have : p ≃ q := le_antisymm ‹p ≤ q› ‹q ≤ p›
  have : max p q ≃ q := eqv_trans ‹max p q ≃ p› ‹p ≃ q›
  exact this
| Or.inr (_ : max p q ≃ q) =>
  have := ‹max p q ≃ q›
  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 : ℚ
x✝ : p ≤ q
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
⊢ Ordered.max p q ≃ q
Tactic:
have : q ≤ max p q := max_leR
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 : ℚ
x✝ : p ≤ q
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this : q ≤ Ordered.max p q
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this : q ≤ Ordered.max p q
⊢ Ordered.max p q ≃ q
Tactic:
have : q ≤ p := le_substR_eqv ‹max p q ≃ p› ‹q ≤ max 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 : ℚ
x✝ : p ≤ q
this✝¹ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this✝ : q ≤ Ordered.max p q
this : q ≤ p
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
this✝¹ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this✝ : q ≤ Ordered.max p q
this : q ≤ p
⊢ Ordered.max p q ≃ q
Tactic:
have : p ≃ q := le_antisymm ‹p ≤ q› ‹q ≤ p›
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 : ℚ
x✝ : p ≤ q
this✝² : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this✝¹ : q ≤ Ordered.max p q
this✝ : q ≤ p
this : p ≃ q
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
this✝² : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this✝¹ : q ≤ Ordered.max p q
this✝ : q ≤ p
this : p ≃ q
⊢ Ordered.max p q ≃ q
Tactic:
have : max p q ≃ q := eqv_trans ‹max p q ≃ p› ‹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 : ℚ
x✝ : p ≤ q
this✝³ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this✝² : q ≤ Ordered.max p q
this✝¹ : q ≤ p
this✝ : p ≃ q
this : Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
this✝³ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ p
this✝² : q ≤ Ordered.max p q
this✝¹ : q ≤ p
this✝ : p ≃ q
this : Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q
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 : ℚ
x✝ : p ≤ q
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ : Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q
Tactic:
have := ‹max p q ≃ 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 : ℚ
x✝ : p ≤ q
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ this : Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q

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 : ℚ
x✝ : p ≤ q
this✝ : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
h✝ this : Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q
Tactic:
exact this
State after:
no goals