internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.mul_sgn_self_max
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 ℚ
p q : ℚ
x✝ : sgn (p * from_integer (sgn q) - p * from_integer (sgn p)) ≃ 1
this✝⁵ : sgn (sgn q - sgn p) * sgn p ≃ sgn (p * from_integer (sgn q) - p * from_integer (sgn p))
this✝⁴ : sgn (sgn q - sgn p) * sgn p ≃ 1
sqrt1_and_eqv : Integer.Sqrt1 (sgn p) ∧ sgn (sgn q - sgn p) ≃ sgn p
this✝³ : Integer.Sqrt1 (sgn p)
this✝² : sgn (sgn q - sgn p) ≃ sgn p
this✝¹ : sgn p ≃ 1 ∨ sgn p ≃ -1
h✝ : sgn p ≃ -1
this✝ : -1 ≃ sgn p
this : sgn (sgn q - -1) ≃ -1
⊢ False
Tactic:
have : sgn q < -1 := Integer.lt_sgn.mpr 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 ℚ
p q : ℚ
x✝ : sgn (p * from_integer (sgn q) - p * from_integer (sgn p)) ≃ 1
this✝⁶ : sgn (sgn q - sgn p) * sgn p ≃ sgn (p * from_integer (sgn q) - p * from_integer (sgn p))
this✝⁵ : sgn (sgn q - sgn p) * sgn p ≃ 1
sqrt1_and_eqv : Integer.Sqrt1 (sgn p) ∧ sgn (sgn q - sgn p) ≃ sgn p
this✝⁴ : Integer.Sqrt1 (sgn p)
this✝³ : sgn (sgn q - sgn p) ≃ sgn p
this✝² : sgn p ≃ 1 ∨ sgn p ≃ -1
h✝ : sgn p ≃ -1
this✝¹ : -1 ≃ sgn p
this✝ : sgn (sgn q - -1) ≃ -1
this : sgn q < -1
⊢ False
Theorem: Lean4Axiomatic.Rational.mul_sgn_self_max
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 ℚ
p q : ℚ
x✝ : sgn (p * from_integer (sgn q) - p * from_integer (sgn p)) ≃ 1
this✝⁶ : sgn (sgn q - sgn p) * sgn p ≃ sgn (p * from_integer (sgn q) - p * from_integer (sgn p))
this✝⁵ : sgn (sgn q - sgn p) * sgn p ≃ 1
sqrt1_and_eqv : Integer.Sqrt1 (sgn p) ∧ sgn (sgn q - sgn p) ≃ sgn p
this✝⁴ : Integer.Sqrt1 (sgn p)
this✝³ : sgn (sgn q - sgn p) ≃ sgn p
this✝² : sgn p ≃ 1 ∨ sgn p ≃ -1
h✝ : sgn p ≃ -1
this✝¹ : -1 ≃ sgn p
this✝ : sgn (sgn q - -1) ≃ -1
this : sgn q < -1
⊢ False
Tactic:
have : sgn q ≥ -1 := sgn_min
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 ℚ
p q : ℚ
x✝ : sgn (p * from_integer (sgn q) - p * from_integer (sgn p)) ≃ 1
this✝⁷ : sgn (sgn q - sgn p) * sgn p ≃ sgn (p * from_integer (sgn q) - p * from_integer (sgn p))
this✝⁶ : sgn (sgn q - sgn p) * sgn p ≃ 1
sqrt1_and_eqv : Integer.Sqrt1 (sgn p) ∧ sgn (sgn q - sgn p) ≃ sgn p
this✝⁵ : Integer.Sqrt1 (sgn p)
this✝⁴ : sgn (sgn q - sgn p) ≃ sgn p
this✝³ : sgn p ≃ 1 ∨ sgn p ≃ -1
h✝ : sgn p ≃ -1
this✝² : -1 ≃ sgn p
this✝¹ : sgn (sgn q - -1) ≃ -1
this✝ : sgn q < -1
this : sgn q ≥ -1
⊢ False
Theorem: Lean4Axiomatic.Rational.mul_sgn_self_max
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 ℚ
p q : ℚ
x✝ : sgn (p * from_integer (sgn q) - p * from_integer (sgn p)) ≃ 1
this✝⁷ : sgn (sgn q - sgn p) * sgn p ≃ sgn (p * from_integer (sgn q) - p * from_integer (sgn p))
this✝⁶ : sgn (sgn q - sgn p) * sgn p ≃ 1
sqrt1_and_eqv : Integer.Sqrt1 (sgn p) ∧ sgn (sgn q - sgn p) ≃ sgn p
this✝⁵ : Integer.Sqrt1 (sgn p)
this✝⁴ : sgn (sgn q - sgn p) ≃ sgn p
this✝³ : sgn p ≃ 1 ∨ sgn p ≃ -1
h✝ : sgn p ≃ -1
this✝² : -1 ≃ sgn p
this✝¹ : sgn (sgn q - -1) ≃ -1
this✝ : sgn q < -1
this : sgn q ≥ -1
⊢ False
Tactic:
exact Integer.lt_ge_false ‹sgn q < -1› this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_substN_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
⊢ p < q → p / r < q / r
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
⊢ p / r < q / r
Theorem: Lean4Axiomatic.Rational.lt_substN_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
⊢ p / r < q / r
Tactic:
have : sgn (p - q) ≃ -1 := lt_sgn.mp ‹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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this : sgn (p - q) ≃ -1
⊢ p / r < q / r
Theorem: Lean4Axiomatic.Rational.lt_substN_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this : sgn (p - q) ≃ -1
⊢ p / r < q / r
Tactic:
have : sgn (p/r - q/r) ≃ sgn (p - q) := sgn_sub_cancelR_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this✝ : sgn (p - q) ≃ -1
this : sgn (p / r - q / r) ≃ sgn (p - q)
⊢ p / r < q / r
Theorem: Lean4Axiomatic.Rational.lt_substN_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this✝ : sgn (p - q) ≃ -1
this : sgn (p / r - q / r) ≃ sgn (p - q)
⊢ p / r < q / r
Tactic:
have : sgn (p/r - q/r) ≃ -1 :=
  AA.eqv_substL (Rel.symm this) ‹sgn (p - q) ≃ -1›
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this✝¹ : sgn (p - q) ≃ -1
this✝ : sgn (p / r - q / r) ≃ sgn (p - q)
this : sgn (p / r - q / r) ≃ -1
⊢ p / r < q / r
Theorem: Lean4Axiomatic.Rational.lt_substN_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this✝¹ : sgn (p - q) ≃ -1
this✝ : sgn (p / r - q / r) ≃ sgn (p - q)
this : sgn (p / r - q / r) ≃ -1
⊢ p / r < q / r
Tactic:
have : p/r < q/r := lt_sgn.mpr 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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this✝² : sgn (p - q) ≃ -1
this✝¹ : sgn (p / r - q / r) ≃ sgn (p - q)
this✝ : sgn (p / r - q / r) ≃ -1
this : p / r < q / r
⊢ p / r < q / r
Theorem: Lean4Axiomatic.Rational.lt_substN_div_pos
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
x✝ : p < q
this✝² : sgn (p - q) ≃ -1
this✝¹ : sgn (p / r - q / r) ≃ sgn (p - q)
this✝ : sgn (p / r - q / r) ≃ -1
this : p / r < q / r
⊢ p / r < q / r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
⊢ p < q → q / r < p / r
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
⊢ q / r < p / r
Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
⊢ q / r < p / r
Tactic:
have : sgn (p - q) ≃ -1 := lt_sgn.mp ‹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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this : sgn (p - q) ≃ -1
⊢ q / r < p / r
Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this : sgn (p - q) ≃ -1
⊢ q / r < p / r
Tactic:
have : sgn (q/r - p/r) ≃ sgn (p - q) := sgn_sub_cancelR_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝ : sgn (p - q) ≃ -1
this : sgn (q / r - p / r) ≃ sgn (p - q)
⊢ q / r < p / r
Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝ : sgn (p - q) ≃ -1
this : sgn (q / r - p / r) ≃ sgn (p - q)
⊢ q / r < p / r
Tactic:
have : sgn (q/r - p/r) ≃ -1 :=
  AA.eqv_substL (Rel.symm this) ‹sgn (p - q) ≃ -1›
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝¹ : sgn (p - q) ≃ -1
this✝ : sgn (q / r - p / r) ≃ sgn (p - q)
this : sgn (q / r - p / r) ≃ -1
⊢ q / r < p / r
Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝¹ : sgn (p - q) ≃ -1
this✝ : sgn (q / r - p / r) ≃ sgn (p - q)
this : sgn (q / r - p / r) ≃ -1
⊢ q / r < p / r
Tactic:
have : q/r < p/r := lt_sgn.mpr 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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝² : sgn (p - q) ≃ -1
this✝¹ : sgn (q / r - p / r) ≃ sgn (p - q)
this✝ : sgn (q / r - p / r) ≃ -1
this : q / r < p / r
⊢ q / r < p / r
Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg
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 ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝² : sgn (p - q) ≃ -1
this✝¹ : sgn (q / r - p / r) ≃ sgn (p - q)
this✝ : sgn (q / r - p / r) ≃ -1
this : q / r < p / r
⊢ q / r < p / r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.average
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 ℚ
p q : ℚ
⊢ p < q → p < (p + q) / 2 ∧ (p + q) / 2 < 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 ℚ
p q : ℚ
x✝ : p < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Theorem: Lean4Axiomatic.Rational.average
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 ℚ
p q : ℚ
x✝ : p < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
have : p < (p + q)/2 := calc
  _ ≃ p         := eqv_refl
  _ ≃ (2 * p)/2 := eqv_symm mulL_div_same
  _ ≃ (p + p)/2 := div_substL mul_two_add
  _ < (p + q)/2 := lt_substN_div_pos (lt_substR_add ‹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 ℚ
p q : ℚ
x✝ : p < q
this : p < (p + q) / 2
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Theorem: Lean4Axiomatic.Rational.average
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 ℚ
p q : ℚ
x✝ : p < q
this : p < (p + q) / 2
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
have : (p + q)/2 < q := calc
  _ ≃ (p + q)/2 := eqv_refl
  _ < (q + q)/2 := lt_substN_div_pos (lt_substL_add ‹p < q›)
  _ ≃ (2 * q)/2 := div_substL (eqv_symm mul_two_add)
  _ ≃ q         := mulL_div_same
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 ℚ
p q : ℚ
x✝ : p < q
this✝ : p < (p + q) / 2
this : (p + q) / 2 < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Theorem: Lean4Axiomatic.Rational.average
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 ℚ
p q : ℚ
x✝ : p < q
this✝ : p < (p + q) / 2
this : (p + q) / 2 < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
exact And.intro ‹p < (p + q)/2› ‹(p + q)/2 < q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.halve
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 ℚ
p : ℚ
⊢ p > 0 → p > p / 2 ∧ p / 2 > 0
Tactic:
intro (_ : p > 0)
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 ℚ
p : ℚ
x✝ : p > 0
⊢ p > p / 2 ∧ p / 2 > 0
Theorem: Lean4Axiomatic.Rational.halve
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 ℚ
p : ℚ
x✝ : p > 0
⊢ p > p / 2 ∧ p / 2 > 0
Tactic:
have (And.intro (_ : 0 < (0 + p)/2) (_ : (0 + p)/2 < p)) := average ‹0 < 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 ℚ
p : ℚ
x✝ : p > 0
left✝ : 0 < (0 + p) / 2
right✝ : (0 + p) / 2 < p
⊢ p > p / 2 ∧ p / 2 > 0
Theorem: Lean4Axiomatic.Rational.halve
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 ℚ
p : ℚ
x✝ : p > 0
left✝ : 0 < (0 + p) / 2
right✝ : (0 + p) / 2 < p
⊢ p > p / 2 ∧ p / 2 > 0
Tactic:
have : p > p/2 := calc
  _ ≃ p         := eqv_refl
  _ > (0 + p)/2 := ‹(0 + p)/2 < p›
  _ ≃ p/2       := div_substL add_identL
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 ℚ
p : ℚ
x✝ : p > 0
left✝ : 0 < (0 + p) / 2
right✝ : (0 + p) / 2 < p
this : p > p / 2
⊢ p > p / 2 ∧ p / 2 > 0
Theorem: Lean4Axiomatic.Rational.halve
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 ℚ
p : ℚ
x✝ : p > 0
left✝ : 0 < (0 + p) / 2
right✝ : (0 + p) / 2 < p
this : p > p / 2
⊢ p > p / 2 ∧ p / 2 > 0
Tactic:
have : p/2 > 0 := calc
  _ ≃ p/2       := eqv_refl
  _ ≃ (0 + p)/2 := div_substL (eqv_symm add_identL)
  _ > 0         := ‹0 < (0 + p)/2›
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 ℚ
p : ℚ
x✝ : p > 0
left✝ : 0 < (0 + p) / 2
right✝ : (0 + p) / 2 < p
this✝ : p > p / 2
this : p / 2 > 0
⊢ p > p / 2 ∧ p / 2 > 0
Theorem: Lean4Axiomatic.Rational.halve
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 ℚ
p : ℚ
x✝ : p > 0
left✝ : 0 < (0 + p) / 2
right✝ : (0 + p) / 2 < p
this✝ : p > p / 2
this : p / 2 > 0
⊢ p > p / 2 ∧ p / 2 > 0
Tactic:
exact And.intro ‹p > p/2› ‹p/2 > 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_neg_nonneg
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 ℚ
p : ℚ
⊢ p ≥ 0 → -p ≤ p
Tactic:
intro (_ : p ≥ 0)
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 ℚ
p : ℚ
x✝ : p ≥ 0
⊢ -p ≤ p
Theorem: Lean4Axiomatic.Rational.le_neg_nonneg
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 ℚ
p : ℚ
x✝ : p ≥ 0
⊢ -p ≤ p
Tactic:
have : -p ≤ 0 := calc
  _ ≃ -p := eqv_refl
  _ ≤ -0 := le_subst_neg ‹0 ≤ p›
  _ ≃ 0  := neg_preserves_zero.mpr eqv_refl
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 ℚ
p : ℚ
x✝ : p ≥ 0
this : -p ≤ 0
⊢ -p ≤ p
Theorem: Lean4Axiomatic.Rational.le_neg_nonneg
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 ℚ
p : ℚ
x✝ : p ≥ 0
this : -p ≤ 0
⊢ -p ≤ p
Tactic:
have : -p ≤ p := le_trans ‹-p ≤ 0› ‹0 ≤ 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 ℚ
p : ℚ
x✝ : p ≥ 0
this✝ : -p ≤ 0
this : -p ≤ p
⊢ -p ≤ p
Theorem: Lean4Axiomatic.Rational.le_neg_nonneg
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 ℚ
p : ℚ
x✝ : p ≥ 0
this✝ : -p ≤ 0
this : -p ≤ p
⊢ -p ≤ p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_lower
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 ℚ
ε p q : ℚ
⊢ -ε ≤ q - p ↔ 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 ℚ
ε p q : ℚ
⊢ -ε ≤ q - p → 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 ℚ
ε p q : ℚ
⊢ p - ε ≤ q → -ε ≤ q - p
Theorem: Lean4Axiomatic.Rational.le_diff_lower
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 ℚ
ε p q : ℚ
⊢ -ε ≤ q - p → p - ε ≤ q
Tactic:
case mp =>
  intro (_ : -ε ≤ q - p)
  show p - ε ≤ q
  calc
    _ ≃ p - ε          := eqv_refl
    _ ≃ p + (-ε)       := sub_add_neg
    _ ≤ p + (q - p)    := le_substR_add ‹-ε ≤ q - p›
    _ ≃ p + (q + (-p)) := add_substR sub_add_neg
    _ ≃ p + ((-p) + q) := add_substR add_comm
    _ ≃ (p + (-p)) + q := eqv_symm add_assoc
    _ ≃ 0 + q          := add_substL add_inverseR
    _ ≃ q              := add_identL
Proof state after:
no goals