diff --git a/PFR.lean b/PFR.lean
index a87e9795..de6b24f6 100644
--- a/PFR.lean
+++ b/PFR.lean
@@ -2,6 +2,7 @@ import PFR.ApproxHomPFR
 import PFR.BoundingMutual
 import PFR.Endgame
 import PFR.EntropyPFR
+import PFR.Examples
 import PFR.Fibring
 import PFR.FirstEstimate
 import PFR.ForMathlib.AffineSpaceDim
diff --git a/examples.lean b/PFR/Examples.lean
similarity index 98%
rename from examples.lean
rename to PFR/Examples.lean
index e1ae47cf..51d55c86 100644
--- a/examples.lean
+++ b/PFR/Examples.lean
@@ -32,9 +32,8 @@ example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K
 /-- The even more improved version -/
 example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
     ∃ (H : Submodule (ZMod 2) G) (c : Set G),
-      Nat.card c < 2 * K ^ 9 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
-  convert better_PFR_conjecture h₀A hA
-  norm_cast
+      Nat.card c < 2 * K ^ 9 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H :=
+  better_PFR_conjecture h₀A hA
 
 #print axioms better_PFR_conjecture
 
@@ -200,7 +199,7 @@ example {a : ℝ≥0∞} (ha : a < ∞) : a + 3 < ∞ := by finiteness
 
 example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ∞ := by finiteness
 
-example (f : α → ℕ) : ∀ i, (f i : ℝ≥0∞) ≠ ∞ := by finiteness
+example {α : Type*} (f : α → ℕ) : ∀ i, (f i : ℝ≥0∞) ≠ ∞ := by finiteness
 
 open MeasureTheory
 
@@ -208,5 +207,4 @@ example {Ω Ω' : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsFiniteMeasure
     (ν' : Measure Ω') [IsFiniteMeasure ν'] (E : Set (Ω × Ω')) :
     (ν.prod ν') E < ∞ := by finiteness
 
-
 end Finiteness