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

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

Tactic:
push_cast

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

Goal state before:
pp: case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ cardFactors n = 0 ∨ (-1) ^ cardFactors n = 1 ∨ (-1) ^ cardFactors n = -1

Tactic:
right
    exact neg_one_pow_eq_or ..

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0

Tactic:
simp only [moebius_eq_zero_of_not_squarefree h, abs_zero]

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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2) • ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v - 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)

Tactic:
rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ←
    two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul]

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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2 * 2) • ∫ (a : V), 𝐞 (-⟪a, w⟫) • f a

case hf
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f v) volume

case hg
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case hnc
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ ¬k = 1

Tactic:
rintro rfl

Goal state after:
case hnc
p : ℕ
hp : Nat.Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Nat.Prime (p ^ 1)
⊢ False
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 y : ℝ
hy : y ∈ ↑K
⊢ ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) ⟨y, hy⟩‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)

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⟩‖

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

Tactic:
cocompact_eq_atBot_atTop,

Goal state after:
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 ⊔ atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot ⊔ atTop] fun x ↦ |x| ^ (-b)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

Tactic:
rintro rfl

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
⊢ IsPrimitiveRoot 1 1
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:
push_cast

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.Complex

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

Tactic:
push_cast

Goal state after:
case e'_3
q : ℚ
h : Odd q.num
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * (↑q / 2))
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
hd : (↑n.divisors).PairwiseDisjoint fun k ↦ primitiveRoots k K
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1

Tactic:
simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
    IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots]

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

Tactic:
lift i to ℕ using h0

Goal state after:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : (↑i).gcd ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ ↑i) k
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
⊢ IsPrimitiveRoot (-1) 2

Tactic:
convert! IsPrimitiveRoot.orderOf (-1 : R)
  rw [orderOf_neg_one, if_neg <| by rwa [ringChar.eq_iff.mpr h]]

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

Tactic:
push_cast

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))

Tactic:
push_cast

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 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) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))

Tactic:
push_cast

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) - 2 * ↑Real.pi = (↑i - ↑n) / ↑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) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))

Tactic:
push_cast

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) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ P = cyclotomic n ℤ

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective

Goal state after:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i ℤ = X ^ n - 1

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective

Goal state after:
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (X ^ n - 1)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a α : R
hα : α ^ n = a
⊢ (nthRoots n a).card = n

Tactic:
rw [nthRoots_eq hζ hα, Multiset.card_map, Multiset.card_range]

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⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B
bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * volume.real A
this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ ε * volume.real A < ε * (2 * ↑B)

Tactic:
mul_lt_mul_iff_right₀ hε

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⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B
bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * volume.real A
this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ volume.real A < 2 * ↑B
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) = minpoly ℤ (μ ^ (p * a))

Tactic:
rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.Coprime.coprime_mul_left hcop)) hdiv]

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.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X - 1) ^ p - (-1) ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1

Tactic:
(hpri.odd_of_ne_two hp).neg_pow,

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X - 1) ^ p - -1 ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R ((B.basis.repr (B.gen ^ (↑I.1 + ↑I.2))) i)

Tactic:
exact repr_gen_pow_isIntegral hB hmin _ _

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

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this✝ : NeZero n
this : 0 < eval (↑(-1)) (cyclotomic n ℝ)
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)

Tactic:
rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this

Goal state after:
n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this✝ : NeZero n
this : 0 < (fun x ↦ ↑x) (eval (↑(-1)) (cyclotomic n ℤ))
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inl.hb.inl.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ i ≠ 0

Tactic:
rintro rfl

Goal state after:
case h.inl.hb.inl.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
hk : Odd n
hi : 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inl.hb.inl.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ i ≠ 2

Tactic:
rintro rfl

Goal state after:
case h.inl.hb.inl.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
hk : Odd n
hi : 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inl.hb.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ i ≠ 0

Tactic:
rintro rfl

Goal state after:
case h.inl.hb.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
hx : 0 < x + 1
hi : 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
hk : 0 ≠ 2
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case hb.ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
i : ℕ
hi : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ i ≠ 0

Tactic:
rintro rfl

Goal state after:
case hb.ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : 0 ≠ 2 ∧ 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
⊢ ¬ζ = 1

Tactic:
rintro rfl

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
hζ : IsPrimitiveRoot 1 n
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤

Tactic:
rw [← adjoin_adjoin_coe_preimage, preimage_ofPred_eq]

Goal state after:
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = adjoin A {a | ∃ a_1 ∈ S, a_1 ≠ 0 ∧ ↑a ^ a_1 = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg.refine_1.inr
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
m : ℕ
hm₂ : m ≠ 0
inst✝ : NeZero m
hr : IsPrimitiveRoot r m
hn : ¬m = 0
⊢ ∃ r, IsPrimitiveRoot r m

Tactic:
· use r

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
h : ζ.re ≤ 0 ∧ ζ.im = 0
⊢ ζ ≠ 0

Tactic:
rintro rfl

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
hζ : IsPrimitiveRoot 0 n
h : Complex.re 0 ≤ 0 ∧ Complex.im 0 = 0
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ i.fieldRange = IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
AlgHom.fieldRange_eq_map,

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ IntermediateField.map i ⊤ = IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
⊢ ψ a = 1 ↔ a = 0

Tactic:
refine ⟨fun h => not_imp_comm.mp (@hψ a) ?_, fun ha => by rw [ha, map_zero_eq_one]⟩

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : ψ a = 1
⊢ ¬ψ.mulShift a ≠ 1
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ 2 ^ (2 * 2 ^ k₁) = ↑2 ^ (2 * 2 ^ k₁)

Tactic:
← _root_.pow_succ'

Goal state after:
case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ 2 ^ 2 ^ (k₁ + 1) = ↑2 ^ 2 ^ (k₁ + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (↑(2 * π / 1 * (↑j / ↑N)) * I) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
push_cast

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (2 * ↑π / 1 * (↑j / ↑N) * I) = cexp (2 * ↑π * I * ↑j / ↑N)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ cexp (2 * ↑π * I * ↑j.val / ↑N) = cexp (↑(2 * π * (↑j.val / ↑N)) * I)

Tactic:
push_cast

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ cexp (2 * ↑π * I * ↑j.val / ↑N) = cexp (2 * ↑π * (↑j.val / ↑N) * I)
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
⊢ ∃ χ, orderOf χ = n

Tactic:
let ζ' : Rˣ := (hζ.isUnit hn₀.ne').unit

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
⊢ ∃ χ, orderOf χ = n