diff --git a/Common.lean b/Common.lean
index dc64440..bd5e5a0 100644
--- a/Common.lean
+++ b/Common.lean
@@ -1,4 +1,3 @@
-import Common.Finset
 import Common.List
 import Common.Logic
 import Common.Real
diff --git a/Common/Finset.lean b/Common/Finset.lean
deleted file mode 100644
index 1fca96b..0000000
--- a/Common/Finset.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathlib.Data.Finset.Basic
-
-/-! # Common.Finset
-
-Additional theorems and definitions useful in the context of `Finset`s.
--/
-
-namespace Finset
-
-/--
-An alternative `Finset.range` function that returns `Fin` indices instead of `ℕ`
-indices.
--/
-def finRange (n : ℕ) : Finset (Fin n) :=
-  ⟨sorry, sorry⟩
-
-end Finset
\ No newline at end of file
diff --git a/Common/Geometry/StepFunction.lean b/Common/Geometry/StepFunction.lean
index 907165f..8a5b6b9 100644
--- a/Common/Geometry/StepFunction.lean
+++ b/Common/Geometry/StepFunction.lean
@@ -1,4 +1,3 @@
-import Common.Finset
 import Common.Geometry.Rectangle.Orthogonal
 import Common.List.Basic
 import Common.List.NonEmpty
@@ -73,19 +72,7 @@ namespace StepFunction
 /--
 The ordinate set of the `StepFunction`.
 -/
-def toSet (sf : StepFunction) : Set Point :=
-  ⋃ i ∈ Finset.finRange sf.ivls.length,
-    let I := sf.ivls[i]
-    Rectangle.Orthogonal.toSet
-      ⟨
-        {
-          tl := ⟨I.left, sf.toFun i⟩,
-          bl := ⟨I.left, 0⟩,
-          br := ⟨I.right, 0⟩,
-          has_right_angle := sorry
-        },
-        by simp
-      ⟩
+def toSet (sf : StepFunction) : Set Point := sorry
 
 end StepFunction
 
diff --git a/Common/Real.lean b/Common/Real.lean
index 21b63a3..baf1db9 100644
--- a/Common/Real.lean
+++ b/Common/Real.lean
@@ -1,4 +1,2 @@
 import Common.Real.Floor
-import Common.Real.Rational
-import Common.Real.Sequence
-import Common.Real.Trigonometry
\ No newline at end of file
+import Common.Real.Sequence
\ No newline at end of file
diff --git a/Common/Real/Rational.lean b/Common/Real/Rational.lean
deleted file mode 100644
index 98d68d2..0000000
--- a/Common/Real/Rational.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Rational
-
-Additional theorems and definitions useful in the context of rational numbers.
-Most of these will likely be deleted once the corresponding functions in
-`Mathlib` are ported to Lean 4.
--/
-
-/--
-Assert that a real number is irrational.
--/
-def irrational (x : ℝ) := x ∉ Set.range RatCast.ratCast
-
-/--
-Assert that a real number is rational.
--/
-def rational (x : ℝ) := ¬ irrational x
diff --git a/Common/Real/Trigonometry.lean b/Common/Real/Trigonometry.lean
deleted file mode 100644
index 8c673fb..0000000
--- a/Common/Real/Trigonometry.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Trigonometry
-
-Additional theorems and definitions useful in the context of trigonometry. Most
-of these will likely be deleted once the corresponding functions in `Mathlib`
-are ported to Lean 4.
--/
-
-namespace Real
-
-/--
-The standard `π` variable with value `3.14159...`.
--/
-axiom pi : ℝ
-
-/--
-The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
-either of those points equals `p₂`, this is `π / 2`.
--/
-axiom angle (p₁ p₂ p₃ : ℝ × ℝ) : ℝ
-
-noncomputable def euclideanAngle (p₁ p₂ p₃ : ℝ × ℝ) :=
-  if p₁ = p₂ ∨ p₂ = p₃ then pi / 2 else angle p₁ p₂ p₃
-
-end Real
\ No newline at end of file