mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p s : ℝ
hs : -1 < s
hp : 0 < p
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
have ht : (0 : ℝ) < (s + 1) / p := div_pos (by linarith) hp
  refine ((integrableOn_Ioi_comp_rpow_iff' _ hp.ne').mpr
    (GammaIntegral_convergent ht)).congr_fun (fun x hx => ?_) measurableSet_Ioi
  simp only [smul_eq_mul]
  rw [mul_comm (exp (-x ^ p)), ← mul_assoc, ← rpow_mul hx.le, ← rpow_add hx]
  field_simp
  ring_nf

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case hfm
ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (map (Function.eval i) (Measure.pi μ))

Tactic:
· rwa [(measurePreserving_eval μ i).map_eq]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -(((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0)
hn : s ≠ 0
⊢ (∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) - ↑(rexp (-X)) * ↑X ^ s =
    (∫ (x : ℝ) in 0..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1))) - ↑(rexp (-X)) * ↑X ^ s

Tactic:
congr with x

Goal state after:
case e_a.e_f
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -(((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0)
hn : s ≠ 0
x : ℝ
⊢ ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = s * (↑(rexp (-x)) * ↑x ^ (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ -π ≤ π

Tactic:
linarith [pi_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

Tactic:
exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inr
b : ℝ
hb : 0 < b
⊢ ↑(∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = ↑(√(π / b) ^ 2)

Tactic:
← integral_ofReal,

Goal state after:
case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), ↑(rexp (-b * x ^ 2))) ^ 2 = ↑(√(π / b) ^ 2)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ Tendsto (fun c ↦ ∫ (v : V), cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (∫ (v : V), f v))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm
  · filter_upwards with v
    nth_rewrite 2 [show f v = cexp (- (0 : ℝ) * ‖v‖ ^ 2) • f v by simp]
    apply (Tendsto.cexp _).smul_const
    exact tendsto_inv_atTop_zero.ofReal.neg.mul_const _
  · filter_upwards with c using
      AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1
  · filter_upwards [Ici_mem_atTop (0 : ℝ)] with c (hc : 0 ≤ c)
    filter_upwards with v
    simp only [ofReal_inv, neg_mul, norm_smul]
    norm_cast
    conv_rhs => rw [← one_mul (‖f v‖)]
    gcongr
    simp only [norm_eq_abs, abs_exp, exp_le_one_iff, Left.neg_nonpos_iff]
    positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ Gamma 1 = 1

Tactic:
Gamma_eq_integral

Goal state after:
⊢ GammaIntegral 1 = 1

⊢ 0 < re 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inr
b : ℝ
hb : 0 < b
⊢ ↑(∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2)) = ↑(√(π / b) / 2)

Tactic:
← integral_ofReal,

Goal state after:
case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-b * x ^ 2)) = ↑(√(π / b) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
this :
  (((∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(-↑T).im * I) ^ 2)) -
          ∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(↑T + ↑c * I).im * I) ^ 2)) +
        I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(↑T + ↑c * I).re + ↑y * I) ^ 2)) -
      I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(-↑T).re + ↑y * I) ^ 2) =
    0
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0

