-- The starting properties of the real numbers, rather than a construction -- of them. All results in the article are universally quantified over a -- number system satisfying these properties. No analytic function or -- differentiation rule is part of this interface. class RealNumbers (R : Type) extends Lean.Grind.Field R, LE R, LT R where [linearOrder : Std.IsLinearOrder R] [lawfulLT : Std.LawfulOrderLT R] [orderedArithmetic : Lean.Grind.OrderedRing R] leastUpperBound : ∀ E : R → Prop, (∃ x, E x) → (∃ b, ∀ x, E x → x ≤ b) → ∃ s, (∀ x, E x → x ≤ s) ∧ (∀ b, (∀ x, E x → x ≤ b) → s ≤ b)attribute [instance] RealNumbers.linearOrder RealNumbers.lawfulLT RealNumbers.orderedArithmeticattribute [local instance] Lean.Grind.Semiring.natCast Lean.Grind.Ring.intCastvariable {R : Type} [RealNumbers R]example : (0 : R) < 1 := byR:Typeinst✝:RealNumbers R⊢ 0 < 1 grindAll goals completed! 🐙example (a b c : R) : a*(b+c)=a*b+a*c := byR:Typeinst✝:RealNumbers Ra:Rb:Rc:R⊢ a * (b + c) = a * b + a * c grindAll goals completed! 🐙noncomputable def abs (x : R) : R := @ite _ (0 ≤ x) (Classical.propDecidable _) x (-x)noncomputable def smaller (x y : R) : R := @ite _ (x ≤ y) (Classical.propDecidable _) x ytheorem abs_nonneg (x : R) : 0 ≤ abs x := byR:Typeinst✝:RealNumbers Rx:R⊢ 0 ≤ abs x unfold absR:Typeinst✝:RealNumbers Rx:R⊢ 0 ≤ if 0 ≤ x then x else -x; splitisTrueR:Typeinst✝:RealNumbers Rx:Rh✝:0 ≤ x⊢ 0 ≤ xisFalseR:Typeinst✝:RealNumbers Rx:Rh✝:¬0 ≤ x⊢ 0 ≤ -x <;>isTrueR:Typeinst✝:RealNumbers Rx:Rh✝:0 ≤ x⊢ 0 ≤ xisFalseR:Typeinst✝:RealNumbers Rx:Rh✝:¬0 ≤ x⊢ 0 ≤ -x grindAll goals completed! 🐙theorem abs_zero : abs (0 : R) = 0 := byR:Typeinst✝:RealNumbers R⊢ abs 0 = 0 unfold absR:Typeinst✝:RealNumbers R⊢ (if 0 ≤ 0 then 0 else -0) = 0; grindAll goals completed! 🐙theorem abs_eq_zero (x : R) : abs x = 0 ↔ x = 0 := byR:Typeinst✝:RealNumbers Rx:R⊢ abs x = 0 ↔ x = 0 unfold absR:Typeinst✝:RealNumbers Rx:R⊢ (if 0 ≤ x then x else -x) = 0 ↔ x = 0; splitisTrueR:Typeinst✝:RealNumbers Rx:Rh✝:0 ≤ x⊢ x = 0 ↔ x = 0isFalseR:Typeinst✝:RealNumbers Rx:Rh✝:¬0 ≤ x⊢ -x = 0 ↔ x = 0 <;>isTrueR:Typeinst✝:RealNumbers Rx:Rh✝:0 ≤ x⊢ x = 0 ↔ x = 0isFalseR:Typeinst✝:RealNumbers Rx:Rh✝:¬0 ≤ x⊢ -x = 0 ↔ x = 0 grindAll goals completed! 🐙theorem abs_neg (x : R) : abs (-x) = abs x := byR:Typeinst✝:RealNumbers Rx:R⊢ abs (-x) = abs x unfold absR:Typeinst✝:RealNumbers Rx:R⊢ (if 0 ≤ -x then -x else - -x) = if 0 ≤ x then x else -x; splitisTrueR:Typeinst✝:RealNumbers Rx:Rh✝:0 ≤ -x⊢ -x = if 0 ≤ x then x else -xisFalseR:Typeinst✝:RealNumbers Rx:Rh✝:¬0 ≤ -x⊢ - -x = if 0 ≤ x then x else -x <;>isTrueR:Typeinst✝:RealNumbers Rx:Rh✝:0 ≤ -x⊢ -x = if 0 ≤ x then x else -xisFalseR:Typeinst✝:RealNumbers Rx:Rh✝:¬0 ≤ -x⊢ - -x = if 0 ≤ x then x else -x splitisFalse.isTrueR:Typeinst✝:RealNumbers Rx:Rh✝¹:¬0 ≤ -xh✝:0 ≤ x⊢ - -x = xisFalse.isFalseR:Typeinst✝:RealNumbers Rx:Rh✝¹:¬0 ≤ -xh✝:¬0 ≤ x⊢ - -x = -x <;>isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Rh✝¹:0 ≤ -xh✝:0 ≤ x⊢ -x = xisTrue.isFalseR:Typeinst✝:RealNumbers Rx:Rh✝¹:0 ≤ -xh✝:¬0 ≤ x⊢ -x = -xisFalse.isTrueR:Typeinst✝:RealNumbers Rx:Rh✝¹:¬0 ≤ -xh✝:0 ≤ x⊢ - -x = xisFalse.isFalseR:Typeinst✝:RealNumbers Rx:Rh✝¹:¬0 ≤ -xh✝:¬0 ≤ x⊢ - -x = -x grindAll goals completed! 🐙theorem abs_triangle (x y : R) : abs (x + y) ≤ abs x + abs y := byR:Typeinst✝:RealNumbers Rx:Ry:R⊢ abs (x + y) ≤ abs x + abs y unfold absR:Typeinst✝:RealNumbers Rx:Ry:R⊢ (if 0 ≤ x + y then x + y else -(x + y)) ≤ (if 0 ≤ x then x else -x) + if 0 ≤ y then y else -y; splitisTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝:0 ≤ x + y⊢ x + y ≤ (if 0 ≤ x then x else -x) + if 0 ≤ y then y else -yisFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝:¬0 ≤ x + y⊢ -(x + y) ≤ (if 0 ≤ x then x else -x) + if 0 ≤ y then y else -y <;>isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝:0 ≤ x + y⊢ x + y ≤ (if 0 ≤ x then x else -x) + if 0 ≤ y then y else -yisFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝:¬0 ≤ x + y⊢ -(x + y) ≤ (if 0 ≤ x then x else -x) + if 0 ≤ y then y else -y splitisFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝¹:¬0 ≤ x + yh✝:0 ≤ x⊢ -(x + y) ≤ x + if 0 ≤ y then y else -yisFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝¹:¬0 ≤ x + yh✝:¬0 ≤ x⊢ -(x + y) ≤ -x + if 0 ≤ y then y else -y <;>isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝¹:0 ≤ x + yh✝:0 ≤ x⊢ x + y ≤ x + if 0 ≤ y then y else -yisTrue.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝¹:0 ≤ x + yh✝:¬0 ≤ x⊢ x + y ≤ -x + if 0 ≤ y then y else -yisFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝¹:¬0 ≤ x + yh✝:0 ≤ x⊢ -(x + y) ≤ x + if 0 ≤ y then y else -yisFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝¹:¬0 ≤ x + yh✝:¬0 ≤ x⊢ -(x + y) ≤ -x + if 0 ≤ y then y else -y splitisFalse.isFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:¬0 ≤ x + yh✝¹:¬0 ≤ xh✝:0 ≤ y⊢ -(x + y) ≤ -x + yisFalse.isFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:¬0 ≤ x + yh✝¹:¬0 ≤ xh✝:¬0 ≤ y⊢ -(x + y) ≤ -x + -y <;>isTrue.isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:0 ≤ x + yh✝¹:0 ≤ xh✝:0 ≤ y⊢ x + y ≤ x + yisTrue.isTrue.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:0 ≤ x + yh✝¹:0 ≤ xh✝:¬0 ≤ y⊢ x + y ≤ x + -yisTrue.isFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:0 ≤ x + yh✝¹:¬0 ≤ xh✝:0 ≤ y⊢ x + y ≤ -x + yisTrue.isFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:0 ≤ x + yh✝¹:¬0 ≤ xh✝:¬0 ≤ y⊢ x + y ≤ -x + -yisFalse.isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:¬0 ≤ x + yh✝¹:0 ≤ xh✝:0 ≤ y⊢ -(x + y) ≤ x + yisFalse.isTrue.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:¬0 ≤ x + yh✝¹:0 ≤ xh✝:¬0 ≤ y⊢ -(x + y) ≤ x + -yisFalse.isFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:¬0 ≤ x + yh✝¹:¬0 ≤ xh✝:0 ≤ y⊢ -(x + y) ≤ -x + yisFalse.isFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh✝²:¬0 ≤ x + yh✝¹:¬0 ≤ xh✝:¬0 ≤ y⊢ -(x + y) ≤ -x + -y grindAll goals completed! 🐙theorem abs_mul (x y : R) : abs (x * y) = abs x * abs y := byR:Typeinst✝:RealNumbers Rx:Ry:R⊢ abs (x * y) = abs x * abs y have h₁ := @Lean.Grind.OrderedRing.mul_nonneg R _ _ _ _ _ _ x yR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * y⊢ abs (x * y) = abs x * abs y have h₂ := @Lean.Grind.OrderedRing.mul_nonneg R _ _ _ _ _ _ (-x) yR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * y⊢ abs (x * y) = abs x * abs y have h₃ := @Lean.Grind.OrderedRing.mul_nonneg R _ _ _ _ _ _ x (-y)R:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -y⊢ abs (x * y) = abs x * abs y have h₄ := @Lean.Grind.OrderedRing.mul_nonneg R _ _ _ _ _ _ (-x) (-y)R:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -y⊢ abs (x * y) = abs x * abs y unfold absR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -y⊢ (if 0 ≤ x * y then x * y else -(x * y)) = (if 0 ≤ x then x else -x) * if 0 ≤ y then y else -y; splitisTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝:0 ≤ x * y⊢ x * y = (if 0 ≤ x then x else -x) * if 0 ≤ y then y else -yisFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝:¬0 ≤ x * y⊢ -(x * y) = (if 0 ≤ x then x else -x) * if 0 ≤ y then y else -y <;>isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝:0 ≤ x * y⊢ x * y = (if 0 ≤ x then x else -x) * if 0 ≤ y then y else -yisFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝:¬0 ≤ x * y⊢ -(x * y) = (if 0 ≤ x then x else -x) * if 0 ≤ y then y else -y splitisFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝¹:¬0 ≤ x * yh✝:0 ≤ x⊢ -(x * y) = x * if 0 ≤ y then y else -yisFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝¹:¬0 ≤ x * yh✝:¬0 ≤ x⊢ -(x * y) = -x * if 0 ≤ y then y else -y <;>isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝¹:0 ≤ x * yh✝:0 ≤ x⊢ x * y = x * if 0 ≤ y then y else -yisTrue.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝¹:0 ≤ x * yh✝:¬0 ≤ x⊢ x * y = -x * if 0 ≤ y then y else -yisFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝¹:¬0 ≤ x * yh✝:0 ≤ x⊢ -(x * y) = x * if 0 ≤ y then y else -yisFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝¹:¬0 ≤ x * yh✝:¬0 ≤ x⊢ -(x * y) = -x * if 0 ≤ y then y else -y splitisFalse.isFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:¬0 ≤ x * yh✝¹:¬0 ≤ xh✝:0 ≤ y⊢ -(x * y) = -x * yisFalse.isFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:¬0 ≤ x * yh✝¹:¬0 ≤ xh✝:¬0 ≤ y⊢ -(x * y) = -x * -y <;>isTrue.isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:0 ≤ x * yh✝¹:0 ≤ xh✝:0 ≤ y⊢ x * y = x * yisTrue.isTrue.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:0 ≤ x * yh✝¹:0 ≤ xh✝:¬0 ≤ y⊢ x * y = x * -yisTrue.isFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:0 ≤ x * yh✝¹:¬0 ≤ xh✝:0 ≤ y⊢ x * y = -x * yisTrue.isFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:0 ≤ x * yh✝¹:¬0 ≤ xh✝:¬0 ≤ y⊢ x * y = -x * -yisFalse.isTrue.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:¬0 ≤ x * yh✝¹:0 ≤ xh✝:0 ≤ y⊢ -(x * y) = x * yisFalse.isTrue.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:¬0 ≤ x * yh✝¹:0 ≤ xh✝:¬0 ≤ y⊢ -(x * y) = x * -yisFalse.isFalse.isTrueR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:¬0 ≤ x * yh✝¹:¬0 ≤ xh✝:0 ≤ y⊢ -(x * y) = -x * yisFalse.isFalse.isFalseR:Typeinst✝:RealNumbers Rx:Ry:Rh₁:0 ≤ x → 0 ≤ y → 0 ≤ x * yh₂:0 ≤ -x → 0 ≤ y → 0 ≤ -x * yh₃:0 ≤ x → 0 ≤ -y → 0 ≤ x * -yh₄:0 ≤ -x → 0 ≤ -y → 0 ≤ -x * -yh✝²:¬0 ≤ x * yh✝¹:¬0 ≤ xh✝:¬0 ≤ y⊢ -(x * y) = -x * -y grindAll goals completed! 🐙theorem abs_lt (x ε : R) : abs x < ε ↔ -ε < x ∧ x < ε := byR:Typeinst✝:RealNumbers Rx:Rε:R⊢ abs x < ε ↔ -ε < x ∧ x < ε unfold absR:Typeinst✝:RealNumbers Rx:Rε:R⊢ (if 0 ≤ x then x else -x) < ε ↔ -ε < x ∧ x < ε; splitisTrueR:Typeinst✝:RealNumbers Rx:Rε:Rh✝:0 ≤ x⊢ x < ε ↔ -ε < x ∧ x < εisFalseR:Typeinst✝:RealNumbers Rx:Rε:Rh✝:¬0 ≤ x⊢ -x < ε ↔ -ε < x ∧ x < ε <;>isTrueR:Typeinst✝:RealNumbers Rx:Rε:Rh✝:0 ≤ x⊢ x < ε ↔ -ε < x ∧ x < εisFalseR:Typeinst✝:RealNumbers Rx:Rε:Rh✝:¬0 ≤ x⊢ -x < ε ↔ -ε < x ∧ x < ε grindAll goals completed! 🐙-- Compatibility names keep elementary proof steps readable in the article. theorem mul_nonneg {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a*b := Lean.Grind.OrderedRing.mul_nonneg ha hbtheorem mul_pos {a b : R} (ha : 0<a) (hb : 0<b) : 0<a*b := Lean.Grind.OrderedRing.mul_pos ha hbtheorem le_of_lt {a b : R} (h : a<b) : a≤b := Std.le_of_lt htheorem mul_le_mul_of_nonneg_left {a b c : R} (h : a≤b) (hc : 0≤c) : c*a≤c*b := Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_left h hctheorem mul_le_mul_of_nonneg_right {a b c : R} (h : a≤b) (hc : 0≤c) : a*c≤b*c := Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right h hctheorem mul_lt_mul_of_pos_left {a b c : R} (h : a<b) (hc : 0<c) : c*a<c*b := Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left h hctheorem mul_lt_mul_of_pos_right {a b c : R} (h : a<b) (hc : 0<c) : a*c<b*c := Lean.Grind.OrderedRing.mul_lt_mul_of_pos_right h hctheorem mul_lt_mul_right {a b c : R} (hc : 0<c) : a*c<b*c ↔ a<b := Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_right hctheorem inv_pos {a : R} : 0<a⁻¹ ↔ 0<a := Lean.Grind.Field.IsOrdered.inv_pos_iff theorem div_lt_iff {a b c : R} (hb : 0<b) : a/b<c ↔ a<c*b := byR:Typeinst✝:RealNumbers Ra:Rb:Rc:Rhb:0 < b⊢ a / b < c ↔ a < c * b rw [Lean.Grind.Field.div_eq_mul_invR:Typeinst✝:RealNumbers Ra:Rb:Rc:Rhb:0 < b⊢ a * b⁻¹ < c ↔ a < c * bR:Typeinst✝:RealNumbers Ra:Rb:Rc:Rhb:0 < b⊢ a * b⁻¹ < c ↔ a < c * b]R:Typeinst✝:RealNumbers Ra:Rb:Rc:Rhb:0 < b⊢ a * b⁻¹ < c ↔ a < c * b exact Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_lt_mul _ _ hbAll goals completed! 🐙theorem div_mul_cancel {a b : R} (hb : b≠0) : a/b*b=a := byR:Typeinst✝:RealNumbers Ra:Rb:Rhb:b ≠ 0⊢ a / b * b = a grindAll goals completed! 🐙theorem div_def (a b : R) : a/b=a*b⁻¹ := Lean.Grind.Field.div_eq_mul_inv a btheorem sub_self {a : R} : a-a=0 := byR:Typeinst✝:RealNumbers Ra:R⊢ a - a = 0 grindAll goals completed! 🐙theorem inv_zero : (0:R)⁻¹=0 := Lean.Grind.Field.inv_zerotheorem one_mul (a : R) : 1*a=a := byR:Typeinst✝:RealNumbers Ra:R⊢ 1 * a = a grindAll goals completed! 🐙theorem inv_mul_rev (a b : R) : (a*b)⁻¹=b⁻¹*a⁻¹ := byR:Typeinst✝:RealNumbers Ra:Rb:R⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹ grindAll goals completed! 🐙theorem natCast_mul (a b : Nat) : ((a*b : Nat) : R)=(a:R)*(b:R) := Lean.Grind.Semiring.natCast_mul a btheorem natCast_le_natCast {a b : Nat} : (a:R)≤(b:R) ↔ a≤b := byR:Typeinst✝:RealNumbers Ra:Natb:Nat⊢ ↑a ≤ ↑b ↔ a ≤ b constructormpR:Typeinst✝:RealNumbers Ra:Natb:Nat⊢ ↑a ≤ ↑b → a ≤ bmprR:Typeinst✝:RealNumbers Ra:Natb:Nat⊢ a ≤ b → ↑a ≤ ↑b ·mpR:Typeinst✝:RealNumbers Ra:Natb:Nat⊢ ↑a ≤ ↑b → a ≤ b exact Lean.Grind.OrderedRing.le_of_natCast_le_natCast a bAll goals completed! 🐙 ·mprR:Typeinst✝:RealNumbers Ra:Natb:Nat⊢ a ≤ b → ↑a ≤ ↑b exact Lean.Grind.OrderedRing.natCast_le_natCast_of_le a bAll goals completed! 🐙 theorem natCast_pos {a : Nat} : 0<(a:R) ↔ 0<a := byR:Typeinst✝:RealNumbers Ra:Nat⊢ 0 < ↑a ↔ 0 < a have hz : ((0:Nat):R)=0 := by grindR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0⊢ 0 < ↑a ↔ 0 < aR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0⊢ 0 < ↑a ↔ 0 < a constructormpR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0⊢ 0 < ↑a → 0 < amprR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0⊢ 0 < a → 0 < ↑a ·mpR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0⊢ 0 < ↑a → 0 < a intro hmpR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0h:0 < ↑a⊢ 0 < a exact Lean.Grind.OrderedRing.lt_of_natCast_lt_natCast (R := R) 0 a (byR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0h:0 < ↑a⊢ ↑0 < ↑a grindAll goals completed! 🐙) ·mprR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0⊢ 0 < a → 0 < ↑a intro hmprR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0h:0 < a⊢ 0 < ↑a have := Lean.Grind.OrderedRing.natCast_lt_natCast_of_lt (R:=R) 0 a hmprR:Typeinst✝:RealNumbers Ra:Nathz:↑0 = 0h:0 < athis:↑0 < ↑a⊢ 0 < ↑a simpa only [hz] using thisAll goals completed! 🐙theorem lt_iff_sub_pos (a b : R) : a<b ↔ 0<b-a := byR:Typeinst✝:RealNumbers Ra:Rb:R⊢ a < b ↔ 0 < b - a grindAll goals completed! 🐙