-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this_1 : NeZero n
this : NumberField.{u_1} ↥ℚ⟮ζ⟯
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₁ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₂ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₃ :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 1) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₄ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        ((algebraMap (↥ℚ⟮ζ⟯) K : (a : ↥ℚ⟮ζ⟯) → K) (HSub.hSub (α := ↥ℚ⟮ζ⟯) (AdjoinSimple.gen ℚ ζ) 1) : K) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
have rw₅ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : ↥ℚ⟮ζ⟯) → ℚ)
      ((Algebra.norm ↥ℚ⟮ζ⟯ : (a : K) → ↥ℚ⟮ζ⟯)
          ((algebraMap (↥ℚ⟮ζ⟯) K : (a : ↥ℚ⟮ζ⟯) → K) (HSub.hSub (α := ↥ℚ⟮ζ⟯) (AdjoinSimple.gen ℚ ζ) 1)) :
        ↥ℚ⟮ζ⟯) :
    ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ)
        ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
            (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
          ℤ)
        (Module.finrank (↥ℚ⟮ζ⟯) K)) :
    ℚ)
Tactic: rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]