internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
this : q ≤ Ordered.max p q
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have : p ≤ max q p := 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
this✝ : q ≤ Ordered.max p q
this : p ≤ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
this✝ : q ≤ Ordered.max p q
this : p ≤ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have : max p q ≃ max q p :=
  opposite_eqv ‹max p q ≃ p› ‹max q p ≃ q› ‹q ≤ max p q› ‹p ≤ max 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
this✝¹ : q ≤ Ordered.max p q
this✝ : p ≤ Ordered.max q p
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
this✝¹ : q ≤ Ordered.max p q
this✝ : p ≤ Ordered.max q p
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have : max p q ≃ max q p := calc
  _ ≃ max p q := eqv_refl
  _ ≃ p       := ‹max p q ≃ p›
  _ ≃ max q p := eqv_symm ‹max q p ≃ 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ p
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ p
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝ : Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
match qp_cases with
| Or.inl (_ : max q p ≃ q) =>
  have : max p q ≃ max q p := calc
    _ ≃ max p q := eqv_refl
    _ ≃ q       := ‹max p q ≃ q›
    _ ≃ max q p := eqv_symm ‹max q p ≃ q›
  exact this
| Or.inr (_ : max q p ≃ p) =>
  have : p ≤ max p q := max_leL
  have : q ≤ max q p := max_leL
  have : max p q ≃ max q p :=
    opposite_eqv ‹max p q ≃ q› ‹max q p ≃ p› ‹p ≤ max p q› ‹q ≤ max q p›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ q
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have : max p q ≃ max q p := calc
  _ ≃ max p q := eqv_refl
  _ ≃ q       := ‹max p q ≃ q›
  _ ≃ max q p := eqv_symm ‹max 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ q
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ q
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
⊢ Ordered.max p q ≃ Ordered.max q p
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
this : p ≤ Ordered.max p q
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
this : p ≤ Ordered.max p q
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have : q ≤ max q p := 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
this✝ : p ≤ Ordered.max p q
this : q ≤ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
this✝ : p ≤ Ordered.max p q
this : q ≤ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have : max p q ≃ max q p :=
  opposite_eqv ‹max p q ≃ q› ‹max q p ≃ p› ‹p ≤ max p q› ‹q ≤ max 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
this✝¹ : p ≤ Ordered.max p q
this✝ : q ≤ Ordered.max q p
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Theorem: Lean4Axiomatic.Rational.max_comm
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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ q
h✝ : Ordered.max q p ≃ p
this✝¹ : p ≤ Ordered.max p q
this✝ : q ≤ Ordered.max q p
this : Ordered.max p q ≃ Ordered.max q p
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_substL
Proof state before:
n₁ n₂ m : Nat
⊢ n₁ ≃ n₂ → compare n₁ m = compare n₂ m
Tactic:
intro (_ : n₁ ≃ n₂)
Proof state after:
n₁ n₂ m : Nat
x✝ : n₁ ≃ n₂
⊢ compare n₁ m = compare n₂ m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_substL
Proof state before:
n₁ n₂ m : Nat
x✝ : n₁ ≃ n₂
⊢ compare n₁ m = compare n₂ m
Tactic:
rw [‹n₁ ≃ n₂›]
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_substR
Proof state before:
n₁ n₂ m : Nat
⊢ n₁ ≃ n₂ → compare m n₁ = compare m n₂
Tactic:
intro (_ : n₁ ≃ n₂)
Proof state after:
n₁ n₂ m : Nat
x✝ : n₁ ≃ n₂
⊢ compare m n₁ = compare m n₂
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_substR
Proof state before:
n₁ n₂ m : Nat
x✝ : n₁ ≃ n₂
⊢ compare m n₁ = compare m n₂
Tactic:
rw [‹n₁ ≃ n₂›]
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m : Nat
⊢ le n n
Tactic:
show ∃ k, n + k ≃ n
Proof state after:
n m : Nat
⊢ ∃ k, n + k ≃ n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m : Nat
⊢ ∃ k, n + k ≃ n
Tactic:
have : n + 0 ≃ n := AA.identR
Proof state after:
n m : Nat
this : n + 0 ≃ n
⊢ ∃ k, n + k ≃ n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m : Nat
this : n + 0 ≃ n
⊢ ∃ k, n + k ≃ n
Tactic:
exact Exists.intro 0 ‹n + 0 ≃ n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
⊢ le n m'.succ
Tactic:
show le n (step m')
Proof state after:
n m m' : Nat
a✝ : n ≤ m'
⊢ le n (step m')
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
⊢ le n (step m')
Tactic:
have : le n m' := impl_le_from_prelude_le ‹n ≤ m'›
Proof state after:
n m m' : Nat
a✝ : n ≤ m'
this : le n m'
⊢ le n (step m')
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
this : le n m'
⊢ le n (step m')
Tactic:
have (Exists.intro k (_ : n + k ≃ m')) := ‹le n m'›
Proof state after:
n m m' : Nat
a✝ : n ≤ m'
this : le n m'
k : Nat
h✝ : n + k ≃ m'
⊢ le n (step m')
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
this : le n m'
k : Nat
h✝ : n + k ≃ m'
⊢ le n (step m')
Tactic:
have : n + step k ≃ step m' := calc
  n + step k   ≃ _ := add_step
  step (n + k) ≃ _ := AA.subst₁ ‹n + k ≃ m'›
  step m'      ≃ _ := Rel.refl
Proof state after:
n m m' : Nat
a✝ : n ≤ m'
this✝ : le n m'
k : Nat
h✝ : n + k ≃ m'
this : n + step k ≃ step m'
⊢ le n (step m')
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
this✝ : le n m'
k : Nat
h✝ : n + k ≃ m'
this : n + step k ≃ step m'
⊢ le n (step m')
Tactic:
have : ∃ k, n + k ≃ step m' := Exists.intro (step k) ‹n + step k ≃ step m'›
Proof state after:
n m m' : Nat
a✝ : n ≤ m'
this✝¹ : le n m'
k : Nat
h✝ : n + k ≃ m'
this✝ : n + step k ≃ step m'
this : ∃ k, n + k ≃ step m'
⊢ le n (step m')
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
this✝¹ : le n m'
k : Nat
h✝ : n + k ≃ m'
this✝ : n + step k ≃ step m'
this : ∃ k, n + k ≃ step m'
⊢ le n (step m')
Tactic:
have : le n (step m') := ‹∃ k, n + k ≃ step m'›
Proof state after:
n m m' : Nat
a✝ : n ≤ m'
this✝² : le n m'
k : Nat
h✝ : n + k ≃ m'
this✝¹ : n + step k ≃ step m'
this✝ : ∃ k, n + k ≃ step m'
this : le n (step m')
⊢ le n (step m')
Theorem: Lean4Axiomatic.Natural.Impl.Nat.impl_le_from_prelude_le
Proof state before:
n m m' : Nat
a✝ : n ≤ m'
this✝² : le n m'
k : Nat
h✝ : n + k ≃ m'
this✝¹ : n + step k ≃ step m'
this✝ : ∃ k, n + k ≃ step m'
this : le n (step m')
⊢ le n (step m')
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n k : Nat
h✝ : n + k ≃ 0
⊢ n ≤ 0
Tactic:
have (And.intro (_ : n ≃ 0) (_ : k ≃ 0)) := zero_sum_split ‹n + k ≃ 0›
Proof state after:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
⊢ n ≤ 0
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
⊢ n ≤ 0
Tactic:
have : n = 0 := ‹n ≃ 0›
Proof state after:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
this : n = 0
⊢ n ≤ 0
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
this : n = 0
⊢ n ≤ 0
Tactic:
match ‹n = 0› with
| rfl => exact Nat.le.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
this : n = 0
⊢ n ≤ n
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' : Nat
h✝ : n + 0 ≃ step m'
⊢ n ≤ m'.succ
Tactic:
show n ≤ step m'
Proof state after:
n m' : Nat
h✝ : n + 0 ≃ step m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' : Nat
h✝ : n + 0 ≃ step m'
⊢ n ≤ step m'
Tactic:
have : n ≃ step m' := Rel.trans (Rel.symm AA.identR) ‹n + 0 ≃ step m'›
Proof state after:
n m' : Nat
h✝ : n + 0 ≃ step m'
this : n ≃ step m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' : Nat
h✝ : n + 0 ≃ step m'
this : n ≃ step m'
⊢ n ≤ step m'
Tactic:
have : n = step m' := ‹n ≃ step m'›
Proof state after:
n m' : Nat
h✝ : n + 0 ≃ step m'
this✝ : n ≃ step m'
this : n = step m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' : Nat
h✝ : n + 0 ≃ step m'
this✝ : n ≃ step m'
this : n = step m'
⊢ n ≤ step m'
Tactic:
match ‹n = step m'› with
| rfl => exact Nat.le.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' : Nat
h✝ : n + 0 ≃ step m'
this✝ : n ≃ step m'
this : n = step m'
⊢ n ≤ n
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ m'.succ
Tactic:
show n ≤ step m'
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ step m'
Tactic:
have : step (n + k') ≃ step m' := calc
  step (n + k') ≃ _ := Rel.symm add_step
  n + step k'   ≃ _ := ‹n + step k' ≃ step m'›
  step m'       ≃ _ := Rel.refl
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this : step (n + k') ≃ step m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this : step (n + k') ≃ step m'
⊢ n ≤ step m'
Tactic:
have : n + k' ≃ m' := AA.inject ‹step (n + k') ≃ step m'›
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝ : step (n + k') ≃ step m'
this : n + k' ≃ m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝ : step (n + k') ≃ step m'
this : n + k' ≃ m'
⊢ n ≤ step m'
Tactic:
have : ∃ k', n + k' ≃ m' := Exists.intro k' ‹n + k' ≃ m'›
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝¹ : step (n + k') ≃ step m'
this✝ : n + k' ≃ m'
this : ∃ k', n + k' ≃ m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝¹ : step (n + k') ≃ step m'
this✝ : n + k' ≃ m'
this : ∃ k', n + k' ≃ m'
⊢ n ≤ step m'
Tactic:
have : le n m' := ‹∃ k', n + k' ≃ m'›
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝² : step (n + k') ≃ step m'
this✝¹ : n + k' ≃ m'
this✝ : ∃ k', n + k' ≃ m'
this : le n m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝² : step (n + k') ≃ step m'
this✝¹ : n + k' ≃ m'
this✝ : ∃ k', n + k' ≃ m'
this : le n m'
⊢ n ≤ step m'
Tactic:
have : n ≤ m' := prelude_le_from_impl_le ‹le n m'›
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝³ : step (n + k') ≃ step m'
this✝² : n + k' ≃ m'
this✝¹ : ∃ k', n + k' ≃ m'
this✝ : le n m'
this : n ≤ m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝³ : step (n + k') ≃ step m'
this✝² : n + k' ≃ m'
this✝¹ : ∃ k', n + k' ≃ m'
this✝ : le n m'
this : n ≤ m'
⊢ n ≤ step m'
Tactic:
have : n ≤ step m' := Nat.le.step ‹n ≤ m'›
Proof state after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝⁴ : step (n + k') ≃ step m'
this✝³ : n + k' ≃ m'
this✝² : ∃ k', n + k' ≃ m'
this✝¹ : le n m'
this✝ : n ≤ m'
this : n ≤ step m'
⊢ n ≤ step m'
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le
Proof state before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝⁴ : step (n + k') ≃ step m'
this✝³ : n + k' ≃ m'
this✝² : ∃ k', n + k' ≃ m'
this✝¹ : le n m'
this✝ : n ≤ m'
this : n ≤ step m'
⊢ n ≤ step m'
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
⊢ n < m ↔ lt n m
Tactic:
apply Iff.intro
Proof state after:
case mp
n m : Nat
⊢ n < m → lt n m

case mpr
n m : Nat
⊢ lt n m → n < m