chore(ring_theory/adjoin_root): fix timeout by writing out simps ma…

…nually (#18209)

The `@[simps]` attribute on `adjoin_root.power_basis_aux'` is prone to timing out. Since `adjoin_root.power_basis_aux'` is defined as just a constructor application, we can't easily fix this by forbidding it from reducing or simplifying the result. So we'll have to work around this issue by defining the `@[simp]` lemmas manually. I left out `adjoin_root.power_basis_aux'_repr_apply_support_val` which says something about casting the support of the `repr` function to a multiset, since I can't imagine that one ever being useful, and we should be able to prove it for all `basis.of_equiv_fun` definitions anyway.

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`. -/