-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
⊢ ∀ (x y : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
        (Subring.closure
          (Set.range (ι := ZMod (n_1 + 1))
              (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
                (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
              (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
        x)
    (hy :
      Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
        (Subring.closure
          (Set.range (ι := ZMod (n_1 + 1))
              (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
                (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
              (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
        y),
    Eq (α := GaloisField (n_1 + 1) n)
        ((aeval x : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
        0 →
      Eq (α := GaloisField (n_1 + 1) n)
          ((aeval y : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
          0 →
        Eq (α := GaloisField (n_1 + 1) n)
          ((aeval (x * y) : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
          0
have succ : ∀ (x y : GaloisField (n_1 + 1) n)
  (hx :
    Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
      (Subring.closure
        (Set.range (ι := ZMod (n_1 + 1))
            (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
              (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
      x)
  (hy :
    Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
      (Subring.closure
        (Set.range (ι := ZMod (n_1 + 1))
            (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
              (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
      y),
  x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y
Tactic: simp only [aeval_X_pow, aeval_X, map_sub, mul_pow, sub_eq_zero]