mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : { i // n i ≠ 0 }
x : ZMod (p ↑i ^ n ↑i)
⊢ (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((DirectSum.of (fun i ↦ ZMod (p i ^ n i)) ↑i) x) =
    (DirectSum.of (fun i ↦ ZMod (p ↑i ^ n ↑i)) i) x

Tactic:
DirectSum.toAddMonoid_of,

Goal state after:
case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : { i // n i ≠ 0 }
x : ZMod (p ↑i ^ n ↑i)
⊢ (if h : n ↑i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨↑i, h⟩) x =
    (DirectSum.of (fun i ↦ ZMod (p ↑i ^ n ↑i)) i) x
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : ∃ C, ∀ (x : E), ‖g x‖ ≤ C
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ ∃ f',
    (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 ((fourierMultiplierCLM F g) f)) = Lp.toTemperedDistribution f'

Tactic:
obtain ⟨C, hC⟩ := hg₂

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
⊢ ∃ f',
    (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 ((fourierMultiplierCLM F g) f)) = Lp.toTemperedDistribution f'
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
⊢ p.Prime → p ≠ 1

Tactic:
intro pp contra

Goal state after:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ False
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x ↦ |x| ^ (-b)

Tactic:
refine (isBigO_of_le _ fun x => ?_).trans h2

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x : ℝ
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤
    ‖((fun x ↦
            ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
          Neg.neg)
        x‖
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) ⟨y, hy⟩‖ =
    ‖(ContinuousMap.restrict (Icc (x - r) (x + r)) f) ⟨y + x, ?refine_2⟩‖

Tactic:
simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case left
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

Tactic:
use i
    simp (discharger := norm_cast) [field]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mpr
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k

Tactic:
· rintro ⟨i, -, hi, rfl⟩; exact h.pow_of_coprime i hi

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_pow_eq_one hξ.pow_eq_one

Goal state after:
case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mpr
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
⊢ (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k

Tactic:
· rintro ⟨i, -, hi, rfl⟩; exact h.pow_of_coprime i hi

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : (cyclotomic n R).IsRoot ζ
⊢ (cyclotomic n R).roots.Nodup

Tactic:
isRoot_cyclotomic_iff

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (cyclotomic n R).roots.Nodup
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ (cyclotomic n R).IsRoot μ

Tactic:
isRoot_cyclotomic_iff

Goal state after:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ IsPrimitiveRoot μ n
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 : (∑ 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

Tactic:
rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]

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
⊢ X ^ (p ^ (n_n + 1) * p) = X ^ p ^ (n_n + 1 + 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
⊢ 0 < eval (-1) (cyclotomic n R)

Tactic:
have := NeZero.of_gt hn
  rw [← map_cyclotomic_int, ← Int.cast_one, ← Int.cast_neg, eval_intCast_map, Int.coe_castRingHom,
    Int.cast_pos]
  suffices 0 < eval (↑(-1 : ℤ)) (cyclotomic n ℝ) by
    rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this
    simpa only [Int.cast_pos] using this
  simp only [Int.cast_one, Int.cast_neg]
  have h0 := cyclotomic_coeff_zero ℝ hn.le
  rw [coeff_zero_eq_eval_zero] at h0
  by_contra! hx
  have := intermediate_value_univ (-1) 0 (cyclotomic n ℝ).continuous
  obtain ⟨y, hy : IsRoot _ y⟩ := this (show (0 : ℝ) ∈ Set.Icc _ _ by simpa [h0] using hx)
  rw [@isRoot_cyclotomic_iff] at hy
  rw [hy.eq_orderOf] at hn
  exact hn.not_ge LinearOrderedRing.orderOf_le_two

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁶ : NeZero n
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑n
⊢ (cyclotomic n B).IsRoot (zeta n A B)

Tactic:
isRoot_cyclotomic_iff

Goal state after:
n : ℕ
inst✝⁶ : NeZero n
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑n
⊢ IsPrimitiveRoot (zeta n A B) n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inl
m 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 m R).IsRoot μ ↔ IsPrimitiveRoot μ m

Tactic:
isRoot_cyclotomic_iff

Goal state after:
case inl
m p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ IsPrimitiveRoot μ m ↔ IsPrimitiveRoot μ m
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 m R).IsRoot μ
⊢ IsPrimitiveRoot μ m

Tactic:
isRoot_cyclotomic_iff

Goal state after:
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 : IsPrimitiveRoot μ m
⊢ IsPrimitiveRoot μ m
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
y : C
b₁ : B
h₁ : f b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
⊢ f (b₁ ^ n) = 1

Tactic:
hn.2.2,

Goal state after:
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
y : C
b₁ : B
h₁ : f b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
⊢ f 1 = 1
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
isRoot_cyclotomic_iff

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this✝ : Subsingleton (Subalgebra A B)
hS : S ⊆ {0, 1}
s : ℕ
hs : s ∈ S
hs' : s ≠ 0
this : s = 1
⊢ ∃ r, IsPrimitiveRoot r s

Tactic:
exact ⟨0, this ▸ IsPrimitiveRoot.of_subsingleton 0⟩

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:
mem_rootSet_of_ne aux

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,
    (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0
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:
mem_rootSet_of_ne aux

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)
⊢ (aeval 0) (X ^ (n✝ + 1) ^ n - X) = 0
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:
mem_rootSet_of_ne aux

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)
⊢ (aeval 1) (X ^ (n✝ + 1) ^ n - X) = 0
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:
mem_rootSet_of_ne aux

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) →
        (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
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:
mem_rootSet_of_ne aux

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
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:
mem_rootSet_of_ne aux

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) →
        (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
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 0 ≤ eval q (cyclotomic 0 ℝ)

Tactic:
by simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]

Goal state after: