diff --git a/Bookshelf/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean
index 2f02b47..c5f0b39 100644
--- a/Bookshelf/Apostol/Chapter_I_03.lean
+++ b/Bookshelf/Apostol/Chapter_I_03.lean
@@ -352,8 +352,8 @@ has a supremum, and `sup C = sup A + sup B`.
 theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ)
   (hA : A.Nonempty) (hB : B.Nonempty)
   (ha : IsLUB A a) (hb : IsLUB B b)
-  : IsLUB (Set.minkowski_sum A B) (a + b) := by
-  let C := Set.minkowski_sum A B
+  : IsLUB (Set.minkowskiSum A B) (a + b) := by
+  let C := Set.minkowskiSum A B
   -- First we show `a + b` is an upper bound of `C`.
   have hub : a + b ∈ upperBounds C := by
     rw [mem_upper_bounds_iff_forall_le]
@@ -402,8 +402,8 @@ has an infimum, and `inf C = inf A + inf B`.
 theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ)
   (hA : A.Nonempty) (hB : B.Nonempty)
   (ha : IsGLB A a) (hb : IsGLB B b)
-  : IsGLB (Set.minkowski_sum A B) (a + b) := by
-  let C := Set.minkowski_sum A B
+  : IsGLB (Set.minkowskiSum A B) (a + b) := by
+  let C := Set.minkowskiSum A B
   -- First we show `a + b` is a lower bound of `C`.
   have hlb : a + b ∈ lowerBounds C := by
     rw [mem_lower_bounds_iff_forall_ge]
@@ -616,10 +616,9 @@ An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd* if
 ###### TODO
 -/
 
+def isEven (n : ℤ) := ∃ m : ℤ, n = 2 * m
 
-def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m
-
-def is_odd (n : ℤ) := is_even (n + 1)
+def isOdd (n : ℤ) := isEven (n + 1)
 
 /-! #### Exercise 11
 
diff --git a/Bookshelf/Enderton/Chapter_0.lean b/Bookshelf/Enderton/Chapter_0.lean
index 5ef44b3..24b344c 100644
--- a/Bookshelf/Enderton/Chapter_0.lean
+++ b/Bookshelf/Enderton/Chapter_0.lean
@@ -219,13 +219,13 @@ private lemma n_pred_m_eq_m_k : n + (m - 1) = m + k := by
   rw [←Nat.add_sub_assoc p, Nat.add_comm, Nat.add_sub_assoc (n_geq_one p q)]
   conv => lhs; rw [n_pred_eq_k p q]
 
-private def cast_norm : GTuple α (n, m - 1) → LTuple α (m + k)
+private def castNorm : GTuple α (n, m - 1) → LTuple α (m + k)
   | xs => cast (by rw [q]) xs.norm
 
-private def cast_fst : GTuple α (n, m - 1) → LTuple α (k + 1)
+private def castFst : GTuple α (n, m - 1) → LTuple α (k + 1)
   | xs => cast (by rw [n_eq_succ_k p q]) xs.fst
 
-private def cast_take (ys : LTuple α (m + k)) :=
+private def castTake (ys : LTuple α (m + k)) :=
   cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1))
 
 /-- #### Lemma 0A
@@ -234,7 +234,7 @@ Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Th
 `x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
 -/
 theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k))
-  : (cast_norm q xs = ys) → (cast_fst p q xs = cast_take p ys) := by
+  : (castNorm q xs = ys) → (castFst p q xs = castTake p ys) := by
   intro h
   suffices HEq
     (cast (_ : LTuple α n = LTuple α (k + 1)) xs.fst)
@@ -257,7 +257,7 @@ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k))
   · exact Eq.symm (n_eq_min_comm_succ p q)
   · exact n_pred_eq_k p q
   · rw [GTuple.self_fst_eq_norm_take]
-    unfold cast_norm at h
+    unfold castNorm at h
     simp at h
     rw [←h, ←n_eq_succ_k p q]
     have h₂ := Eq.recOn
diff --git a/Common/Real/Geometry/Area.lean b/Common/Real/Geometry/Area.lean
index 6bae72b..39be5d3 100644
--- a/Common/Real/Geometry/Area.lean
+++ b/Common/Real/Geometry/Area.lean
@@ -89,7 +89,7 @@ axiom congruent_imp_area_eq_area
 -/
 
 axiom rectangle_measurable (R : Rectangle)
-  : R.set_def ∈ 𝓜
+  : R.toSet ∈ 𝓜
 
 axiom rectangle_area_eq_mul_edge_lengths (R : Rectangle)
   : area (rectangle_measurable R) = R.width * R.height
@@ -107,23 +107,23 @@ Every step region is measurable. This follows from the choice of scale axiom,
 and the fact all step regions are equivalent to the union of a collection of
 rectangles.
 -/
-theorem step_function_measurable (S : StepFunction) : S.set_def ∈ 𝓜 := by
+theorem step_function_measurable (S : StepFunction) : S.toSet ∈ 𝓜 := by
   sorry
 
-def forall_subset_between_step_imp_le_between_area (k : ℝ) (Q : Set ℝ²) :=
+def exhaustionProperty (k : ℝ) (Q : Set ℝ²) :=
   ∀ S T : StepFunction,
-    (hS : S.set_def ⊆ Q) →
-    (hT : Q ⊆ T.set_def) →
+    (hS : S.toSet ⊆ Q) →
+    (hT : Q ⊆ T.toSet) →
     area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T)
 
 axiom exhaustion_exists_unique_imp_measurable (Q : Set ℝ²)
-  : (∃! k : ℝ, forall_subset_between_step_imp_le_between_area k Q)
+  : (∃! k : ℝ, exhaustionProperty k Q)
   → Q ∈ 𝓜
 
 axiom exhaustion_exists_unique_imp_area_eq (Q : Set ℝ²)
   : ∃ k : ℝ,
-      (h : forall_subset_between_step_imp_le_between_area k Q ∧
-        (∀ x : ℝ, forall_subset_between_step_imp_le_between_area x Q → x = k))
+      (h : exhaustionProperty k Q ∧
+        (∀ x : ℝ, exhaustionProperty x Q → x = k))
     → area (exhaustion_exists_unique_imp_measurable Q ⟨k, h⟩) = k
 
 end Real.Geometry.Area
diff --git a/Common/Real/Geometry/Basic.lean b/Common/Real/Geometry/Basic.lean
index a4c7a1b..33ff993 100644
--- a/Common/Real/Geometry/Basic.lean
+++ b/Common/Real/Geometry/Basic.lean
@@ -20,10 +20,10 @@ definition once ported.
 -/
 axiom angle (p₁ p₂ p₃ : ℝ²) : ℝ
 
-noncomputable def port_geometry_euclidean_angle (p₁ p₂ p₃ : ℝ²) :=
+noncomputable def euclideanAngle (p₁ p₂ p₃ : ℝ²) :=
   if p₁ = p₂ ∨ p₂ = p₃ then π / 2 else angle p₁ p₂ p₃
 
-notation "∠" => port_geometry_euclidean_angle
+notation "∠" => euclideanAngle
 
 /--
 Determine the distance between two points in `ℝ²`.
diff --git a/Common/Real/Geometry/Rectangle.lean b/Common/Real/Geometry/Rectangle.lean
index 5ebc700..d07f71f 100644
--- a/Common/Real/Geometry/Rectangle.lean
+++ b/Common/Real/Geometry/Rectangle.lean
@@ -28,7 +28,7 @@ namespace Rectangle
 The top-right corner of the rectangle, oriented with respect to the other
 vertices.
 -/
-def top_right (r : Rectangle) : ℝ² :=
+def topRight (r : Rectangle) : ℝ² :=
   ( r.top_left.fst + r.bottom_right.fst - r.bottom_left.fst
   , r.top_left.snd + r.bottom_right.snd - r.bottom_left.snd
   )
@@ -36,23 +36,23 @@ def top_right (r : Rectangle) : ℝ² :=
 /--
 A `Rectangle` is the locus of points bounded by its edges.
 -/
-def set_def (r : Rectangle) : Set ℝ² :=
+def toSet (r : Rectangle) : Set ℝ² :=
   sorry
 
 /--
 A `Rectangle`'s top side is equal in length to its bottom side.
 -/
 theorem dist_top_eq_dist_bottom (r : Rectangle)
-  : dist r.top_left r.top_right = dist r.bottom_left r.bottom_right := by
-  unfold top_right dist
+  : dist r.top_left r.topRight = dist r.bottom_left r.bottom_right := by
+  unfold topRight dist
   repeat rw [add_comm, sub_right_comm, add_sub_cancel']
 
 /--
 A `Rectangle`'s left side is equal in length to its right side.
 -/
 theorem dist_left_eq_dist_right (r : Rectangle)
-  : dist r.top_left r.bottom_left = dist r.top_right r.bottom_right := by
-  unfold top_right dist
+  : dist r.top_left r.bottom_left = dist r.topRight r.bottom_right := by
+  unfold topRight dist
   repeat rw [
     sub_sub_eq_add_sub,
     add_comm,
@@ -86,7 +86,7 @@ namespace Point
 /--
 A `Point` is the set consisting of just itself.
 -/
-def set_def (p : Point) : Set ℝ² := p.val.set_def
+def toSet (p : Point) : Set ℝ² := p.val.toSet
 
 /--
 The width of a `Point` is `0`.
@@ -121,7 +121,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 ℝ² := s.val.set_def
+def toSet (s : LineSegment) : Set ℝ² := s.val.toSet
 
 /--
 Either the width or height of a `LineSegment` is zero.
diff --git a/Common/Real/Geometry/StepFunction.lean b/Common/Real/Geometry/StepFunction.lean
index c8c16df..25544a2 100644
--- a/Common/Real/Geometry/StepFunction.lean
+++ b/Common/Real/Geometry/StepFunction.lean
@@ -154,7 +154,7 @@ namespace StepFunction
 The set definition of a `StepFunction` is the region between the constant values
 of the function's subintervals and the real axis.
 -/
-def set_def (f : StepFunction) : Set ℝ² := sorry
+def toSet (f : StepFunction) : Set ℝ² := sorry
 
 end StepFunction
 
diff --git a/Common/Real/Sequence/Arithmetic.lean b/Common/Real/Sequence/Arithmetic.lean
index 469047e..97a5500 100644
--- a/Common/Real/Sequence/Arithmetic.lean
+++ b/Common/Real/Sequence/Arithmetic.lean
@@ -72,7 +72,7 @@ The summation of the first `n + 1` terms of an arithmetic sequence.
 
 This function calculates the sum directly.
 -/
-noncomputable def sum_closed (seq : Arithmetic) (n : Nat) : Real :=
+noncomputable def sumClosed (seq : Arithmetic) (n : Nat) : Real :=
   (n + 1) * (seq.a₀ + seq.termClosed n) / 2
 
 /--
@@ -80,9 +80,9 @@ The summation of the first `n + 1` terms of an arithmetic sequence.
 
 This function calculates the sum recursively.
 -/
-def sum_recursive : Arithmetic → Nat → Real
+def sumRecursive : Arithmetic → Nat → Real
   | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
+  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sumRecursive n
 
 /--
 Simplify a summation of terms found in the proof of `sum_recursive_closed`.
@@ -101,16 +101,16 @@ The recursive and closed definitions of the sum of an arithmetic sequence agree
 with one another.
 -/
 theorem sum_recursive_closed (seq : Arithmetic) (n : Nat)
-  : seq.sum_recursive n = seq.sum_closed n := by
+  : seq.sumRecursive n = seq.sumClosed n := by
   induction n with
   | zero =>
-    unfold sum_recursive sum_closed termClosed
+    unfold sumRecursive sumClosed termClosed
     norm_num
   | succ n ih =>
     calc
-      seq.sum_recursive (n + 1)
-      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
-      _ = seq.termClosed (n + 1) + seq.sum_closed n := by rw [ih]
+      seq.sumRecursive (n + 1)
+      _ = seq.termClosed (n + 1) + seq.sumRecursive n := rfl
+      _ = seq.termClosed (n + 1) + seq.sumClosed n := by rw [ih]
       _ = seq.termClosed (n + 1) + ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 := rfl
       _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed n + seq.a₀ + seq.termClosed n) / 2 := by ring_nf
       _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * (seq.termClosed (n + 1) - seq.Δ) + seq.a₀ + (seq.termClosed (n + 1) - seq.Δ)) / 2 := by rw [@term_closed_sub_succ_delta n]
@@ -118,6 +118,6 @@ theorem sum_recursive_closed (seq : Arithmetic) (n : Nat)
       _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + 2 * seq.a₀) / 2 := by rw [sub_delta_summand_eq_two_mul_a₀]
       _ = ((n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by ring_nf
       _ = (↑(n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by simp only [Nat.cast_add, Nat.cast_one]
-      _ = seq.sum_closed (n + 1) := rfl
+      _ = seq.sumClosed (n + 1) := rfl
 
 end Real.Arithmetic
\ No newline at end of file
diff --git a/Common/Real/Sequence/Geometric.lean b/Common/Real/Sequence/Geometric.lean
index 50b2187..7bda2e4 100644
--- a/Common/Real/Sequence/Geometric.lean
+++ b/Common/Real/Sequence/Geometric.lean
@@ -57,7 +57,7 @@ The summation of the first `n + 1` terms of a geometric sequence.
 
 This function calculates the sum directly.
 -/
-noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat)
+noncomputable def sumClosed (seq : Geometric) (n : Nat)
   : seq.r ≠ 1 → Real :=
   fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r)
 
@@ -66,33 +66,33 @@ The summation of the first `n + 1` terms of a geometric sequence.
 
 This function calculates the sum recursively.
 -/
-def sum_recursive : Geometric → Nat → Real
+def sumRecursive : Geometric → Nat → Real
   | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
+  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sumRecursive n
 
 /--
 The recursive and closed definitions of the sum of a geometric sequence agree
 with one another.
 -/
 theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1)
-  : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by
+  : sumRecursive seq n = sumClosed seq n p := by
   have h : 1 - seq.r ≠ 0 := by
     intro h
     rw [sub_eq_iff_eq_add, zero_add] at h
     exact False.elim (p (Eq.symm h))
   induction n with
   | zero =>
-    unfold sum_recursive sum_closed_ratio_neq_one
+    unfold sumRecursive sumClosed
     simp
     rw [mul_div_assoc, div_self h, mul_one] 
   | succ n ih =>
     calc
-      sum_recursive seq (n + 1)
-      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
-      _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih]
+      sumRecursive seq (n + 1)
+      _ = seq.termClosed (n + 1) + seq.sumRecursive n := rfl
+      _ = seq.termClosed (n + 1) + seq.sumClosed n p := by rw [ih]
       _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl
       _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h]
       _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf
-      _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl
+      _ = seq.sumClosed (n + 1) p := rfl
 
 end Real.Geometric
\ No newline at end of file
diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean
index c1ed9ea..e255ca1 100644
--- a/Common/Set/Basic.lean
+++ b/Common/Set/Basic.lean
@@ -11,7 +11,7 @@ namespace Set
 The Minkowski sum of two sets `s` and `t` is the set
 `s + t = { a + b : a ∈ s, b ∈ t }`.
 -/
-def minkowski_sum {α : Type u} [Add α] (s t : Set α) :=
+def minkowskiSum {α : Type u} [Add α] (s t : Set α) :=
   { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }
 
 /--
@@ -19,7 +19,7 @@ The sum of two sets is nonempty **iff** the summands are nonempty.
 -/
 theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
   {s t : Set α}
-  : (minkowski_sum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
+  : (minkowskiSum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
   apply Iff.intro
   · intro h
     have ⟨x, hx⟩ := h