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

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

pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume

Tactic:
· exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume
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
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-((↑c)⁻¹ * ↑‖v‖ ^ 2))‖ * ‖f v‖ ≤ ‖f v‖

Tactic:
norm_cast

Goal state after:
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
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * ‖v‖ ^ 2))‖ * ‖f v‖ ≤ ‖f v‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ -s.re < ↑0

Tactic:
norm_cast

Goal state after:
s : ℂ
hs : 0 < s.re
⊢ -s.re < 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Tactic:
· exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))

Tactic:
norm_cast

Goal state after:
case e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ ↑(a - 1) * ↑(rexp (-(r * t)))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (-b).re < 0

Tactic:
rwa [neg_re, neg_lt_zero]

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

Goal state before:
pp: case e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * ↑√(∑ x, v x ^ 2) ^ 2) + ∑ i, c * (↑(v i) * ↑(w.ofLp i)) = -∑ x, b * ↑(v x) ^ 2 + ∑ x, c * (↑(w.ofLp x) * ↑(v x))

Tactic:
norm_cast

Goal state after:
case e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * ↑(√(∑ x, v x ^ 2) ^ 2)) + ∑ x, c * ↑(v x * w.ofLp x) = -∑ x, b * ↑(v x ^ 2) + ∑ x, c * ↑(w.ofLp x * v x)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a.e_a
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
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑(-π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2) = -↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2

Tactic:
norm_cast

Goal state after:
case e_f.e_a.e_a
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
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ -π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2 = -π ^ 2 * c * ‖v - w‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_2.e'_7.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ ↑√(∑ x, y x ^ 2) ^ 2 = ∑ i, ↑(y i) ^ 2 ∨ b = 0

Tactic:
norm_cast

Goal state after:
case e'_2.e'_7.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ √(∑ x, y x ^ 2) ^ 2 = ∑ i, y i ^ 2 ∨ b = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_3.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ ↑√(∑ x, w.ofLp x ^ 2) ^ 2 = ∑ i, ↑(w.ofLp i) ^ 2

Tactic:
norm_cast

Goal state after:
case e'_3.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ √(∑ x, w.ofLp x ^ 2) ^ 2 = ∑ i, w.ofLp i ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2) = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2)

Tactic:
simpa using integral_cexp_neg_mul_sq_norm_add hb 0 (0 : V)

Goal state after:
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)
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f

Tactic:
by
  let ι := Fin (Module.finrank ℝ E)
  let b := stdOrthonormalBasis ℝ E
  have : ∀ i (hi : i ∈ Finset.univ),
      (fun x ↦ Complex.ofReal (inner ℝ x (b i)) ^ 2).HasTemperateGrowth := by
    fun_prop
  simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, Complex.ofReal_sum, Complex.ofReal_pow,
    fourierMultiplierCLM_sum F this, sum_apply, Finset.smul_sum]
  congr 1
  ext i x
  simp_rw [lineDeriv_eq_fourierMultiplierCLM, map_smul, smul_smul]
  rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop),
    ← Complex.coe_smul (-(2 * π) ^ 2)]
  congr 4
  · ring_nf
    simp
  · simp [sq, Pi.mul_def]

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
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ ↑((1 + ‖x‖ ^ 2) ^ (s / 2)) * ↑((1 + ‖x‖ ^ 2) ^ (s' / 2)) = ↑((1 + ‖x‖ ^ 2) ^ ((s + s') / 2))

Tactic:
norm_cast

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
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖x‖ ^ 2) ^ (s' / 2) = (1 + ‖x‖ ^ 2) ^ ((s + s') / 2)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : ¬j = i
⊢ (fourier (Pi.single i 1 j)) (z j) = 1

Tactic:
simp only [Pi.single_eq_of_ne hj, fourier_zero]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
a : d → ℝ
⊢ MeasurePreserving (⇑(measurableEquivPiIoc a)) volume (Measure.comap Subtype.val volume)

