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