diff --git a/Mathlib/NumberTheory/Cyclotomic/Gal.lean b/Mathlib/NumberTheory/Cyclotomic/Gal.lean
index 4fa73cdc884f22..2c186a7b95544f 100644
--- a/Mathlib/NumberTheory/Cyclotomic/Gal.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/Gal.lean
@@ -56,24 +56,11 @@ variable [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L]
 field extension. -/
 theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by
   intro f g hfg
-  apply_fun Units.val at hfg
-  simp only [IsPrimitiveRoot.coe_autToPow_apply] at hfg
-  generalize_proofs hf' hg' at hfg
-  have hf := hf'.choose_spec
-  have hg := hg'.choose_spec
-  generalize_proofs hζ at hf hg
-  suffices f (hμ.toRootsOfUnity : Lˣ) = g (hμ.toRootsOfUnity : Lˣ) by
-    apply AlgEquiv.coe_algHom_injective
+  have : f.toAlgHom = g.toAlgHom := by
     apply (hμ.powerBasis K).algHom_ext
-    exact this
-  rw [ZMod.natCast_eq_natCast_iff] at hfg
-  refine (hf.trans ?_).trans hg.symm
-  rw [← rootsOfUnity.coe_pow _ hf'.choose, ← rootsOfUnity.coe_pow _ hg'.choose]
-  congr 2
-  rw [pow_eq_pow_iff_modEq]
-  convert hfg
-  conv => enter [2]; rw [hμ.eq_orderOf, ← hμ.val_toRootsOfUnity_coe]
-  rw [orderOf_units, Subgroup.orderOf_coe]
+    rw [AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe, AlgHom.coe_coe,
+      powerBasis_gen, ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
+  exact AlgEquiv.coe_algHom_injective this
 
 end IsPrimitiveRoot