internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.min_le
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ this : Ordered.min p q ≃ p
⊢ Ordered.min p q ≃ p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ p
Tactic:
have : min p q ≤ p := min_leL
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this : Ordered.min p q ≤ p
⊢ Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this : Ordered.min p q ≤ p
⊢ Ordered.min p q ≃ p
Tactic:
have : q ≤ p := le_substL_eqv ‹min p q ≃ q› ‹min p q ≤ p›
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this✝ : Ordered.min p q ≤ p
this : q ≤ p
⊢ Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this✝ : Ordered.min p q ≤ p
this : q ≤ p
⊢ Ordered.min p q ≃ p
Tactic:
have : q ≃ p := le_antisymm ‹q ≤ p› ‹p ≤ q›
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this✝¹ : Ordered.min p q ≤ p
this✝ : q ≤ p
this : q ≃ p
⊢ Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this✝¹ : Ordered.min p q ≤ p
this✝ : q ≤ p
this : q ≃ p
⊢ Ordered.min p q ≃ p
Tactic:
have : min p q ≃ p := eqv_trans ‹min p q ≃ q› ‹q ≃ p›
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this✝² : Ordered.min p q ≤ p
this✝¹ : q ≤ p
this✝ : q ≃ p
this : Ordered.min p q ≃ p
⊢ Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof 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.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ q
this✝² : Ordered.min p q ≤ p
this✝¹ : q ≤ p
this✝ : q ≃ p
this : Ordered.min p q ≃ p
⊢ Ordered.min p q ≃ p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.max_le
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.min_le_both
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_le_both
Proof 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)
Proof 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