-- 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
succ :
  ∀ (x : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        (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),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
succ₁ :
  Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 0
succ₂ :
  Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 1
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),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x →
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
          ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) y →
        Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
          ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) (x + y)
succ₄ :
  ∀ (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),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x →
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) (-x)
⊢ Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
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),
  Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x →
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) y →
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) (x * y)
Tactic: refine Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx