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

Goal state before:
pp: case hgi
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
⊢ Integrable
    (fun a ↦
      (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖)
    μ

pp: case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
⊢ (fun a ↦ ‖iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k) a‖) ≤ᵐ[μ] fun a ↦
    (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖

Tactic:
· exact (integrable_finsetSum _ I).const_mul _

Goal state after:
case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
⊢ (fun a ↦ ‖iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k) a‖) ≤ᵐ[μ] fun a ↦
    (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
hf_ae : ↑↑(f.toLp 2 μ) =ᵐ[μ] ⇑f
⊢ (fun a ↦ inner ℂ (↑↑(f.toLp 2 μ) a) (↑↑(g.toLp 2 μ) a)) =ᵐ[μ] fun a ↦ inner ℂ (f a) (g a)

Tactic:
have hg_ae := g.coeFn_toLp 2 μ

Goal state after:
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
hf_ae : ↑↑(f.toLp 2 μ) =ᵐ[μ] ⇑f
hg_ae : ↑↑(g.toLp 2 μ) =ᵐ[μ] ⇑g
⊢ (fun a ↦ inner ℂ (↑↑(f.toLp 2 μ) a) (↑↑(g.toLp 2 μ) a)) =ᵐ[μ] fun a ↦ inner ℂ (f a) (g a)
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℝ
ha : a < 0
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, RCLike.re (Complex.exp (↑a * ↑x)) = -RCLike.re (Complex.exp (↑a * ↑c)) / a

Tactic:
integral_re,

Goal state after:
a : ℝ
ha : a < 0
c : ℝ
⊢ RCLike.re (∫ (x : ℝ) in Ioi c, Complex.exp (↑a * ↑x)) = -RCLike.re (Complex.exp (↑a * ↑c)) / a

a : ℝ
ha : a < 0
c : ℝ
⊢ Integrable (fun x ↦ Complex.exp (↑a * ↑x)) (volume.restrict (Ioi c))
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((innerₗ V) a✝) x) • f₂ a✝

