mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ (∂_{b i} (∂_{b i} f)) x = (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f) x

Tactic:
simp_rw [lineDeriv_eq_fourierMultiplierCLM, map_smul, smul_smul]

Goal state after:
case e_f
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ ((2 * ↑π * Complex.I * (2 * ↑π * Complex.I)) •
        (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) f))
      x =
    (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f) x
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
x : V
⊢ (𝓕⁻ f) x = 𝓕⁻ (⇑f) x

Tactic:
exact (fourierInv_eq_fourier_neg f x).symm

Goal state after:
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t = mFourierCoeff (↑↑f) i

Tactic:
apply integral_congr_ae
    filter_upwards [coeFn_mFourierLp 2 i] with _ ht
    rw [ht, ← mFourier_neg, smul_eq_mul]

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
ψ₁ ψ₂ : AddChar G R
inst✝ : Fintype G
⊢ ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂

Tactic:
by
  rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_right_iff]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case pos
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ (directSumNeZeroMulHom p n) (0 x) = (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

pp: case neg
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : ¬n i = 0
⊢ (directSumNeZeroMulHom p n) ((DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

Tactic:
· simp [(ZMod.subsingleton_iff.2 <| by rw [h, pow_zero]).elim x 0]

Goal state after:
case neg
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : ¬n i = 0
⊢ (directSumNeZeroMulHom p n) ((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.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
i : ι
hi : n i ≠ 0
⊢ 1 < (fun i ↦ p ↑i ^ n ↑i) ⟨i, hi⟩

Tactic:
exact one_lt_pow₀ (hp _).one_lt hi

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ∀ ⦃a₁ a₂ : ZMod n⦄, zmod n a₁ = zmod n a₂ → a₁ = a₂

Tactic:
ZMod.intCast_surjective.forall

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ∀ (x x_1 : ℤ), zmod n ↑x = zmod n ↑x_1 → ↑x = ↑x_1
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)
hf : MemSobolev s 2 f
m x : E
⊢ 1 + ‖x‖ ^ 2 = ((1 + ‖x‖ ^ 2) ^ (1 / 2)) ^ 2

Tactic:
by
        rw [← Real.rpow_mul (by positivity)]; simp

Goal state after:
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_2
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), f (x + ↑n) = F ↑x

Tactic:
simpa only [F, coe_mk, ← QuotientAddGroup.mk_zero, Periodic.lift_coe, zsmul_one, comp_apply,
      coe_addRight, zero_add]
       using (hasSum_apply (summable_of_locally_summable_norm h_norm).hasSum x).tsum_eq

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

Goal state before:
pp: case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∀ (l : ℕ) (x : ℤ), ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑x * (2 * ↑π * I) → n ∣ l

Tactic:
have hn0 : (n : ℂ) ≠ 0 := mod_cast h0

Goal state after:
case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑x * (2 * ↑π * I) → n ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : 0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
lift i to ℕ using h0
    exact_mod_cast h.pow_of_coprime i hi

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
i : ℤ
hi : ↑k ∣ i
⊢ { toFun := fun i ↦ Additive.ofMul ⟨ζ ^ i, ⋯⟩, map_zero' := ⋯ } i = 0

Tactic:
obtain ⟨i, rfl⟩ := hi

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
i : ℤ
⊢ { toFun := fun i ↦ Additive.ofMul ⟨ζ ^ i, ⋯⟩, map_zero' := ⋯ } (↑k * i) = 0
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
h : IsPrimitiveRoot μ 0
hdiv : ¬p ∣ 0
⊢ minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)

Tactic:
simp_all

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

Goal state before:
pp: case refine_1
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑k
i : ℤ := n % ↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ i₀ < k

Tactic:
zify; rw [hi₀]; exact Int.emod_lt_of_pos _ hk0

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
have h0d : 0 < d := Nat.pos_of_dvd_of_pos hdvd (by positivity)

Goal state after:
R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
n : ℕ
hn : 0 < n
⊢ ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
    (algebraMap R[X] (RatFunc R)) (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
map_prod

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
n : ℕ
hn : 0 < n
⊢ ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
    ∏ x ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic x R)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝¹ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h✝ : a * b ≡ 1 [MOD n]
h : n ≤ 0
val✝ : R
property✝ : val✝ ∈ primitiveRoots n R
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))

Tactic:
have := Fact.mk hprime

Goal state after:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
ha₀ : a = 0
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto (fun w ↦ ∫ (v : ℝ), 𝐞 (-(v * w)) • f v) (cocompact ℝ) (𝓝 0)

Tactic:
simp_rw [mul_comm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto (fun w ↦ ∫ (v : ℝ), 𝐞 (-(w * v)) • f v) (cocompact ℝ) (𝓝 0)
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case pos
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
simp_all

Goal state after:
Module: Mathlib.FieldTheory.Galois.Abelian

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(L/K)
⊢ x * y = y * x

Tactic:
obtain ⟨x, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M x

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
y : Gal(L/K)
x : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) x * y = y * (AlgEquiv.restrictNormalHom L) x
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
⊢ (cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt
  refine ⟨fun hμ => ?_, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩
  have hμn : μ ^ n = 1 := by
    rw [isRoot_of_unity_iff hnpos _]
    exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
  by_contra hnμ
  have ho : 0 < orderOf μ := (isOfFinOrder_iff_pow_eq_one.2 <| ⟨n, hnpos, hμn⟩).orderOf_pos
  have := pow_orderOf_eq_one μ
  rw [isRoot_of_unity_iff ho] at this
  obtain ⟨i, hio, hiμ⟩ := this
  replace hio := Nat.dvd_of_mem_divisors hio
  rw [IsPrimitiveRoot.not_iff] at hnμ
  rw [← orderOf_dvd_iff_pow_eq_one] at hμn
  have key : i < n := (Nat.le_of_dvd ho hio).trans_lt ((Nat.le_of_dvd hnpos hμn).lt_of_ne hnμ)
  have key' : i ∣ n := hio.trans hμn
  rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ
  have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
  obtain ⟨k, hk⟩ := hiμ
  obtain ⟨j, hj⟩ := hμ
  have := prod_cyclotomic_eq_X_pow_sub_one hnpos K
  rw [← Finset.prod_sdiff hni, Finset.prod_pair key.ne, hk, hj] at this
  have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree
  rw [← this, Squarefree] at hn
  specialize hn (X - C μ) ⟨(∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * k * j, by ring⟩
  simp [Polynomial.isUnit_iff_degree_eq_zero] at hn

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

Goal state before:
pp: case pos
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).coeff 0 = 0
h : ↑a = 0
hone : n = 1
⊢ False

Tactic:
simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero,
      one_ne_zero, coeff_sub] at hroot

Goal state after:
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 = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y))

