From fcbd510dbee9b9727300001f3ff698a8c9228e61 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Tue, 2 May 2023 11:29:42 -0600
Subject: [PATCH] Fix up (ir)rational definition and point/line segment set
 definitions.

---
 Bookshelf/Real/Rational.lean                      | 12 ++++++------
 OneVariableCalculus/Apostol/Exercises_I_3_12.lean |  2 +-
 OneVariableCalculus/Real/Geometry/Rectangle.lean  |  6 ++----
 3 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/Bookshelf/Real/Rational.lean b/Bookshelf/Real/Rational.lean
index fb69634..ee08068 100644
--- a/Bookshelf/Real/Rational.lean
+++ b/Bookshelf/Real/Rational.lean
@@ -1,14 +1,14 @@
 import Bookshelf.Real.Basic
 
+/--
+Assert that a real number is irrational.
+-/
+def irrational (x : ℝ) := x ∉ Set.range RatCast.ratCast
+
 /--
 Assert that a real number is rational.
 
 Note this does *not* require the found rational to be in reduced form. Members
 of `ℚ` expect this (by proving the numerator and denominator are co-prime).
 -/
-def rational (x : ℝ) := ∃ a : ℤ, ∃ b : ℕ, b ≠ 0 ∧ x = a / b
-
-/--
-Assert that a real number is irrational.
--/
-def irrational (x : ℝ) := ¬ rational x
+def rational (x : ℝ) := ¬ irrational x
diff --git a/OneVariableCalculus/Apostol/Exercises_I_3_12.lean b/OneVariableCalculus/Apostol/Exercises_I_3_12.lean
index b4538c0..985fd26 100644
--- a/OneVariableCalculus/Apostol/Exercises_I_3_12.lean
+++ b/OneVariableCalculus/Apostol/Exercises_I_3_12.lean
@@ -112,7 +112,7 @@ example (x y : ℝ) (h : x < y) : ∃ r : ℚ, x < r ∧ r < y := by
 -- ========================================
 
 example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
-  : irrational (x + y) := by
+  : irrational (x + y) :=
   sorry
 
 example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
diff --git a/OneVariableCalculus/Real/Geometry/Rectangle.lean b/OneVariableCalculus/Real/Geometry/Rectangle.lean
index 2585b87..6d6c7ef 100644
--- a/OneVariableCalculus/Real/Geometry/Rectangle.lean
+++ b/OneVariableCalculus/Real/Geometry/Rectangle.lean
@@ -70,8 +70,7 @@ namespace Point
 /--
 A `Point` is the set consisting of just itself.
 -/
-def set_def (p : Point) : Set ℝ² :=
-  { x : ℝ² | x = p.val.top_left }
+def set_def (p : Point) : Set ℝ² := p.val.set_def
 
 /--
 The width of a `Point` is `0`.
@@ -106,8 +105,7 @@ namespace LineSegment
 A `LineSegment` `s` is the set of points corresponding to the shortest line
 segment joining the two distinct points of `s`.
 -/
-def set_def (s : LineSegment) : Set ℝ² :=
-  sorry
+def set_def (s : LineSegment) : Set ℝ² := s.val.set_def
 
 /--
 Either the width or height of a `LineSegment` is zero.