diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean
index 4d8c81e2496b2..6fb17d1e38b18 100644
--- a/src/ring_theory/adjoin_root.lean
+++ b/src/ring_theory/adjoin_root.lean
@@ -334,8 +334,17 @@ basis.of_equiv_fun
       exact (degree_eq_nat_degree $ hg.ne_zero).symm ▸ degree_sum_fin_lt _ },
   end}
 
--- This was moved after the definition to prevent a timeout
-attribute [simps] power_basis_aux'
+/-- This lemma could be autogenerated by `@[simps]` but unfortunately that would require
+unfolding that causes a timeout. -/
+@[simp] lemma power_basis_aux'_repr_symm_apply (hg : g.monic) (c : fin g.nat_degree →₀ R) :
+  (power_basis_aux' hg).repr.symm c = mk g (∑ (i : fin _), monomial i (c i)) := rfl
+
+/-- This lemma could be autogenerated by `@[simps]` but unfortunately that would require
+unfolding that causes a timeout. -/
+@[simp] theorem power_basis_aux'_repr_apply_to_fun (hg : g.monic) (f : adjoin_root g)
+  (i : fin g.nat_degree) :
+  (power_basis_aux' hg).repr f i = (mod_by_monic_hom hg f).coeff ↑i :=
+rfl
 
 /-- The power basis `1, root g, ..., root g ^ (d - 1)` for `adjoin_root g`,
 where `g` is a monic polynomial of degree `d`. -/