mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1

Tactic:
this

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n m : ℕ
h : n ≠ m
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hnzero)

Goal state after:
case inl
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

case inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n = ∏ x_1 ∈ nthRootsFinset n 1, (algebraMap R K) (x - x_1 * y)

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n = ∏ x_1 ∈ nthRootsFinset n 1, (algebraMap R K) (x - x_1 * y)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
⊢ (↑(nthRootsFinset n 1)).ncard ≤ (↑(nthRootsFinset n 1)).ncard

Tactic:
simp [h.card_nthRootsFinset, h'.card_nthRootsFinset]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 < ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R) * ?h.inl.b

Tactic:
this

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 < ∑ i ∈ range n, x ^ i
⊢ 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
this : cyclotomic 6 ℤ = X ^ 2 - X + 1
⊢ map (Int.castRingHom R) (cyclotomic 6 ℤ) = X ^ 2 - X + 1

Tactic:
this

Goal state after:
R : Type u_1
inst✝ : Ring R
this : cyclotomic 6 ℤ = X ^ 2 - X + 1
⊢ map (Int.castRingHom R) (X ^ 2 - X + 1) = X ^ 2 - X + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ eval x (cyclotomic n R) * ?h.inr.inr.b < 0

Tactic:
this

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ ∑ i ∈ range n, x ^ i < 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : (cyclotomic (p ^ k * m) R).IsRoot μ
⊢ IsPrimitiveRoot μ m

pp: case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ

Tactic:
· rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow]
      at h
    replace h := eq_zero_of_pow_eq_zero h
    rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h

Goal state after:
case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m

Tactic:
by
  rcases k.eq_zero_or_pos with (rfl | hk)
  · rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow]
      at h
    replace h := eq_zero_of_pow_eq_zero h
    rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h
  · rw [← isRoot_cyclotomic_iff, IsRoot.def] at h
    rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow,
      h, zero_pow]
    exact Nat.sub_ne_zero_of_lt <| pow_right_strictMono₀ hp.out.one_lt <| Nat.pred_lt hk.ne'

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
set g_poly := (X ^ p ^ n - X : (ZMod p)[X])

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)
⊢ False

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)
⊢ False
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
this : g_poly.rootSet (GaloisField p n) = Set.univ
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
[

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
this : g_poly.rootSet (GaloisField p n) = Set.univ
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ x ∈ Algebra.adjoin (ZMod p) ((X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField),
    x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)

Tactic:
[

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ x ∈ Algebra.adjoin (ZMod p) ((X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField),
    x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
left; exact ⟨n, hn₁, hnpow⟩

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_1
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 ∈
      Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField,
    x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
[

Goal state after:
case succ.refine_1
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 ∈
      Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField,
    x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_2
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)
⊢ 0 ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
[

Goal state after:
case succ.refine_2
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)
⊢ 0 ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_3
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)
⊢ 1 ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
[

Goal state after:
case succ.refine_3
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)
⊢ 1 ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
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) →
        x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
          y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
            x + y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
[

Goal state after:
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) →
        x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
          y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
            x + y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
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),
    x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
      -x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
[

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),
    x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
      -x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
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) →
        x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
          y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
            x * y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
[

Goal state after:
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) →
        x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
          y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n) →
            x * y ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_1.inl
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)
r : ZMod (n✝ + 1)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) (r ^ (n✝ + 1) ^ n) -
      (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r =
    0

Tactic:
ZMod.pow_card_pow,

Goal state after:
case succ.refine_1.inl
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)
r : ZMod (n✝ + 1)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r - (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case refine_2
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ False

Tactic:
this

Goal state after:
case refine_2
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot (-1) n
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | n ≠ 0 ∧ b ^ n = 1} = ↑(nthRoots n 1).toFinset
⊢ {b | n ≠ 0 ∧ b ^ n = 1}.Finite

Tactic:
this

Goal state after:
case refine_1
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | n ≠ 0 ∧ b ^ n = 1} = ↑(nthRoots n 1).toFinset
⊢ (↑(nthRoots n 1).toFinset).Finite
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ✝ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ✝ : IsPrimitiveRoot ζ✝ n
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
ζ : ℂ
hζ : ζ ∈ primitiveRoots n ℂ
hhζ : ‖↑q - ζ‖ < q + 1
⊢ True ∧ ‖↑q - ζ‖ < ↑(q + 1).toNNReal

Tactic:
by simp [hhζ]

Goal state after: