awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
r : ZMod (n_1 + 1)
⊢ Eq (α := GaloisField (n_1 + 1) n)
    (((aeval
            ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n)
              r) :
          (ZMod (n_1 + 1))[X] →ₐ[ZMod (n_1 + 1)] GaloisField (n_1 + 1) n) :
        (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 : HSub.hSub (β := GaloisField (n_1 + 1) n)
    (HPow.hPow (α := GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n)
      ((n_1 + 1) ^ n))
    ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
      GaloisField (n_1 + 1) n) =
  0
Tactic: simp only [map_sub, map_pow, aeval_X]
-- 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
r : ZMod (n_1 + 1)
⊢ HSub.hSub (β := GaloisField (n_1 + 1) n)
      (HPow.hPow (α := GaloisField (n_1 + 1) n)
        ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
          GaloisField (n_1 + 1) n)
        ((n_1 + 1) ^ n))
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
have succ : HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
    ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n)
        (r ^ (n_1 + 1) ^ n) :
      GaloisField (n_1 + 1) n)
    ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
      GaloisField (n_1 + 1) n) =
  0
Tactic: rw [← map_pow, ZMod.pow_card_pow, sub_self]
-- 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
r : ZMod (n_1 + 1)
succ :
  HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n)
          (r ^ (n_1 + 1) ^ n) :
        GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
⊢ HSub.hSub (β := GaloisField (n_1 + 1) n)
      (HPow.hPow (α := GaloisField (n_1 + 1) n)
        ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
          GaloisField (n_1 + 1) n)
        ((n_1 + 1) ^ n))
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
have succ₁ : HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
    ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
      GaloisField (n_1 + 1) n)
    ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
      GaloisField (n_1 + 1) n) =
  0
Tactic: rw [← map_pow, ZMod.pow_card_pow, sub_self]
-- 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
r : ZMod (n_1 + 1)
succ :
  HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n)
          (r ^ (n_1 + 1) ^ n) :
        GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
succ₁ :
  HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
⊢ HSub.hSub (β := GaloisField (n_1 + 1) n)
      (HPow.hPow (α := GaloisField (n_1 + 1) n)
        ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
          GaloisField (n_1 + 1) n)
        ((n_1 + 1) ^ n))
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
have succ₂ : Eq (α := GaloisField (n_1 + 1) n) 0 0
Tactic: rw [← map_pow, ZMod.pow_card_pow, sub_self]
-- 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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Set (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
    ((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
⊢ 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
have succ : ∀
  (hx :
    Eq (α := (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
      ((aeval x : (a : (ZMod (n_1 + 1))[X]) → (X ^ (n_1 + 1) ^ n - X).SplittingField)
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
      0),
  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
Tactic: rwa [mem_rootSet_of_ne aux] at hx
Cleared hypotheses: hx
-- 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
⊢ Eq (α := GaloisField (n_1 + 1) n)
    ((aeval 0 : (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 : Eq (α := GaloisField (n_1 + 1) n)
  ((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).coeff 0) :
    GaloisField (n_1 + 1) n)
  (0 : GaloisField (n_1 + 1) n)
Tactic: rw [← coeff_zero_eq_aeval_zero']
-- 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
⊢ Eq (α := GaloisField (n_1 + 1) n)
    ((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).coeff 0) :
      GaloisField (n_1 + 1) n)
    (0 : GaloisField (n_1 + 1) n)
have succ : 0 = (n_1 + 1) ^ n → False
Tactic: simp only [coeff_X_pow, coeff_X_zero, sub_zero, _root_.map_eq_zero, ite_eq_right_iff,
      one_ne_zero, coeff_sub]
-- 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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x y : GaloisField (n_1 + 1) n
hx_2 :
  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_1 :
  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
hx : x ^ (n_1 + 1) ^ n = x
hy : y ^ (n_1 + 1) ^ n = y
⊢ x ^ (n_1 + 1) ^ n + y ^ (n_1 + 1) ^ n = x + y
have succ : x + y ^ (n_1 + 1) ^ n = x + y
Tactic: rw [hx, hy]
-- 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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x y : GaloisField (n_1 + 1) n
hx_2 :
  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_1 :
  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
hx : x ^ (n_1 + 1) ^ n = x
hy : y ^ (n_1 + 1) ^ n = y
succ : x + y ^ (n_1 + 1) ^ n = x + y
⊢ x ^ (n_1 + 1) ^ n + y ^ (n_1 + 1) ^ n = x + y
have succ₁ : x + y = x + y
Tactic: rw [hx, hy]
-- 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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x : GaloisField (n_1 + 1) n
hx_2 :
  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
hx :
  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 (-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
have succ : ∀ (hx : x ^ (n_1 + 1) ^ n = x), (-x) ^ (n_1 + 1) ^ n + x = 0
Tactic: simp only [g_poly, sub_eq_zero, aeval_X_pow, aeval_X, map_sub, sub_neg_eq_add] at *
Cleared hypotheses: hx
-- 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
      (↑((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) : Type) =
    (n_1 + 1) ^ n
nat_degree_eq : (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).natDegree = (n_1 + 1) ^ n
x_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x : GaloisField (n_1 + 1) n
hx_2 :
  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
hx : x ^ (n_1 + 1) ^ n = x
⊢ (-x) ^ (n_1 + 1) ^ n + x = 0
have succ : -1 * x + x = 0
Tactic: rw [neg_pow, hx, neg_one_pow_char_pow]
-- 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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x y : GaloisField (n_1 + 1) n
hx_2 :
  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_1 :
  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
hx : x ^ (n_1 + 1) ^ n = x
hy : y ^ (n_1 + 1) ^ n = y
⊢ x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y
have succ : x * y ^ (n_1 + 1) ^ n = x * y
Tactic: rw [hx, hy]
-- 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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x y : GaloisField (n_1 + 1) n
hx_2 :
  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_1 :
  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
hx : x ^ (n_1 + 1) ^ n = x
hy : y ^ (n_1 + 1) ^ n = y
succ : x * y ^ (n_1 + 1) ^ n = x * y
⊢ x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y
have succ₁ : x * y = x * y
Tactic: rw [hx, hy]