internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝ : Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
match qp_cases with
| Or.inl (_ : min q p ≃ q) =>
  have : min p q ≃ min q p := calc
    _ ≃ min p q := eqv_refl
    _ ≃ q       := ‹min p q ≃ q›
    _ ≃ min q p := eqv_symm ‹min q p ≃ q›
  exact this
| Or.inr (_ : min q p ≃ p) =>
  have : min p q ≤ p := min_leL
  have : min q p ≤ q := min_leL
  have : min p q ≃ min q p :=
    opposite_eqv ‹min p q ≃ q› ‹min q p ≃ p› ‹min p q ≤ p› ‹min q p ≤ q›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≃ min q p := calc
  _ ≃ min p q := eqv_refl
  _ ≃ q       := ‹min p q ≃ q›
  _ ≃ min q p := eqv_symm ‹min 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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
⊢ Ordered.min p q ≃ Ordered.min 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≤ p
⊢ Ordered.min p q ≃ Ordered.min q p
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≤ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min q p ≤ q := 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 : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝ : Ordered.min p q ≤ p
this : Ordered.min q p ≤ q
⊢ Ordered.min p q ≃ Ordered.min q p
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝ : Ordered.min p q ≤ p
this : Ordered.min q p ≤ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≃ min q p :=
  opposite_eqv ‹min p q ≃ q› ‹min q p ≃ p› ‹min p q ≤ p› ‹min 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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝¹ : Ordered.min p q ≤ p
this✝ : Ordered.min q p ≤ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Theorem: Lean4Axiomatic.Rational.min_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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝¹ : Ordered.min p q ≤ p
this✝ : Ordered.min q p ≤ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min 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 : ℚ
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have opposite_eqv
    {r s x y : ℚ} : max r s ≃ x → max s r ≃ y → y ≤ max r s → x ≤ max s r →
    max r s ≃ max s r
    := by
  intro (_ : max r s ≃ x) (_ : max s r ≃ y)
  intro (_ : y ≤ max r s) (_ : x ≤ max s r)
  show max r s ≃ max s r
  have : y ≤ x := le_substR_eqv ‹max r s ≃ x› ‹y ≤ max r s›
  have : x ≤ y := le_substR_eqv ‹max s r ≃ y› ‹x ≤ max s r›
  have : x ≃ y := le_antisymm ‹x ≤ y› ‹y ≤ x›
  have : max r s ≃ max s r := calc
    _ ≃ max r s := eqv_refl
    _ ≃ x       := ‹max r s ≃ x›
    _ ≃ y       := ‹x ≃ y›
    _ ≃ max s r := eqv_symm ‹max s r ≃ y›
  exact this
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
⊢ 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
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have pq_cases : 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 : ℚ
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
⊢ 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
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
have qp_cases : max q p ≃ q ∨ max q p ≃ p := 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 : ℚ
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
⊢ 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
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
match pq_cases with
| Or.inl (_ : max p q ≃ p) =>
  match qp_cases with
  | Or.inl (_ : max q p ≃ q) =>
    have : q ≤ max p q := max_leR
    have : p ≤ max q p := max_leR
    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›
    exact this
  | Or.inr (_ : max q p ≃ p) =>
    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›
    exact this
| Or.inr (_ : max p q ≃ q) =>
  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 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
Tactic:
intro (_ : max r s ≃ x) (_ : max s r ≃ y)
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 s x y : ℚ
x✝¹ : Ordered.max r s ≃ x
x✝ : Ordered.max s r ≃ y
⊢ y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
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 r s x y : ℚ
x✝¹ : Ordered.max r s ≃ x
x✝ : Ordered.max s r ≃ y
⊢ y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
Tactic:
intro (_ : y ≤ max r s) (_ : x ≤ max s 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 s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
⊢ Ordered.max r s ≃ Ordered.max s r
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 r s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
⊢ Ordered.max r s ≃ Ordered.max s r
Tactic:
have : y ≤ x := le_substR_eqv ‹max r s ≃ x› ‹y ≤ max r s›
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 s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this : y ≤ x
⊢ Ordered.max r s ≃ Ordered.max s r
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 r s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this : y ≤ x
⊢ Ordered.max r s ≃ Ordered.max s r
Tactic:
have : x ≤ y := le_substR_eqv ‹max s r ≃ y› ‹x ≤ max s 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 s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this✝ : y ≤ x
this : x ≤ y
⊢ Ordered.max r s ≃ Ordered.max s r
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 r s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this✝ : y ≤ x
this : x ≤ y
⊢ Ordered.max r s ≃ Ordered.max s r
Tactic:
have : x ≃ y := le_antisymm ‹x ≤ y› ‹y ≤ x›
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 s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this✝¹ : y ≤ x
this✝ : x ≤ y
this : x ≃ y
⊢ Ordered.max r s ≃ Ordered.max s r
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 r s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this✝¹ : y ≤ x
this✝ : x ≤ y
this : x ≃ y
⊢ Ordered.max r s ≃ Ordered.max s r
Tactic:
have : max r s ≃ max s r := calc
  _ ≃ max r s := eqv_refl
  _ ≃ x       := ‹max r s ≃ x›
  _ ≃ y       := ‹x ≃ y›
  _ ≃ max s r := eqv_symm ‹max s r ≃ y›
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 s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this✝² : y ≤ x
this✝¹ : x ≤ y
this✝ : x ≃ y
this : Ordered.max r s ≃ Ordered.max s r
⊢ Ordered.max r s ≃ Ordered.max s r
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 r s x y : ℚ
x✝³ : Ordered.max r s ≃ x
x✝² : Ordered.max s r ≃ y
x✝¹ : y ≤ Ordered.max r s
x✝ : x ≤ Ordered.max s r
this✝² : y ≤ x
this✝¹ : x ≤ y
this✝ : x ≃ y
this : Ordered.max r s ≃ Ordered.max s r
⊢ Ordered.max r s ≃ Ordered.max s r
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
⊢ Ordered.max p q ≃ Ordered.max q p
Tactic:
match qp_cases with
| Or.inl (_ : max q p ≃ q) =>
  have : q ≤ max p q := max_leR
  have : p ≤ max q p := max_leR
  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›
  exact this
| Or.inr (_ : max q p ≃ p) =>
  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›
  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 ≃ q
⊢ Ordered.max p q ≃ Ordered.max q p
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 : ℚ
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