refactor(NumberTheory): golf Mathlib/NumberTheory/NumberField/Norm

Mathlib/NumberTheory/NumberField/Norm.lean

@@ -68,21 +68,6 @@ theorem norm_algebraMap (x : 𝓞 K) : norm K (algebraMap (𝓞 K) (𝓞 L) x) =
     RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
     RingOfIntegers.coe_eq_algebraMap, map_pow]
 
-theorem isUnit_norm_of_isGalois [FiniteDimensional K L] [IsGalois K L] {x : 𝓞 L} :
-    IsUnit (norm K x) ↔ IsUnit x := by
-  classical
-  refine ⟨fun hx => ?_, IsUnit.map _⟩
-  replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
-  refine @isUnit_of_mul_isUnit_right (𝓞 L) _ _
-    ⟨(univ \ {AlgEquiv.refl}).prod fun σ : Gal(L/K) => σ x,
-      prod_mem fun σ _ => x.2.map (σ : L →+* L).toIntAlgHom⟩ _ ?_
-  convert hx using 1
-  ext
-  convert_to ((univ \ {AlgEquiv.refl}).prod fun σ : Gal(L/K) => σ x) *
-    ∏ σ ∈ {(AlgEquiv.refl : Gal(L/K))}, σ x = _
-  · simp
-  · rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
-
 /-- If `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)` we have that
 `x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x)`. -/
 theorem dvd_norm [FiniteDimensional K L] [IsGalois K L] (x : 𝓞 L) :
@@ -97,6 +82,10 @@ theorem dvd_norm [FiniteDimensional K L] [IsGalois K L] (x : 𝓞 L) :
   rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
   simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
 
+theorem isUnit_norm_of_isGalois [FiniteDimensional K L] [IsGalois K L] {x : 𝓞 L} :
+    IsUnit (norm K x) ↔ IsUnit x :=
+  ⟨fun hx ↦ isUnit_of_dvd_unit (dvd_norm K x) (hx.map _), IsUnit.map _⟩
+
 variable (F : Type*) [Field F] [Algebra K F] [FiniteDimensional K F]
 
 theorem norm_norm [Algebra F L] [FiniteDimensional F L] [IsScalarTower K F L] (x : 𝓞 L) :