mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case pos
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
this : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ + ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - 0‖ < ε

Tactic:
]

Goal state after:
case pos
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
this : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ + ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - 0‖ < ε
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

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

Tactic:
]

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

Goal state before:
pp: case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1

Tactic:
]

Goal state after:
case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ.addHaarScalarFactor volume • volume) (cocompact (StrongDual ℝ V)) (𝓝 0)

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ.addHaarScalarFactor volume • volume) (cocompact (StrongDual ℝ V)) (𝓝 0)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R = cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
]

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

Goal state before:
pp: case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R).degree ≠ ⊥

Tactic:
]

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R).degree ≠ ⊥
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1)
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 S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
⊢ orderOf μ' = orderOf hμ.toRootsOfUnity

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ μ.addHaarScalarFactor volume • ∫ (v : V), 𝐞 (-w v) • f v ∂volume) (cocompact (StrongDual ℝ V))
    (𝓝 (μ.addHaarScalarFactor volume • 0))

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ μ.addHaarScalarFactor volume • ∫ (v : V), 𝐞 (-w v) • f v ∂volume) (cocompact (StrongDual ℝ V))
    (𝓝 (μ.addHaarScalarFactor volume • 0))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ (X ^ m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R =
    (X ^ m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R

Tactic:
]

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

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots ↔ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots

pp: n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0

Tactic:
]

Goal state after:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K
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 S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ m, ↑1 ↑↑μ' = ↑↑μ' ^ m
h : μ' ^ 1 = μ' ^ h1.choose
⊢ ↑h1.choose = 1

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ m, ↑1 ↑↑μ' = ↑↑μ' ^ m
h : μ' ^ 1 = μ' ^ h1.choose
⊢ ↑h1.choose = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ ζ ^ n = 1

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ ζ ^ n = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ ζ ^ n = 1

Tactic:
convert! eq_add_of_sub_eq' this

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ 1 = 1 + eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ (∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ) ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = d * i
⊢ cyclotomic i K = cyclotomic' i K

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = d * i
⊢ cyclotomic i K = cyclotomic' i K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : μ ∈ primitiveRoots n R
⊢ μ ∈ primitiveRoots n R

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : μ ∈ primitiveRoots n R
⊢ μ ∈ primitiveRoots n R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K
⊢ (X ^ k - 1) /ₘ ∏ x ∈ k.properDivisors, cyclotomic' x K = (X ^ k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic' i K

Tactic:
]

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

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
⊢ ∃ i ∈ n.divisors, (cyclotomic i K).IsRoot μ

Tactic:
]

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
⊢ ∃ i ∈ n.divisors, (cyclotomic i K).IsRoot μ
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case e_f
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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : StrongDual ℝ V
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-w v) • f v

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ m, ↑(x * y) ↑↑μ' = ↑↑μ' ^ m
hx' : ∃ m, ↑x ↑↑μ' = ↑↑μ' ^ m
hy' : ∃ m, ↑y ↑↑μ' = ↑↑μ' ^ m
hxy : x ↑↑μ' ^ hy'.choose = ↑↑μ' ^ hxy'.choose
⊢ ↑hxy'.choose = ↑hx'.choose * ↑hy'.choose

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ m, ↑(x * y) ↑↑μ' = ↑↑μ' ^ m
hx' : ∃ m, ↑x ↑↑μ' = ↑↑μ' ^ m
hy' : ∃ m, ↑y ↑↑μ' = ↑↑μ' ^ m
hxy : x ↑↑μ' ^ hy'.choose = ↑↑μ' ^ hxy'.choose
⊢ ↑hxy'.choose = ↑hx'.choose * ↑hy'.choose
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R = cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R

Tactic:
]

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

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : ∃ i ∈ (orderOf μ).divisors, (cyclotomic i K).IsRoot μ
⊢ False

Tactic:
]

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : ∃ i ∈ (orderOf μ).divisors, (cyclotomic i K).IsRoot μ
⊢ False
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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
this : (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v) = (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A
⊢ Tendsto ((fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A) (cocompact (StrongDual ℝ V)) (𝓝 0)

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
this : (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v) = (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A
⊢ Tendsto ((fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A) (cocompact (StrongDual ℝ V)) (𝓝 0)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
⊢ False

Tactic:
]

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
⊢ False
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 S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ m, ↑(x * y) ↑↑μ' = ↑↑μ' ^ m
hx' : ∃ m, ↑x ↑↑μ' = ↑↑μ' ^ m
hy' : ∃ m, ↑y ↑↑μ' = ↑↑μ' ^ m
hxy : ↑↑μ' ^ (hx'.choose * hy'.choose) = ↑↑μ' ^ hxy'.choose
⊢ ↑hxy'.choose = ↑hx'.choose * ↑hy'.choose

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ m, ↑(x * y) ↑↑μ' = ↑↑μ' ^ m
hx' : ∃ m, ↑x ↑↑μ' = ↑↑μ' ^ m
hy' : ∃ m, ↑y ↑↑μ' = ↑↑μ' ^ m
hxy : ↑↑μ' ^ (hx'.choose * hy'.choose) = ↑↑μ' ^ hxy'.choose
⊢ ↑hxy'.choose = ↑hx'.choose * ↑hy'.choose
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
⊢ False

Tactic:
]

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P = P

pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic i R).degree

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False

Tactic:
]

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
⊢ μ ^ (↑⋯.choose).val = f μ

Tactic:
]

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
⊢ μ ^ (↑⋯.choose).val = f μ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R).degree ≠ ⊥

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R).degree ≠ ⊥
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
⊢ ↑↑(hμ.toRootsOfUnity ^ (↑h.choose).val) = ↑↑(hμ.toRootsOfUnity ^ h.choose)

Tactic:
]

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
⊢ ↑↑(hμ.toRootsOfUnity ^ (↑h.choose).val) = ↑↑(hμ.toRootsOfUnity ^ h.choose)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
⊢ False

Tactic:
]

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
⊢ False