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

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

Tactic:
rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]
    refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi
    #adaptation_note /-- 2026-05-17(kmill) added `dsimp only` because a slightly different
    instantiation order leads to a term with a beta redex.
    https://github.com/leanprover/lean4/pull/13762
    This will be removed once app elaboration itself does beta reduction. -/
    dsimp only
    rw [← mul_assoc, mul_rpow, mul_rpow, ← rpow_mul (z := p), neg_mul, neg_mul, inv_mul_cancel₀,
      rpow_neg_one, mul_inv_cancel_left₀]
    all_goals linarith [mem_Ioi.mp hx]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
⊢ HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x

Tactic:
simpa using! (hasDerivAt_neg x).exp

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

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

Tactic:
← rpow_two

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in ↑polarCoord.symm '' polarCoord.target, f p

Tactic:
rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]

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

Goal state before:
pp: case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ Gamma (↑(n + 1) + 1) = ↑(n + 1)!

Tactic:
Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n

Goal state after:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ ↑n.succ * Gamma ↑n.succ = ↑(n + 1)!
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
⊢ Complex.Gamma ↑s = ↑(Gamma s)

Tactic:
by
  rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]

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

Goal state before:
pp: case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ ∀ (m : ℕ), s + 1 ≠ -↑m

Tactic:
intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
⊢ (besselPotential E F (-2)) (Δ f) = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f

Tactic:
rw [laplacian_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
⊢ -(2 * π) ^ 2 • (fourierMultiplierCLM F ((fun x ↦ ↑(‖x‖ ^ 2)) * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-2 / 2)))) f =
    -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case refine_2
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ ∀ (x y : C(UnitAddTorus d, ℂ)),
    x ∈ Submonoid.closure (range mFourier) →
      y ∈ Submonoid.closure (range mFourier) → x ∈ range mFourier → y ∈ range mFourier → x * y ∈ range mFourier

Tactic:
· rintro _ _ _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
    refine ⟨m + n, ?_⟩
    ext z
    simp only [mFourier, Pi.add_apply, fourier_apply, fourier_add', Finset.prod_mul_distrib,
      ContinuousMap.coe_mk, ContinuousMap.mul_apply]

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)
w : ι → ℝ
g : (i : ι) → E i
⊢ ⟪0, g⟫_[𝕜, w] = 0

Tactic:
by simp [wInner]

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)
w : ι → ℝ
f : (i : ι) → E i
⊢ ⟪f, 0⟫_[𝕜, w] = 0

Tactic:
by simp [wInner]

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)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w]

Tactic:
sub_eq_add_neg,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ ⟪f₁ + -f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + -⟪f₂, g⟫_[𝕜, w]
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)
w : ι → ℝ
f g₁ g₂ : (i : ι) → E i
⊢ ⟪f, g₁ - g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] - ⟪f, g₂⟫_[𝕜, w]

Tactic:
sub_eq_add_neg,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f g₁ g₂ : (i : ι) → E i
⊢ ⟪f, g₁ + -g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] + -⟪f, g₂⟫_[𝕜, w]
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)
f g : (i : ι) → E i
⊢ ⟪f, g⟫_[𝕜] = ∑ i, ⟪f i, g i⟫_𝕜

Tactic:
by simp [wInner]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
⊢ (map (powMonoidHom n) B).IsFiniteRelIndex B

Tactic:
by
  rw [isFiniteRelIndex_iff_finiteIndex]
  have : (map (powMonoidHom (α := A) n) B).subgroupOf B = (powMonoidHom (α := B) n).range := by
    ext1
    simp [mem_subgroupOf, Subtype.ext_iff]
  rw [this]
  have := (Group.fg_iff_subgroup_fg B).mpr hB
  exact finiteIndex_range_powMonoidHom_of_fg B hn

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

Goal state before:
pp: 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
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight ↑n)) x

Tactic:
simp only [mul_comp] at eadd ⊢
      simp_rw [eadd]

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) • ((∫ (a : V), 𝐞 (-⟪a, w⟫) • f a) - -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v)

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

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

Tactic:
sub_eq_add_neg,

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) • ((∫ (a : V), 𝐞 (-⟪a, w⟫) • f a) + - -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v)

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: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p)

Tactic:
apply prod_congr rfl; intro p hp
    rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
        (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]
    ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p)

pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
· apply prod_congr rfl; intro p hp
    rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
        (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]
    ring

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (μ • g') n = f' n ↔ n > 0 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
cases n with
    | zero => simp
    | succ n =>
      simp only [forall_prop_of_true, succ_pos', smul_apply, f', g', coe_mk, succ_ne_zero,
        ite_false]
      rw [sum_congr rfl fun x hx => ?_]
      rw [if_neg (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)).ne']

Goal state after:
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[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
⊢ ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)

Tactic:
convert! hf.comp_tendsto tendsto_neg_atTop_atBot using 1

Goal state after:
case e'_8
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
⊢ (fun x ↦ |x| ^ (-b)) = (fun x ↦ |x| ^ (-b)) ∘ Neg.neg
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑x * (2 * ↑π * I) → n ∣ l

Tactic:
rintro l k hk

Goal state after:
case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑k * (2 * ↑π * I)
⊢ n ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
n : ℕ
inst✝ : NeZero n
f : F
hf : Function.Injective ⇑f
hζ : (primitiveRoots n R).Nonempty
η : ↥(rootsOfUnity n S)
⊢ f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η) = ↑↑η

Tactic:
obtain ⟨ε, rfl⟩ := (rootsOfUnityEquivOfPrimitiveRoots hf hζ).surjective η

Goal state after:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
n : ℕ
inst✝ : NeZero n
f : F
hf : Function.Injective ⇑f
hζ : (primitiveRoots n R).Nonempty
ε : ↥(rootsOfUnity n R)
⊢ f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm ((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)) =
    ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)
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
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) Q ^ p

Tactic:
hfrob

Goal state after:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i ∈ n.divisors, cyclotomic i ℤ

Tactic:
exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')

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:
by
  rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]

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

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

Tactic:
by_cases hα' : α = 0

Goal state after:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
⊢ (nthRoots n a).Nodup

case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ (nthRoots n a).Nodup
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬cyclotomic n R = 0

pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0

Tactic:
· simp [cyclotomic_ne_zero]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0
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
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
⊢ ‖∫ (a : V), 𝐞 (-⟪a, w⟫) • (f a - g a) ∂volume‖ ≤ ∫ (x : V), ‖f x - g x‖

Tactic:
← Pi.sub_apply

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
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
⊢ ‖∫ (a : V), 𝐞 (-⟪a, w⟫) • (f - g) a ∂volume‖ ≤ ∫ (x : V), ‖(f - g) x‖
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 R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
hr : 0 < n
⊢ b.Coprime n

Tactic:
simpa [(b.gcd_dvd_left n).trans] using h.dvd_iff (Nat.gcd_dvd_right b n)

Goal state after:
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.divisors, cyclotomic x R

Tactic:
prod_cyclotomic_eq_X_pow_sub_one (Nat.pos_of_mem_properDivisors hm)

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.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
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
by_cases hn : n = 0; · simp_all
  have : NeZero n := ⟨hn⟩
  have hpos := Nat.pos_of_ne_zero hn
  intro x hx
  obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h).1 ((mem_primitiveRoots hpos).1 hx)
  simp only [Multiset.mem_toFinset]
  convert! pow_isRoot_minpoly h hcop using 0
  rw [← mem_roots]
  exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos

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:
replace hxy : (((μ' : Sˣ) : S) ^ hx'.choose) ^ hy'.choose = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hx'.choose_spec ▸ hxy

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: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℤ = cyclotomic m ℤ
⊢ n = m

Tactic:
replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : map (Int.castRingHom ℂ) (cyclotomic n ℤ) = map (Int.castRingHom ℂ) (cyclotomic m ℤ)
⊢ n = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = map (Int.castRingHom ℂ) (cyclotomic m ℤ)
⊢ n = m

Tactic:
map_cyclotomic_int

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
⊢ n = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p) (map (Int.castRingHom ℚ) (cyclotomic n ℤ))

Tactic:
map_cyclotomic_int

Goal state after:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this✝ : NeZero n
this : (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
⊢ map (Int.castRingHom R) (cyclotomic (n * p) ℤ) = cyclotomic (n * p) R

Tactic:
map_cyclotomic_int

Goal state after:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this✝ : NeZero n
this : (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
⊢ cyclotomic (n * p) R = cyclotomic (n * p) R
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r n) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ n = 1}

Tactic:
simp [isCyclotomicExtension_iff, NeZero.ne]

Goal state after: