mathlib-initiative/mathlib-tactics huggingface dataset:
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)
x : ℝ
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖

Tactic:
]

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 : ℝ
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖
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)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ ≤ ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖

Tactic:
]

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✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ ≤ ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
x✝¹ : a > 0
x✝ : a ∈ s
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ ↑(μ x.1) * g x.2 = ↑(μ x.1) * g x.2

Tactic:
]

Goal state after:
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[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✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f.toFun x‖ = ‖f.toFun x‖

Tactic:
]

Goal state after:
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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • (f v - f (v + i w))‖ < 2 * ε

Tactic:
]

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
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • (f v - f (v + i w))‖ < 2 * ε
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → n.divisors.prod ?m.177 = g n ↔
    n ∈ s → ∏ x ∈ n.divisors, (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1) = g n

pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ℕ → R

pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisors, f x = ?m.177 x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisors, f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = f x

Tactic:
]

Goal state after:
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[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)

Tactic:
]

Goal state after:
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
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
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[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x : ℝ
⊢ ∀ (x_1 : ↑↑K),
    ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
]

Goal state after:
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 : ℝ
⊢ ∀ (x_1 : ↑↑K),
    ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → n.divisorsAntidiagonal.prod ?m.242 = f n ↔ n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ℕ × ℕ → R

pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisorsAntidiagonal, (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = ?m.242 x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ g x.2 ^ μ x.1 = g x.2 ^ μ x.1

Tactic:
]

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

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h0 : 0 < k
⊢ IsPrimitiveRoot ζ k → ζ ^ k = 1

Tactic:
]

Goal state after:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h0 : 0 < k
⊢ IsPrimitiveRoot ζ k → ζ ^ k = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∅ = ∅

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : k ≠ 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j - i = 0

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j - i = 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ j = ζ ^ j

Tactic:
]

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k

Tactic:
]

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
]

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (ζ ^ i) k
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ 0 (x + p) = 0 x

Tactic:
]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ 0 (x + p) = 0 x
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1

Tactic:
]

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 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
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v - -i w‖

Tactic:
]

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
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v - -i w‖
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

Tactic:
]

Goal state after:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), cexp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

Tactic:
field_simp at hk

Goal state after:
case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑l * ↑i = ↑n * ↑k
⊢ n ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
b : ℕ
hb : i.Coprime k
this : b = k
⊢ i.Coprime k

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
b : ℕ
hb : i.Coprime k
this : b = k
⊢ i.Coprime k
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
⊢ b = k

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
⊢ b = k
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: q : ℚ
⊢ ↑(↑q.num / ↑q.den) = ↑q.num / ↑q.den

Tactic:
]

Goal state after:
q : ℚ
⊢ ↑(↑q.num / ↑q.den) = ↑q.num / ↑q.den
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ b = k

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ b = k
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * ↑(↑(↑2 * n) / ↑q.den)) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))

Tactic:
]

Goal state after:
case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * ↑(↑(↑2 * n) / ↑q.den)) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_4
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ q.den = { num := n, den := q.den, den_nz := ⋯, reduced := ?m.148 }.den

pp: q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ n.natAbs.Coprime q.den

Tactic:
]

Goal state after:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ n.natAbs.Coprime q.den
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).natDegree = n.totient

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).natDegree = n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i ∈ primitiveRoots n R, (X - C i).natDegree = n.totient

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ primitiveRoots n R, X - C i ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i ∈ primitiveRoots n R, (X - C i).natDegree = n.totient

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ primitiveRoots n R, X - C i ≠ 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))
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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R + ‖i w‖ ≤ ‖v‖

Tactic:
]

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
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R + ‖i w‖ ≤ ‖v‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val

Tactic:
]

Goal state after:
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) j
⊢ i = j

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) j
⊢ i = j
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (↑q.num / ↑q.den / 2).den

Tactic:
]

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (↑q.num / ↑q.den / 2).den