Tactic:
simpa only [neg_im, ofReal_im, neg_zero, ofReal_zero, zero_mul, add_zero, neg_re,
      ofReal_re, add_re, mul_re, I_re, mul_zero, I_im, tsub_zero, add_im, mul_im,
      mul_one, zero_add, smul_eq_mul, ofReal_neg] using this

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (I ^ 2 * t ^ 2 / (4 * b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
I_sq,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (-1 * t ^ 2 / (4 * b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (-b * ∑ i, ↑(v i) ^ 2 + ∑ i, c i * ↑(v i)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))

Tactic:
by
  simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℂ E
V : Type u_3
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : FiniteDimensional ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L⋆[ℂ] F →L[ℂ] G
⊢ ∫ (ξ : V), (M ((𝓕 f) ξ)) ((𝓕 g) ξ) = ∫ (x : V), (M (f x)) (g x)

Tactic:
simpa using integral_sesq_fourier_eq f (𝓕 g) M

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → InnerProductSpace 𝕜 (E i)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ ⟪c • f, g⟫_[𝕜, w] = star c • ⟪f, g⟫_[𝕜, w]

Tactic:
by
  simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : Group.FG G
n : ℕ
ι : Type
inst : Fintype ι
x : ι → ℕ
p : ∀ (i : ι), Nat.Prime (x i)
e : ι → ℕ
equiv : Nonempty (Additive G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (x i ^ e i))
⊢ ∃ ι j x x p,
    ∃ (_ : ∀ (i : ι), Nat.Prime (p i)),
      ∃ e, Nonempty (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))

Tactic:
exact ⟨ι, Fin n, inst, inferInstance, x, p, e, ⟨MulEquiv.toAdditive.symm <| equiv.some.trans <|
    ((Finsupp.addEquivFunOnFinite.trans <| ((AddEquiv.piAdditive _).trans <|
        (AddEquiv.additiveMultiplicative ℤ).arrowCongr (Equiv.refl _)).symm).prodCongr
          (DirectSum.addEquivProd _ )).trans <| (AddEquiv.prodAdditive _ _).symm⟩⟩

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, p.Prime ∧ p ∣ n

Tactic:
exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)

Goal state after:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ⟨p, ⋯⟩ ∣ n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: k m n : ℕ+
h : m.Coprime n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n

Tactic:
by
  rw [← coprime_coe] at h; apply eq
  simp only [gcd_coe, mul_coe]; apply Nat.Coprime.gcd_mul k h

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

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

Tactic:
simp_all only [pow_one, Nat.coprime_zero_right]

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R + ‖i w‖ ≤ R + 1

Tactic:
add_le_add_iff_left,

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‖
⊢ ‖i w‖ ≤ 1
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
int_A : ∫ (v : V), ‖f v - f (v + i w)‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ ∫ (a : V), ‖f a - f (a + (1 / (2 * ‖w‖ ^ 2)) • w)‖ < 2 * ε

Tactic:
rw [int_A]

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: n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n

Tactic:
rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
  obtain ⟨i, h, hin, rfl⟩ := h
  rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
  refine ⟨if i * 2 ≤ n then i else i - n, ?_, ?isCoprime, by lia⟩
  case isCoprime =>
    replace hin := Nat.isCoprime_iff_coprime.mpr hin
    split_ifs
    · exact hin
    · convert! hin.add_mul_left_left (-1) using 1
      rw [mul_neg_one, sub_eq_add_neg]
  split_ifs with h₂
  · convert! Complex.arg_cos_add_sin_mul_I _
    · push_cast; rfl
    · push_cast; rfl
    simp only [Int.cast_natCast, Set.mem_Ioc]
    refine ⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩
    · rw [neg_zero]
      positivity
    refine Eq.trans_le (b := Real.pi * (i * 2 / n)) (by ring) ?_
    rw [← mul_one n] at h₂
    exact mul_le_of_le_one_right Real.pi_pos.le
      ((div_le_iff₀' <| mod_cast pos_of_gt h).mpr <| mod_cast h₂)
  rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]
  convert! Complex.arg_cos_add_sin_mul_I _
  · push_cast
    rw [← sub_one_mul, sub_div, div_self]
    exact mod_cast hn
  · push_cast
    rw [← sub_one_mul, sub_div, div_self]
    exact mod_cast hn
  simp only [Int.cast_sub, Int.cast_natCast, Set.mem_Ioc]
  field_simp
  constructor
  · push Not at h₂
    rify at h₂
    linear_combination h₂
  · rify at h
    linear_combination 2 * h + (n : ℝ) * one_pos (α := ℝ)

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

Goal state before:
pp: case h.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

Tactic:
exact fun hk => h.2.not_ge <| Nat.divisor_le hk

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

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

Tactic:
h.card_nthRoots_one

Goal state after:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ n = n
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)‖
⊢ ↑B < ↑B + ↑B

Tactic:
exact lt_add_of_pos_left _ hB_pos

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
⊢ (cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
⊢ (cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n
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 = 𝐞 (-⟪v, A w⟫) • f v

Tactic:
rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]

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

Goal state before:
pp: G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
⊢ IsPrimitiveRoot (φ g) (Nat.card G)

Tactic:
rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]

Goal state after:
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
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
⊢ IsIntegral R ((B.basis.repr (B.gen ^ n)) i)

Tactic:
let Q := X ^ n %ₘ minpoly R B.gen

Goal state after:
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
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ IsIntegral R ((B.basis.repr (B.gen ^ n)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

Tactic:
rw [mem_primitiveRoots hn] at hζ'

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q - 1 ≤ ‖↑q - ζ'‖
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 1 n
⊢ False

Tactic:
linarith [hζ.unique IsPrimitiveRoot.one]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
⊢ ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)

Tactic:
cyclotomic',

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
⊢ ∏ σ, (1 - σ ζ) = eval 1 (∏ μ ∈ primitiveRoots n E, (X - C μ))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval 1 (cyclotomic' n E) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
cyclotomic',

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval 1 (∏ μ ∈ primitiveRoots n E, (X - C μ)) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ ‖↑q - ζ'‖ ≤ q + 1

Tactic:
rw [mem_primitiveRoots hn] at hζ'

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖↑q - ζ'‖ ≤ q + 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝¹ : Algebra B C := (↑f).toAlgebra
this✝ : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C

Tactic:
exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}.Finite

Tactic:
simp only [mem_singleton_iff, exists_eq_left]
    have : {b : B | n ≠ 0 ∧ b ^ n = 1} = (nthRoots n (1 : B)).toFinset :=
      Set.ext fun x ↦ ⟨fun h ↦ by simpa [n.pos_of_neZero] using h.2,
        fun h ↦ by simpa [n.pos_of_neZero, NeZero.ne n] using h⟩
    rw [this]
    exact (nthRoots n 1).toFinset.finite_toSet

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ ∃ i ∈ n.divisors, (cyclotomic i B).IsRoot x

Tactic:
refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ (cyclotomic n B).IsRoot x