-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
η : ↥(rootsOfUnity n K)
this : (↑(↑η : Kˣ) : K) ^ n = 1
rw :
  HSub.hSub (α := K[n√a]) (β := K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          (HPow.hPow (α := K [X]) X n) :
        K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₁ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          X)
        n)
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₂ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          X)
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
rw₃ :
  HSub.hSub (β := K[n√a])
      (((↑(↑η : Kˣ) : K) •
          root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
rw₄ :
  HSub.hSub (β := K[n√a])
      (HMul.hMul (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) (↑(↑η : Kˣ) : K) : K[n√a])
          (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
rw₅ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) (↑(↑η : Kˣ) : K) : K[n√a]) n *
        root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
        (a_1 : K [X]) → K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
    0
have rw₆ : HSub.hSub (β := K[n√a])
    (HMul.hMul (β := K[n√a])
      (HPow.hPow (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) (↑(↑η : Kˣ) : K) : K[n√a]) n)
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
          a :
        K[n√a]))
    ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]