Tactic:
map_prod

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.Expand

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic (p ^ 1 * m) R = cyclotomic m R ^ (p ^ 1 - p ^ (1 - 1))

Tactic:
by
    rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]

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

Goal state before:
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 : eval μ (cyclotomic m R) = 0
⊢ eval μ (cyclotomic m R ^ (p ^ k - p ^ (k - 1))) = 0

Tactic:
eval_pow,

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 : eval μ (cyclotomic m R) = 0
⊢ eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F ((X ^ Fintype.card K - X).rootSet K) = ⊤

Tactic:
by
    classical
    trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
    · simp only [rootSet, aroots, Polynomial.map_pow, map_X, Polynomial.map_sub]
    · rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]

Goal state after:
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
r : ℕ
hr : x = (-ζ) ^ r
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
refine ⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩

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
r : ℕ
hr : x = (-ζ) ^ r
⊢ x = ζ ^ (r % n) ∨ x = -ζ ^ (r % n)
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
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
by
  obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx
  refine ⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩
  rw [show ζ ^ (r % n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]
  rcases Nat.even_or_odd r with (h | h) <;> simp [neg_pow, h.neg_one_pow]

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

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

Tactic:
simp_all

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

Goal state before:
pp: case neg.refine_1.inl
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₂ : m ≠ 0
hm₁ : m ∈ S
⊢ ∃ r, IsPrimitiveRoot r m

pp: case neg.refine_1.inr
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
m : ℕ
hm₂ : m ≠ 0
inst✝ : NeZero m
hr : IsPrimitiveRoot r m
hn : ¬m = 0
⊢ ∃ r, IsPrimitiveRoot r m

Tactic:
· exact exists_isPrimitiveRoot A B hm₁ hm₂

Goal state after:
case neg.refine_1.inr
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
m : ℕ
hm₂ : m ≠ 0
inst✝ : NeZero m
hr : IsPrimitiveRoot r m
hn : ¬m = 0
⊢ ∃ r, IsPrimitiveRoot r m
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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ‖eval (↑q) (cyclotomic n ℂ)‖₊ ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
⊢ insert n S \ {0} = S \ {0}

Tactic:
simp_all

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

Goal state before:
pp: case convert_5
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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ ≤ Units.mk0 (q + 1).toNNReal ⋯

Tactic:
simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
      Units.val_le_val, ← NNReal.coe_le_coe, Units.val_mk0,
      coe_nnnorm]

