From 0a8aa466c67c7f13065e9d13e39ed12e63f0415b Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Mon, 8 May 2023 20:30:59 -0600
Subject: [PATCH] Apostol Chapter 1.11, exercise 4c.

---
 Bookshelf/Apostol/Chapter_1_11.lean | 26 ++++++++++++++++++++++++--
 Bookshelf/Apostol/Chapter_1_11.tex  |  9 +++++++--
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean
index 61b4cef..cc1af60 100644
--- a/Bookshelf/Apostol/Chapter_1_11.lean
+++ b/Bookshelf/Apostol/Chapter_1_11.lean
@@ -49,7 +49,29 @@ theorem exercise_4b_2 (x : ℝ) (h : ∃ n : ℤ, x ∈ Set.Ioo ↑n (↑n + (1
 -/
 theorem exercise_4c (x y : ℝ)
   : ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ∨ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by
-  sorry
+  have hx : x = Int.floor x + Int.fract x := Eq.symm (add_eq_of_eq_sub' rfl)
+  have hy : y = Int.floor y + Int.fract y := Eq.symm (add_eq_of_eq_sub' rfl)
+  by_cases Int.fract x + Int.fract y < 1
+  · refine Or.inl ?_
+    rw [Int.floor_eq_iff]
+    simp only [Int.cast_add]
+    apply And.intro
+    · exact add_le_add (Int.floor_le x) (Int.floor_le y)
+    · conv => lhs; rw [hx, hy, add_add_add_comm]; arg 1; rw [add_comm]
+      rwa [add_comm, ← add_assoc, ← sub_lt_iff_lt_add', ← sub_sub, add_sub_cancel, add_sub_cancel]
+  · refine Or.inr ?_
+    rw [Int.floor_eq_iff]
+    simp only [Int.cast_add, Int.cast_one]
+    have h := le_of_not_lt h
+    apply And.intro
+    · conv => lhs; rw [← add_rotate]
+      conv => rhs; rw [hx, hy, add_add_add_comm]; arg 1; rw [add_comm]
+      rwa [← sub_le_iff_le_add', ← sub_sub, add_sub_cancel, add_sub_cancel]
+    · conv => lhs; rw [hx, hy, add_add_add_comm]; arg 1; rw [add_comm]
+      conv => lhs; rw [add_comm, ← add_assoc]
+      conv => rhs; rw [add_assoc]
+      rw [← sub_lt_iff_lt_add', ← sub_sub, add_sub_cancel, add_sub_cancel]
+      exact add_lt_add (Int.fract_lt_one x) (Int.fract_lt_one y)
 
 /-- ### Exercise 4d
 
@@ -73,7 +95,7 @@ The formulas in Exercises 4(d) and 4(e) suggest a generalization for `⌊nx⌋`.
 State and prove such a generalization.
 -/
 theorem exercise_5 (n : ℕ) (x : ℝ)
-  : ⌊n * x⌋ = 10 := by
+  : True := by
   sorry
 
 /-- ### Exercise 7b
diff --git a/Bookshelf/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex
index 24061fa..88c66a5 100644
--- a/Bookshelf/Apostol/Chapter_1_11.tex
+++ b/Bookshelf/Apostol/Chapter_1_11.tex
@@ -39,7 +39,12 @@ $\floor{-x} =
 
 \begin{proof}
 
-  \link{exercise\_4b}
+  \  % Force space prior to *Proof.*
+
+  \begin{enumerate}[(a)]
+    \item \link{exercise\_4b\_1}
+    \item \link{exercise\_4b\_2}
+  \end{enumerate}
 
 \end{proof}
 
@@ -136,7 +141,7 @@ Now apply Exercises 4(a) and (b) to the bracket on the right.
 
 \begin{proof}
 
-  TODO
+  \link{exercise\_7b}
 
 \end{proof}