mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ }, (X - C ζ)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ }, (X - C ζ)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
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
⊢ 1 = 1

Tactic:
]

Goal state after:
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:
]

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 : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ ↦ X - C ζ) (X ^ n - C 1).roots).prod

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ ↦ X - C ζ) (X ^ n - C 1).roots).prod
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_4
q : ℚ
h : Odd q.num
⊢ q.den * 2 = { num := q.num, den := q.den * 2, den_nz := ⋯, reduced := ⋯ }.den

Tactic:
]

Goal state after:
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 : ℕ
hl : f (ζ ^ l) = f 1
⊢ orderOf ζ ∣ l

Tactic:
]

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) = f 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
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (nthRoots n 1).card = n

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (nthRoots n 1).card = n
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:
]

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 : ℕ), ζ ^ l = 1 → orderOf (f ζ) ∣ 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 : ℕ
hl : f ζ ^ l = 1
⊢ orderOf (f ζ) ∣ l

Tactic:
]

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 : f ζ ^ l = 1
⊢ orderOf (f ζ) ∣ l
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ n = n

Tactic:
]

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))

Tactic:
]

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))
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' : ℕ
hl' : ↑l' = -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' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'
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‖
⊢ 1 / 2 / ‖w‖ ≤ 1

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‖
⊢ 1 / 2 / ‖w‖ ≤ 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
]

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
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' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l' = 1 ↔ ζ ^ l' = 1

Tactic:
]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
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:
]

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: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i') k

Tactic:
]

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i') k
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K = cyclotomic' n K

pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Tactic:
]

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
h0 : ¬0 ≤ i
i' : ℕ
hi : (↑i').natAbs.gcd (↑k).natAbs = 1
hi' : ↑i' = -i
⊢ i'.Coprime k

Tactic:
]

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
h0 : ¬0 ≤ i
i' : ℕ
hi : (↑i').natAbs.gcd (↑k).natAbs = 1
hi' : ↑i' = -i
⊢ i'.Coprime k
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

Tactic:
]

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K = cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
]

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

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

Tactic:
]

Goal state after:
case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)
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 = 1
⊢ x = 1

Tactic:
]

Goal state after:
case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x = 1
⊢ x = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K).degree ≠ ⊥

Tactic:
]

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K).degree ≠ ⊥
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
ζ : ℂ
h : ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
hn : n ≠ 0
⊢ ∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n

Tactic:
]

Goal state after:
n : ℕ
ζ : ℂ
h : ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
hn : n ≠ 0
⊢ ∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst✝ : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
⊢ 1 = 1

Tactic:
]

Goal state after:
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
⊢ ¬p = 2

Tactic:
]

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: R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ 2 = 2

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ i_1,
    (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
        ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ i_1.natAbs < n

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ i_1,
    (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
        ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ i_1.natAbs < n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

Tactic:
]

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

Goal state before:
pp: case e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i + -↑n = ↑i + -↑n

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⁻¹
int_A : ∫ (v : V), ‖f v - f (v + i w)‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ ∫ (v : V) in A, ‖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⁻¹
int_A : ∫ (v : V), ‖f v - f (v + i w)‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ ∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε
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)

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

Goal state before:
pp: case left
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
⊢ ∀ (a : ZMod k),
    (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
            ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
          a =
        0 →
      a = 0

Tactic:
]

Goal state after:
case left
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
⊢ ∀ (a : ZMod k),
    (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
            ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
          a =
        0 →
      a = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: 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
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Tactic:
]

Goal state after:
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
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ cyclotomic' x 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
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * Real.pi) = Real.pi * (↑i * 2 / ↑n)

Tactic:
by ring

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

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

Tactic:
]

Goal state after:
case pos.convert_2.refine_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
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) - 2 * ↑Real.pi) +
        Complex.sin (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) * Complex.I).arg =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)

Tactic:
]

Goal state after:
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) - 2 * ↑Real.pi) +
        Complex.sin (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) * Complex.I).arg =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case left
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 : ZMod k
hi :
  ↑((((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i) =
    ↑0
⊢ i = 0

Tactic:
]

Goal state after:
case left
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 : ZMod k
hi :
  ↑((((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i) =
    ↑0
⊢ i = 0
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 - 1) * (2 * ↑Real.pi) = (↑i / ↑n - 1) * (2 * ↑Real.pi)

pp: case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0

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
⊢ ↑n ≠ 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case left
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 : ZMod k
hi :
  ↑((((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i) =
    ↑0
this : ↑k ∣ i.cast
⊢ ↑i.cast = i

Tactic:
]

Goal state after:
case left
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 : ZMod k
hi :
  ↑((((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i) =
    ↑0
this : ↑k ∣ i.cast
⊢ ↑i.cast = i
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 - 1) * (2 * ↑Real.pi) = (↑i / ↑n - 1) * (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
⊢ ↑n ≠ 0

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
⊢ ↑n ≠ 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case right
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 ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩ i =
    ⟨(fun x ↦ ζ ^ x) i, ⋯⟩

Tactic:
]

Goal state after:
case right
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 ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩ i =
    ⟨(fun x ↦ ζ ^ x) i, ⋯⟩
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ^ n = 1
⊢ ↑(ζ ^ n) = 1

Tactic:
]

Goal state after:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ^ n = 1
⊢ ↑(ζ ^ n) = 1