Tactic:
by
  refine (⟨(measurableEquivPiIoc a).symm.measurable, symm ?_⟩ :
    MeasurePreserving (measurableEquivPiIoc a).symm _ _).symm
  have := Measure.map_map (μ := volume.comap Subtype.val) (measurable_pi_lambda
    (fun (x : d → ℝ) => (fun i => x i : UnitAddTorus d))
    (fun i => AddCircle.measurable_mk'.comp (measurable_pi_apply i)))
    measurable_subtype_coe (α := {x : d → ℝ // ∀ i, x i ∈ Ioc (a i) (a i + 1)})
  simp only [Function.comp_def] at this
  simp_rw [coe_symm_measurableEquivPiIoc, ← this]
  convert! (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm
  · simp [volume, AddCircle.haarAddCircle]
  · convert!
    (map_comap_subtype_coe (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc (a := a i))) volume)
    convert! (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm
    grind

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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞

Tactic:
norm_cast

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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ 2 < ∞
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:
by
    induction x using DirectSum.induction_on with
    | zero => simp
    | of i x =>
      rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of, DirectSum.toAddMonoid_of,
        dif_neg i.prop]
    | add x y hx hy => rw [map_add, map_add, hx, hy]

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

Goal state before:
pp: case e'_3
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
x : E
⊢ ↑((1 + ‖x‖ ^ 2) ^ (s / 2)) * ↑((1 + ‖x‖ ^ 2) ^ (-s / 2)) = 1

Tactic:
norm_cast

Goal state after:
case e'_3
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖x‖ ^ 2) ^ (-s / 2) = 1
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ (1 + ‖x‖ ^ 2) * |(1 + ‖x‖ ^ 2) ^ (-(1 / 2))| ^ 2 = 1

Tactic:
norm_cast

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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ (1 + ‖x‖ ^ 2) * |(1 + ‖x‖ ^ 2) ^ (-(1 / 2))| ^ 2 = 1
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖↑(‖x‖ ^ 2 * ((1 + ‖x‖ ^ 2) ^ 1)⁻¹)‖ ≤ 1

Tactic:
norm_cast

Goal state after:
case h
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖‖x‖ ^ 2 * ((1 + ‖x‖ ^ 2) ^ 1)⁻¹‖ ≤ 1
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖‖x‖ ^ 2 * ((1 + ‖x‖ ^ 2) ^ 1)⁻¹‖ ≤ 1

Tactic:
simp only [norm_mul, norm_pow, abs_norm, norm_inv, Real.norm_eq_abs]

Goal state after:
case h
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖x‖ ^ 2 * (|1 + ‖x‖ ^ 2| ^ 1)⁻¹ ≤ 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
⊢ ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x

Tactic:
have : Summable (fourierCoeff F) := by
    convert! h_sum
    exact Real.fourierCoeff_tsum_comp_add h_norm _

Goal state after:
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
⊢ μ p = -1

Tactic:
rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]

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
⊢ ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε

Tactic:
let A := {v : V | ‖v‖ ≤ R + 1}

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}
⊢ ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: k : ℕ
M : Type u_7
B : Type u_8
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : ↥N
⊢ (↑ζ ^ k = 1 ∧ ∀ (l : ℕ), ↑ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

Tactic:
norm_cast

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ (ζ ^ k) ^ i = 1

Tactic:
h.pow_eq_one,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ 1 ^ i = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ (ζ ^ k) ^ a = 1

Tactic:
h.pow_eq_one,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ 1 ^ a = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ Set.InjOn (fun x ↦ ζ ^ x) ↑(range n)

Tactic:
intro i

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
⊢ i ∈ ↑(range n) → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range n) → (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) x₂ → i = x₂
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ f (ζ ^ k) = 1

Tactic:
h.pow_eq_one,

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ f 1 = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ ↑l = 1 ↔ ↑k ∣ ↑l

Tactic:
exact_mod_cast h.pow_eq_one_iff_dvd l

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

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'

Tactic:
norm_cast

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ k ∣ l'
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
⊢ ∀ i ∈ n.properDivisors, (cyclotomic' i K).Monic

Tactic:
intro i

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
⊢ i ∈ n.properDivisors → (cyclotomic' i K).Monic
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ⋯
⊢ ∀ i ∈ k.properDivisors, (cyclotomic' i K).Monic

Tactic:
intro i

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
i : ℕ
⊢ i ∈ k.properDivisors → (cyclotomic' i K).Monic
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✝ h : IsPrimitiveRoot ζ k
⊢ ∀ (x y : ℤ),
    Additive.ofMul ⟨(fun x ↦ ζ ^ x) (x + y), ⋯⟩ =
      Additive.ofMul ⟨(fun x ↦ ζ ^ x) x, ⋯⟩ + Additive.ofMul ⟨(fun x ↦ ζ ^ x) y, ⋯⟩

Tactic:
intro i

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 R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
i : ℤ
⊢ ∀ (y : ℤ),
    Additive.ofMul ⟨(fun x ↦ ζ ^ x) (i + y), ⋯⟩ =
      Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩ + Additive.ofMul ⟨(fun x ↦ ζ ^ x) y, ⋯⟩
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case left
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✝ h : IsPrimitiveRoot ζ k
⊢ ∀ (a : ZMod k),
    (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
            ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
          a =
        0 →
      a = 0

Tactic:
intro i

Goal state after:
case left
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✝ h : IsPrimitiveRoot ζ k
i : ZMod k
⊢ (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i =
      0 →
    i = 0
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑ζ ^ n = 1

Tactic:
norm_cast

Goal state after:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑(ζ ^ n) = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ↑i = ↑↑i

Tactic:
norm_cast

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ WithBot.unbotD 0 ↑n.totient = n.totient

Tactic:
norm_cast

Goal state after:
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 ℤ ∣ X ^ n - 1

Tactic:
← prod_cyclotomic_eq_X_pow_sub_one hn

Goal state after:
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i ∈ n.divisors, cyclotomic i ℤ
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
e : α ^ n = a
hn : n > 0
hα : α = 0
⊢ nthRoots n a = Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)

Tactic:
rw [hα, zero_pow hn.ne'] at e
    simp only [hα, e.symm, nthRoots_zero_right, mul_zero,
      Multiset.map_const', Multiset.card_range]

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

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

Tactic:
intro i

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
i : ℕ
⊢ i ∈ n.properDivisors → (cyclotomic i R).Monic