mathlib-initiative/mathlib-tactics huggingface dataset:
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 : E
⊢ MemSobolev s 2 ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f)

Tactic:
apply (hf.fourierMultiplierCLM_of_bounded (by fun_prop) ?_).smul

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)
hf : MemSobolev s 2 f
m : E
⊢ ∃ C, ∀ (x : E), ‖↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))‖ ≤ C
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0..1, (fourier (-m)) ↑x • ⋯.lift ↑x =
    ∫ (x : ℝ) in 0..1,
      (fourier (-m)) ({ toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ } x) *
        (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
coe_mk,

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0..1, (fourier (-m)) ↑x • ⋯.lift ↑x =
    ∫ (x : ℝ) in 0..1, (fourier (-m)) ↑x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) 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)
hf : MemSobolev s 2 f
⊢ MemSobolev s 2 (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f)

Tactic:
apply (hf.fourierMultiplierCLM_of_bounded (by fun_prop) ?_).smul

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)
hf : MemSobolev s 2 f
⊢ ∃ C, ∀ (x : E), ‖↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))‖ ≤ C
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e_f
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ (fourier (-m)) ({ toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ } x) * f x = cexp (↑(-2 * π * x * ↑m) * I) * f x

Tactic:
coe_mk,

Goal state after:
case e_f
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ (fourier (-m)).toFun ({ toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ } x) * f x =
    cexp (↑(-2 * π * x * ↑m) * I) * f x
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e_f
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ (fourier (-m)).toFun ({ toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ } x) * f x =
    cexp (↑(-2 * π * x * ↑m) * I) * f x

Tactic:
coe_mk,

Goal state after:
case e_f
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ (fourier (-m)).toFun ↑x * f x = cexp (↑(-2 * π * x * ↑m) * I) * f x
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ |μ n| ≤ 1

Tactic:
rw [abs_moebius, apply_ite (· ≤ 1)]

Goal state after:
n : ℕ
⊢ if Squarefree n then 1 ≤ 1 else 0 ≤ 1
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → ∀ (a : V), ‖a - 0‖ = b → ‖∫ (v : V), 𝐞 (-⟪v, a⟫) • f v‖ < ε

Tactic:
sub_zero

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → ∀ (a : V), ‖a‖ = b → ‖∫ (v : V), 𝐞 (-⟪v, a⟫) • f v‖ < ε
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
⊢ {v | ‖v‖ ≤ R + 1} = {y | ‖y - 0‖ ≤ R + 1}

Tactic:
sub_zero

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

Goal state before:
pp: case left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot] fun x ↦ |x| ^ (-b)

pp: case right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atTop] fun x ↦ |x| ^ (-b)

Tactic:
· refine (isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
    simp_rw [norm_norm]; exact this

Goal state after:
case right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atTop] fun x ↦ |x| ^ (-b)
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

Tactic:
simp only [forall_exists_index]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l

Tactic:
intro l hl

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l

Tactic:
intro l hl

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f ζ ^ l = 1
⊢ orderOf ζ ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot (f ζ) k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), ζ ^ l = 1 → orderOf (f ζ) ∣ l

Tactic:
intro l hl

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot (f ζ) k
hf : Injective ⇑f
l : ℕ
hl : ζ ^ l = 1
⊢ orderOf (f ζ) ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ∀ (l : ℕ), ζ⁻¹ ^ l = 1 → k ∣ l

Tactic:
intro l hl

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ k ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ ↑(x ^ n) = ↑1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
Units.val_pow_eq_pow_val,

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ ↑x ^ n = ↑1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ ¬ringChar R = 2

Tactic:
ringChar.eq_iff.mpr h

Goal state after:
R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ ¬p = 2
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 : i ∈ (Int.castAddHom (ZMod k)).ker
⊢ i ∈ { toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }.ker

Tactic:
simp only [AddMonoidHom.mem_ker, CharP.intCast_eq_zero_iff (ZMod k) k, AddMonoidHom.coe_mk,
          Int.coe_castAddHom] at hi ⊢
        obtain ⟨i, rfl⟩ := hi
        simp [zpow_mul, h.pow_eq_one, one_zpow, zpow_natCast]

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

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∃ P, map (Int.castRingHom K) P = cyclotomic' n K ∧ P.degree = (cyclotomic' n K).degree ∧ P.Monic

Tactic:
refine lifts_and_degree_eq_and_monic ?_ (cyclotomic'.monic n K)
  induction n using Nat.strong_induction_on generalizing ζ with | _ k ihk
  rcases k.eq_zero_or_pos with (rfl | hpos)
  · use 1
    simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one]
  let B : K[X] := ∏ i ∈ Nat.properDivisors k, cyclotomic' i K
  have Bmo : B.Monic := by
    apply monic_prod_of_monic
    intro i _
    exact cyclotomic'.monic i K
  have Bint : B ∈ lifts (Int.castRingHom K) := by
    refine Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_
    intro x hx
    have xsmall := (Nat.mem_properDivisors.1 hx).2
    obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
    rw [mul_comm] at hd
    exact ihk x xsmall (h.pow hpos hd)
  replace Bint := lifts_and_degree_eq_and_monic Bint Bmo
  obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint
  let Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
  have huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ (0 : K[X]).degree < B.degree := by
    constructor
    · rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
    · simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero
  replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq
  simp only [lifts, RingHom.mem_rangeS]
  use Q₁
  rw [coe_mapRingHom, map_divByMonic (Int.castRingHom K) hB₁mo, hB₁, ← huniq.1]
  simp

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j

Tactic:
rw [hc, degree_mul, degree_cyclotomic, Nat.totient_prime hp] at hP'

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : ↑(p - 1) + c.degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Goal state after:
case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (cyclotomic (p ^ (m + k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: 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 : Even n ∧ x + 1 < 0
⊢ 2 ∈ n.properDivisors.erase 1

Tactic:
Finset.mem_erase,

Goal state after:
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 : Even n ∧ x + 1 < 0
⊢ 2 ≠ 1 ∧ 2 ∈ n.properDivisors
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}
⊢ IsCyclotomicExtension S A B

Tactic:
refine ⟨fun {s} hs hs' ↦ ?_, fun x ↦ by convert! (mem_top (R := A) : x ∈ ⊤)⟩
    · have : s = 1 := (subset_pair_iff.mp hS s hs).resolve_left hs'
      exact ⟨0, this ▸ IsPrimitiveRoot.of_subsingleton 0⟩

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

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : map (algebraMap A B) (cyclotomic n A) ≠ 0 ∧ (aeval x) (cyclotomic n A) = 0
⊢ n ≠ 0 ∧ x ^ n = 1

Tactic:
isRoot_of_unity_iff (NeZero.pos n)

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : map (algebraMap A B) (cyclotomic n A) ≠ 0 ∧ (aeval x) (cyclotomic n A) = 0
⊢ n ≠ 0 ∧ ∃ i ∈ n.divisors, (cyclotomic i B).IsRoot x
Module: Mathlib.FieldTheory.Finite.GaloisField

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

Tactic:
simp only [aeval_X_pow, aeval_X, map_sub, add_pow_char_pow, sub_eq_zero]

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 ^ (n✝ + 1) ^ n = x → y ^ (n✝ + 1) ^ n = y → x ^ (n✝ + 1) ^ n + y ^ (n✝ + 1) ^ n = x + y
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
have : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
simp only [isUnit_iff_mem_nonZeroDivisors_of_finite,
    mem_nonZeroDivisors_iff_right, not_forall] at hr

Goal state after:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ∃ x, ∃ (_ : x * r = 0), ¬x = 0
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: case refine_1
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ d ≠ N

Tactic:
exact fun h ↦ by simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
⊢ ∑ a, ψ a = 0

Tactic:
have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a :=
    Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl

Goal state after:
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ a, ψ (b + a) = ∑ a, ψ a
⊢ ∑ a, ψ a = 0
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
this : IsCyclic ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), x ∈ Subgroup.zpowers g
hg' : g ^ n = 1
f : ZMod n → ↥(rootsOfUnity n M) := fun j ↦ g ^ ↑j.val
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
⊢ ∃ a, f a = x

Tactic:
refine ⟨k, ?_⟩

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
this : IsCyclic ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), x ∈ Subgroup.zpowers g
hg' : g ^ n = 1
f : ZMod n → ↥(rootsOfUnity n M) := fun j ↦ g ^ ↑j.val
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
⊢ f ↑k = x
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case refine_2.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ ↑(⋯.unit ^ n) = ↑1

Tactic:
Units.val_pow_eq_pow_val,

Goal state after:
case refine_2.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ ↑⋯.unit ^ n = ↑1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]

Goal state after:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1