diff --git a/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean b/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean
index 6e00ce2050..5e1f0ffe72 100644
--- a/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean
+++ b/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean
@@ -13,10 +13,10 @@ Rename
 * `map_add_mul` → `map_add_eq_mul`
 * `map_zero_one` → `map_zero_eq_one`
 * `map_nsmul_pow` → `map_nsmul_eq_pow`
-* `coe_to_fun_apply` → whatever is better, maybe change to `ψ.to_monoid_hom a = ψ (of_mul a)`.
+* `coe_toFun_apply` → whatever is better, maybe change to `ψ.toMonoidNom a = ψ (of_mul a)`.
 
-Kill the evil instance `add_char.monoid_hom_class`. It creates a diamond for
-`fun_like (add_char G R) _ _`.
+Kill the evil instance `AddChar.MonoidHomClass`. It creates a diamond for
+`FunLike (AddChar G R) _ _`.
 -/
 
 --TODO: This instance is evil
@@ -39,7 +39,7 @@ instance instFunLike : FunLike (AddChar G R) G fun _ ↦ R where
   coe := (⇑)
   coe_injective' ψ χ h := by obtain ⟨⟨_, _⟩, _⟩ := ψ; congr
 
--- TODO: Replace `add_char.to_monoid_hom`
+-- TODO: Replace `AddChar.toMonoidHom`
 /-- Interpret an additive character as a monoid homomorphism. -/
 def toMonoidHom' : AddChar G R ≃ (Multiplicative G →* R) := Equiv.refl _
 
diff --git a/blueprint/src/ap.tex b/blueprint/src/ap.tex
index 17d4af8e76..7306d3f994 100644
--- a/blueprint/src/ap.tex
+++ b/blueprint/src/ap.tex
@@ -110,7 +110,7 @@ \chapter{Almost-Periodicity}
 
 \begin{theorem}[$L_p$ almost periodicity]
 \label{lp_ap}
-\lean{almost_periodicity}
+\lean{AlmostPeriodicity.almost_periodicity}
 \leanok
 Let $\epsilon\in (0,1]$ and $m\geq 1$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$.
 Let $f:G\to \bbc$. There exists $T\subseteq G$ such that
diff --git a/blueprint/src/chang.tex b/blueprint/src/chang.tex
index 0d1b5f6eb8..a7ccb30685 100644
--- a/blueprint/src/chang.tex
+++ b/blueprint/src/chang.tex
@@ -85,7 +85,7 @@ \chapter{Chang's lemma}
 \begin{definition}[Energy]
 \label{energy}
 \uses{weight_energy}
-\lean{boring_energy}
+\lean{boringEnergy}
 \leanok
 Let $G$ be a finite abelian group and $A\subseteq G$. Let $m\geq 1$. We define
 \[E_{2m}(A)=\sum_{a_1,\ldots,a_{2m}\in A}1_{a_1+\cdots-a_{2m}=0}.\]
@@ -146,7 +146,7 @@ \chapter{Chang's lemma}
 \begin{lemma}
 \label{energy_alt}
 \uses{energy}
-\lean{boring_energy_eq}
+\lean{boringEnergy_eq}
 \leanok
 If $A\subset G$ and $m\geq 1$ then
 \[E_{2m}(A) = \sum_x 1_A^{(m)}(x)^2.\]
diff --git a/blueprint/src/ff.tex b/blueprint/src/ff.tex
index 18a33fce85..3811a16478 100644
--- a/blueprint/src/ff.tex
+++ b/blueprint/src/ff.tex
@@ -172,7 +172,7 @@ \chapter{Finite field model}
 
 \begin{lemma}
 \label{no3aps_inner_prod}
-\lean{add_salem_spencer.L2inner_mu_conv_mu_mu_two_smul_mu}
+\lean{AddSalemSpencer.l2inner_mu_conv_mu_mu_two_smul_mu}
 \leanok
 If $A\subseteq G$ has no non-trivial three-term arithmetic progressions and $G$ has odd order then
 \[\langle \mu_A\ast \mu_A,\mu_{2\cdot A}\rangle = 1/\abs{A}^2.\]