Goal state after:
case convert_5
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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ a ∈ primitiveRoots n ℂ, ‖↑q - a‖ ≤ ↑(q + 1).toNNReal
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d = ↑a.val * p + ↑N * q
⊢ IsCoprime ↑a₀ ↑N₀

Tactic:
rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm,
      mul_comm _ p, mul_comm _ q] at hpq

Goal state after:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d * (p * ↑a₀ + q * ↑N₀) = ↑d
⊢ IsCoprime ↑a₀ ↑N₀
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : n.gcd ↑m = 1
⊢ IsCoprime (↑m) n

Tactic:
rwa [isCoprime_comm, Int.isCoprime_iff_gcd_eq_one]

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

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this : Finite K
⊢ Nat.card ↥(Units.map (Algebra.norm K)).ker ≤ Nat.card K'ˣ / Nat.card Kˣ

Tactic:
Nat.card_units

Goal state after:
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this : Finite K
⊢ Nat.card ↥(Units.map (Algebra.norm K)).ker ≤ (Nat.card K' - 1) / (Nat.card K - 1)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
k : K
⊢ ∃ a, (Algebra.norm K) a = k

Tactic:
by
  obtain rfl | ne := eq_or_ne k 0
  · exact ⟨0, Algebra.norm_zero ..⟩
  have ⟨x, eq⟩ := unitsMap_norm_surjective K K' (Units.mk0 k ne)
  exact ⟨x, congr_arg (·.1) eq⟩

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x, ψ (x * b) = ↑0

Tactic:
simp_rw [mul_comm]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x, ψ (b * x) = ↑0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁶ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : CyclotomicField 0 K
⊢ finrank K (CyclotomicField 0 K) = 1

Tactic:
have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) :=
        Polynomial.isSplittingField_C 1

Goal state after:
n : ℕ
inst✝⁶ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : CyclotomicField 0 K
this : IsSplittingField K K (cyclotomic 0 K)
⊢ finrank K (CyclotomicField 0 K) = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ stdAddChar ↑j = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
by simp [stdAddChar, toCircle_intCast]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑n = χ₄ ↑(n % 4)

Tactic:
rw [← ZMod.intCast_mod n 4, Nat.cast_ofNat]

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

Goal state before:
pp: n : ℕ
inst✝⁸ : NeZero n
S✝ T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSepClosed K
inst✝ : CharZero K
S : Set ℕ
⊢ IsCyclotomicExtension S K K

Tactic:
rw [IsCyclotomicExtension.eq_self_sdiff_zero]
  exact IsSepClosed.isCyclotomicExtension _ K fun _ _ h ↦ ⟨Nat.cast_ne_zero.mpr h⟩

Goal state after: