mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℂ 𝕜 F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
⊢ fourierMultiplierCLM F (c • g) = c • fourierMultiplierCLM F g

Tactic:
ext1 f

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℂ 𝕜 F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F (c • g)) f = (c • fourierMultiplierCLM F g) f
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℂ 𝕜 F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
⊢ (fourierMultiplierCLM F fun x ↦ ∑ i ∈ s, g i x) = ∑ i ∈ s, fourierMultiplierCLM F (g i)

Tactic:
ext1 f

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℂ 𝕜 F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F fun x ↦ ∑ i ∈ s, g i x) f = (∑ i ∈ s, fourierMultiplierCLM F (g i)) f
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : NormedSpace ℂ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℂ 𝕜 F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ fourierMultiplierCLM F g₁ ∘SL fourierMultiplierCLM F g₂ = fourierMultiplierCLM F (g₁ * g₂)

Tactic:
ext1 f

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : NormedSpace ℂ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℂ 𝕜 F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F g₁ ∘SL fourierMultiplierCLM F g₂) f = (fourierMultiplierCLM F (g₁ * g₂)) f
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f
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 : Fin (Module.finrank ℝ E)
x : E
⊢ ((2 * ↑π * Complex.I) •
        (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)))
          ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f))
      x =
    -(2 * π) ^ 2 • ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x

Tactic:
simp_rw [map_smul, smul_apply, smul_smul]

Goal state after:
case e_f
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 : Fin (Module.finrank ℝ E)
x : E
⊢ (2 * ↑π * Complex.I * (2 * ↑π * Complex.I)) •
      ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f)) x =
    -(2 * π) ^ 2 • ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x
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)
⊢ Δ 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), (inner ℝ · (b i) ^ 2).HasTemperateGrowth := by
    fun_prop
  simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, fourierMultiplierCLM_sum F this,
    _root_.sum_apply, Finset.smul_sum]
  congr 1
  ext i x
  simp_rw [smul_apply, lineDeriv_eq_fourierMultiplierCLM]
  rw [← fourierMultiplierCLM_ofReal ℂ (by fun_prop)]
  simp_rw [map_smul, smul_apply, smul_smul]
  congr 1
  · ring_nf
    simp
  · rw [fourierMultiplierCLM_ofReal ℂ (by fun_prop),
      fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
    simp [sq, Pi.mul_def]

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
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁ = fourierMultiplierCLM F (g₁ * g₂)

Tactic:
ext1 f

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
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ (fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁) f = (fourierMultiplierCLM F (g₁ * g₂)) 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
g : E → ℂ
hg : Function.HasTemperateGrowth g
c : ℂ
⊢ fourierMultiplierCLM F (c • g) = c • fourierMultiplierCLM F g

Tactic:
ext1 f

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
g : E → ℂ
hg : Function.HasTemperateGrowth g
c : ℂ
f : 𝓢'(E, F)
⊢ (fourierMultiplierCLM F (c • g)) f = (c • fourierMultiplierCLM F g) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f : 𝓢(V, H)
⊢ ∫ (ξ : V), ‖(𝓕 f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

Tactic:
apply Complex.ofRealLI.injective
  simpa [← LinearIsometry.integral_comp_comm, inner_self_eq_norm_sq_to_K] using
    integral_inner_fourier_fourier f f

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

Goal state before:
pp: case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x x' : E
⊢ x' ∈ dsupport ⇑(TemperedDistribution.delta x) → x' ∈ {x}

Tactic:
hx'

Goal state after:
case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x x' : E
hx' : x' ∈ dsupport ⇑(TemperedDistribution.delta x)
⊢ x' ∈ {x}
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤) u
h₄ : u x = 1
h₁' : tsupport (⇑Complex.ofRealCLM ∘ u) ⊆ s
h₂' : HasCompactSupport (⇑Complex.ofRealCLM ∘ u)
⊢ (TemperedDistribution.delta x) (h₂'.toSchwartzMap ⋯) ≠ 0

Tactic:
simp [h₄]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ 𝓕 (f.toLp 2 volume) = (𝓕 f).toLp 2 volume

Tactic:
by
  apply LinearMap.extendOfNorm_eq
  · exact SchwartzMap.denseRange_toLpCLM ENNReal.ofNat_ne_top
  use 1
  intro f
  rw [one_mul]
  exact (norm_fourier_toL2_eq f).le

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

Goal state before:
pp: case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
x' : E
⊢ x' ∈ dsupport ⇑(delta x) → x' ∈ {x}

Tactic:
hx'

Goal state after:
case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
x' : E
hx' : x' ∈ dsupport ⇑(delta x)
⊢ x' ∈ {x}
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: case hp.hf
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ 𝓕 (toTemperedDistribution y)

pp: case hp.hg
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ toTemperedDistribution (𝓕 y)

Tactic:
· exact (fourierCLM ℂ 𝓢'(E, F) ∘L toTemperedDistributionCLM F volume 2).continuous

Goal state after:
case hp.hg
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ toTemperedDistribution (𝓕 y)
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: case hp
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ IsClosed {b | p b}

Tactic:
apply isClosed_eq
    · exact (fourierCLM ℂ 𝓢'(E, F) ∘L toTemperedDistributionCLM F volume 2).continuous
    · exact (toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous

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

Goal state before:
pp: E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
s : Set E
hxs : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
t : Set E := s ∩ ↑Ω
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htx : x ∈ t
u : E → ℝ
h₁ : tsupport u ⊆ t
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑n) u
h₄ : u x = 1
⊢ (delta x) { toFun := u, contDiff' := h₃, hasCompactSupport' := h₂, tsupport_subset' := ⋯ } ≠ 0

Tactic:
simp [h₄]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁ = smulLeftCLM F (g₁ * g₂)

Tactic:
ext1 f

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ (smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁) f = (smulLeftCLM F (g₁ * g₂)) f
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
⊢ |inner ℝ x m| ^ 2 * |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 ≤ ‖m‖ ^ 2

Tactic:
have h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2 : ℝ)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹ := by
    field_simp
    norm_cast
    rw [Real.rpow_neg (by positivity), sq_abs, inv_pow]
    field_simp
    calc
      _ = ((1 + ‖x‖ ^ 2) ^ (1 / 2 : ℝ)) ^ (2 : ℝ) := by
        rw [← Real.rpow_mul (by positivity)]; simp
      _ = _ := by simp

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
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
⊢ |inner ℝ x m| ^ 2 * |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 ≤ ‖m‖ ^ 2
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d

Tactic:
by
  trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)
  · simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]
    apply prod_congr rfl; intro p hp
    rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]
  rw [isMultiplicative_zeta.natCast.prodPrimeFactors_add_of_squarefree h_mult hn,
    coe_zeta_mul_apply]

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

Goal state before:
pp: case refine_2
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 ∈ Icc (-x✝ + -S) (-x✝ + -R)

Tactic:
· exact ⟨by linarith [hx.2], by linarith [hx.1]⟩

Goal state after:
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 : ℕ
⊢ IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k

Tactic:
refine ⟨fun hi ↦ ?_, h.pow_of_coprime i⟩
  obtain ⟨a, ha⟩ := i.gcd_dvd_left k
  obtain ⟨b, hb⟩ := i.gcd_dvd_right k
  suffices b = k by
    rwa [this, eq_comm, Nat.mul_eq_right h0.ne', ← Nat.coprime_iff_gcd_eq_one] at hb
  rw [ha] at hi
  rw [mul_comm] at hb
  apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _)
  rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ζ : M
n a b : ℕ
hn : 0 < n
h : IsPrimitiveRoot ζ n
hprod : n = a * b
⊢ IsPrimitiveRoot (ζ ^ a) b

Tactic:
subst n

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ IsPrimitiveRoot (ζ ^ a) b
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_4
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ q.den = (↑n / ↑q.den).den

Tactic:
rw [← Int.cast_natCast, ← Rat.divInt_eq_div, ← Rat.mk_eq_divInt (nz := by simp)]
    apply Nat.Coprime.coprime_mul_left (k := 2)
    convert! q.reduced
    grind

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

Goal state before:
pp: n : ℕ
ζ : ℂ
h : ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
hn : n ≠ 0
⊢ ∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n

Tactic:
obtain ⟨i, h, hin, rfl⟩ := h

Goal state after:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ i_1,
    (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))).arg = ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ i_1.natAbs < n
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case neg.convert_2.right
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * 2 ≤ ↑n

Tactic:
rify at h
    linear_combination 2 * h + (n : ℝ) * one_pos (α := ℝ)

Goal state after:
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
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
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
hn : n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)

case neg
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
hn : ¬n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
constructor
  · intro hξ
    obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_pow_eq_one hξ.pow_eq_one
    rw [h.pow_iff_coprime <| NeZero.pos k] at hξ
    exact ⟨i, hik, hξ, rfl⟩
  · rintro ⟨i, -, hi, rfl⟩; exact h.pow_of_coprime i hi

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

Goal state before:
pp: case neg.h
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
⊢ Multiset.map (fun x ↦ ζ ^ x * α) (range n).val ≤ nthRoots n a

Tactic:
← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα),

Goal state after:
case neg.h
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
⊢ (image (fun x ↦ ζ ^ x * α) (range n)).val ≤ nthRoots n a
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg
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
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R
⊢ False

Tactic:
replace habs :=
    lt_of_lt_of_le (Nat.cast_lt.2 one_lt_two)
      (le_emultiplicity_of_pow_dvd (dvd_trans habs prod))

Goal state after:
case neg
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
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
⊢ False
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)
⊢ ↑((fun x ↦ ⟨↑x ^ b, ⋯⟩) ((fun x ↦ ⟨↑x ^ a, ⋯⟩) x)) = ↑x

Tactic:
simp [← pow_mul,
    pow_eq_pow_of_modEq h (isPrimitiveRoot_of_mem_primitiveRoots x.2).pow_eq_one]

Goal state after:
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
m : ℕ
hcop : m.Coprime n
⊢ (map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)

Tactic:
simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]

Goal state after:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0
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

Goal state after:
case pos
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : n = 0
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R

case neg
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : ¬n = 0
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R