mathlib-initiative/mathlib-tactics huggingface dataset:
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 →
      ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
        if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
·

Goal state after:
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 →
      ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
        if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
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⟩‖

pp: case refine_2
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
⊢ y + x ∈ Icc (x - r) (x + r)

Tactic:
·

Goal state after:
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⟩‖
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_2
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
⊢ y + x ∈ Icc (x - r) (x + r)

Tactic:
·

Goal state after:
case refine_2
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
⊢ y + x ∈ Icc (x - r) (x + r)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ False

Tactic:
exact h _ (Nat.gcd_pos_of_pos_left _ hk) h' (by simp [h1, hl])

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

Goal state before:
pp: case inr
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j

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
⊢ i = j

Tactic:
·

Goal state after:
case inr
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j
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:
·

Goal state after:
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)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1

Tactic:
·

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 → ζ = 1
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case pos
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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

Tactic:
·

Goal state after:
case pos
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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

Tactic:
·

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

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

Tactic:
·

Goal state after:
case pos
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k
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‖

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‖

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.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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) 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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
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:
·

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 left
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

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:
·

Goal state after:
case left
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)
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:
·

Goal state after:
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
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 * ↑q) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))

pp: case e'_4
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ q.den = (↑n / ↑q.den).den

Tactic:
·

Goal state after:
case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))
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 = (↑n / ↑q.den).den

Tactic:
·

Goal state after:
case e'_4
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ q.den = (↑n / ↑q.den).den
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
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_3
q : ℚ
h : Odd q.num
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * ↑(q / 2))

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

Tactic:
·

Goal state after:
case e'_3
q : ℚ
h : Odd q.num
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * ↑(q / 2))
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

Tactic:
·

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (q / 2).den
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

pp: case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
·

Goal state after:
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
·

Goal state after:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
·

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ 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

pp: case neg
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:
·

Goal state after:
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
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

pp: case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ (∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x) → ↑x ^ n = 1

Tactic:
·

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 → ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

Tactic:
·

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

Goal state before:
pp: case refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R

pp: case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1

Tactic:
·

Goal state after:
case refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1

Tactic:
·

Goal state after:
case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case pos
k : ℕ
h : k = 0
⊢ (primitiveRoots k ℂ).card = φ k

pp: case neg
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
·

Goal state after:
case pos
k : ℕ
h : k = 0
⊢ (primitiveRoots k ℂ).card = φ k
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‖

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‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

pp: case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Tactic:
·

Goal state after:
case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ (if i * 2 ≤ n then ↑i else ↑i - ↑n).natAbs < n

Tactic:
by lia

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

Goal state before:
pp: case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n

pp: case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n

Tactic:
·

Goal state after:
case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n

Tactic:
·

Goal state after:
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑↑i / ↑n * (2 * Real.pi)

pp: case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)

Tactic:
·

Goal state after:
case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑↑i / ↑n * (2 * Real.pi)
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))

pp: case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))

pp: case pos.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑↑i / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi

Tactic:
·

Goal state after:
case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))

pp: case pos.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑↑i / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi

Tactic:
·

Goal state after:
case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case pos.convert_2.refine_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ -0 ≤ ↑i / ↑n * (2 * Real.pi)

pp: case pos.convert_2.refine_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * Real.pi) ≤ Real.pi

Tactic:
·

Goal state after:
case pos.convert_2.refine_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ -0 ≤ ↑i / ↑n * (2 * Real.pi)