Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_4
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀ (x y : GaloisField (n✝ + 1) n),
    x ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      y ∈
          Subring.closure
            (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
              (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
        (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 →
          (aeval y) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (x + y)) (X ^ (n✝ + 1) ^ n - X) = 0

pp: case succ.refine_5
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀
    x ∈
      Subring.closure
        (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
          (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField),
    (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (-x)) (X ^ (n✝ + 1) ^ n - X) = 0

pp: case succ.refine_6
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀ (x y : GaloisField (n✝ + 1) n),
    x ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      y ∈
          Subring.closure
            (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
              (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
        (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 →
          (aeval y) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (x * y)) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
· simp only [aeval_X_pow, aeval_X, map_sub, add_pow_char_pow, sub_eq_zero]
    intro x y _ _ hx hy
    rw [hx, hy]

Goal state after:
case succ.refine_5
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀
    x ∈
      Subring.closure
        (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
          (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField),
    (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (-x)) (X ^ (n✝ + 1) ^ n - X) = 0

case succ.refine_6
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀ (x y : GaloisField (n✝ + 1) n),
    x ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      y ∈
          Subring.closure
            (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
              (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
        (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 →
          (aeval y) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (x * y)) (X ^ (n✝ + 1) ^ n - X) = 0