Tactic:
rw [hf']

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

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((-innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((-innerₗ V) a✝) x) • f₂ a✝

Tactic:
rw [hf']

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

Goal state before:
pp: case right
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
exact integrable_of_isBigO_exp_neg one_half_pos
      (continuousOn_id.neg.rexp.mul (continuousOn_id.rpow_const (by grind)))
      (Gamma_integrand_isLittleO _).isBigO

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

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ Tendsto (fun x ↦ -x - -b * x ^ p) atTop atTop

Tactic:
by
    refine Tendsto.congr' ?_ this
    refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)
    rw [mem_Ioi] at hx
    rw [rpow_sub_one hx.ne']
    field

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case right.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
exact Or.inl (le_of_lt hxy)

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

Goal state before:
pp: s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ (fun x ↦ x ^ s * rexp (-x)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)

Tactic:
simpa only [mul_comm] using Real.Gamma_integrand_isLittleO s

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
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
⊢ HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x

Tactic:
have d2 : HasDerivAt (fun y : ℝ => (y : ℂ) ^ s) (s * x ^ (s - 1)) x := by
      have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
      · simpa only [mul_one] using! t.comp_ofReal
      · exact ofReal_mem_slitPlane.2 hx.1

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
d2 : HasDerivAt (fun y ↦ ↑y ^ s) (s * ↑x ^ (s - 1)) x
⊢ HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_3
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
B : Tendsto (fun y ↦ -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ (2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * ↑0 ^ 2)

Tactic:
simp only [mul_zero, ofReal_zero, zero_pow, Ne,
    not_false_iff, Complex.exp_zero, mul_one, sub_neg_eq_add, zero_add, reduceCtorEq]

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

Goal state before:
pp: case zero
⊢ Gamma (-↑0) = 0

Tactic:
Nat.cast_zero,

Goal state after:
case zero
⊢ Gamma (-0) = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℝ → ℂ := fun x ↦ cexp (-b * ↑x ^ 2)
full_integral : (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) * 2 = (↑π / b) ^ (1 / 2)
h_eq : ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f x
⊢ (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) * 2 = (↑π / b) ^ (1 / 2)

Tactic:
by simpa using full_integral

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

Goal state before:
pp: case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -↑0 < s
⊢ 0 < s

Tactic:
Nat.cast_zero,

Goal state after:
case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -0 < s
⊢ 0 < s
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ‖x‖ ^ 2) f

Tactic:
laplacian_eq_sum b,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
⊢ ∑ i, ∂_{b i} (∂_{b i} f) = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ‖x‖ ^ 2) f
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f

Tactic:
laplacian_eq_sum b,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
⊢ ∑ i, ∂_{b i} (∂_{b i} f) = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d✝ : Type u_1
inst✝¹ : Fintype d✝
d : Type u_2
inst✝ : Fintype d
⊢ ∀ {a : C(UnitAddTorus d, ℂ)}, a ∈ (adjoin ℂ (range mFourier)).carrier → star a ∈ (adjoin ℂ (range mFourier)).carrier

Tactic:
change Algebra.adjoin ℂ (range mFourier) ≤ star (Algebra.adjoin ℂ (range mFourier))
    refine adjoin_le ?_
    rintro _ ⟨n, rfl⟩
    refine subset_adjoin ⟨-n, ?_⟩
    ext1 x
    simp only [mFourier_neg, starRingEnd_apply, ContinuousMap.star_apply]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ mFourierCoeff (↑↑f) i • mFourierLp 2 i) f

Tactic:
simpa [← coe_mFourierBasis, mFourierBasis_repr] using mFourierBasis.hasSum_repr f

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

Tactic:
by
  simp [Subsingleton.elim f 0]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
m : E
⊢ 𝓕⁻ (∂_{m} f) = -(2 * ↑π * Complex.I) • (smulLeftCLM F fun x ↦ ↑(inner ℝ x m)) (𝓕⁻ f)

Tactic:
by
  ext u
  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
  simp [SchwartzMap.lineDerivOp_fourierInv_eq, ← smulLeftCLM_ofReal ℂ this]

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

Goal state before:
pp: ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x : ⨁ (i : { i // n i ≠ 0 }), ZMod (p ↑i ^ n ↑i)
⊢ (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) x) =
    x

Tactic:
induction x using DirectSum.induction_on with

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

Goal state before:
pp: ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x : ⨁ (i : ι), ZMod (p i ^ n i)
⊢ (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    x

Tactic:
induction x using DirectSum.induction_on with

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R ↑n) A ≤ B
this✝ : A.toAddSubgroup.FG
this : (AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup).IsFiniteRelIndex A.toAddSubgroup
⊢ B.toAddSubgroup.IsFiniteRelIndex A.toAddSubgroup

Tactic:
refine isFiniteRelIndex_of_le_left (H := A.toAddSubgroup.map (nsmulAddMonoidHom n))
    A.toAddSubgroup ?_

Goal state after:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R ↑n) A ≤ B
this✝ : A.toAddSubgroup.FG
this : (AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup).IsFiniteRelIndex A.toAddSubgroup
⊢ AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup ≤ B.toAddSubgroup
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

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 : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ≤ -x✝ + -R

Tactic:
by linarith [hx.1]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 1 R = {1}

Tactic:
refine Finset.eq_singleton_iff_unique_mem.2 ⟨?_, fun x hx ↦ ?_⟩
  · simp only [IsPrimitiveRoot.one_right_iff, mem_primitiveRoots zero_lt_one]
  · rwa [mem_primitiveRoots zero_lt_one, IsPrimitiveRoot.one_right_iff] at hx

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

Tactic:
exact ⟨∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩

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

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ p.Coprime a

Tactic:
rw [hprime.1.coprime_iff_not_dvd]

Goal state after:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ ¬p ∣ a
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 - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯

Tactic:
convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _

Goal state after:
case e'_3
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i

case convert_2
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i ≤ Units.mk0 ‖↑q - ↑i‖₊ ⋯

case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i < Units.mk0 ‖↑q - ↑i‖₊ ⋯
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
by
  refine
    ⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2
      ⟨fun s hs ↦ ?_, ?_⟩⟩
  · exact H.exists_isPrimitiveRoot (subset_union_left hs)
  · rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ A B).1 H).2]
    refine adjoin_mono fun x hx => ?_
    simp only [union_singleton, mem_insert_iff, mem_ofPred_eq] at hx ⊢
    obtain ⟨m, rfl | hm, hxpow⟩ := hx
    · obtain ⟨y, ⟨hy, hy', ⟨z, rfl⟩⟩⟩ := h
      exact ⟨_, ⟨hy, hy', by simp only [pow_mul, hxpow, one_pow]⟩⟩
    · exact ⟨m, ⟨hm, hxpow⟩⟩

Goal state after:
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
inst✝ : IsCyclotomicExtension S A B
x : B
x✝ : x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ eval₂ (algebraMap A B) x (X ^ n - 1) = 0

Tactic:
simp [h2]

Goal state after:
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
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
⊢ ∃ r, IsPrimitiveRoot r n ∧ (f * g) r = (g * f) r

Tactic:
use r, hr

Goal state after:
case right
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
⊢ (f * g) r = (g * f) r
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η + 1⟯

Tactic:
have H := IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
      ((integral {p ^ (k + 1)} K L).isIntegral (η + 1)).isAlgebraic

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η + 1⟯
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
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n

Tactic:
convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _

Goal state after:
case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q + 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_3 i

case convert_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ ≤ ?convert_3 i

case convert_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < ?convert_3 i