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

Goal state before:
pp: 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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
⊢ ContDiff ℝ (↑N) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)

Tactic:
by_cases h'f : Integrable f μ
  · exact (hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f.1).contDiff
  · have : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0 := by
      ext w; simp [fourierIntegral, integral, h'f]
    simpa [this] using! contDiff_const

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

Goal state before:
pp: case h
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := ⋯
f : 𝓢(D, V)
h' : ∀ (x : D), ‖f x‖ ≤ (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)
⊢ ∫ (x : D), (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f) ∂μ ≤
    (2 ^ n * ∫ (x : D), (1 + ‖x‖) ^ (-↑n) ∂μ) * ((Finset.Iic m).sup (schwartzSeminormFamily 𝕜 D V)) f

Tactic:
unfold schwartzSeminormFamily

Goal state after:
case h
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' : ∀ (x : D), ‖f x‖ ≤ (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)
⊢ ∫ (x : D), (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f) ∂μ ≤
    (2 ^ n * ∫ (x : D), (1 + ‖x‖) ^ (-↑n) ∂μ) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
rw [two_mul, eq]

Goal state after:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f x = (∫ (x : ℝ) in Ioi 0, f x) + ∫ (x : ℝ) in Ioi 0, f x
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℝ
x✝ : IntegrableAtFilter (fun x ↦ x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x ↦ x ^ s) t volume
⊢ s < -1

Tactic:
obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht

Goal state after:
s : ℝ
x✝ : IntegrableAtFilter (fun x ↦ x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x ↦ x ^ s) t volume
a : ℝ
ha : ∀ (b : ℝ), a ≤ b → b ∈ t
⊢ s < -1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ rexp (-x) * x ^ s = 0

pp: case refine_2
s : ℝ
⊢ Tendsto (fun x ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Tactic:
· exfalso; exact (exp_pos (-(1 / 2) * x)).ne' hx

Goal state after:
case refine_2
s : ℝ
⊢ Tendsto (fun x ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ GammaIntegral 1 = 1

Tactic:
by
  simpa only [← ofReal_one, GammaIntegral_ofReal, ofReal_inj, sub_self, rpow_zero,
    mul_one] using integral_exp_neg_Ioi_zero

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

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

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

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

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

Tactic:
have hn : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]

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

Goal state before:
pp: case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 ≤ᵐ[volume.restrict (Ioi 0)] fun x ↦ rexp (-x) * x ^ (s - 1)

pp: case hfi
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
· refine eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_
    exact fun x hx => (mul_pos (exp_pos _) (rpow_pos_of_pos hx _)).le

Goal state after:
case hfi
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
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) * ↑(rexp (-(r * t)))

Tactic:
← ofReal_cpow ht.le,

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.Gamma.Basic

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t)) = (1 / r) ^ a * Gamma a

Tactic:
rw [← ofReal_inj, ofReal_mul, ← Gamma_ofReal, ofReal_cpow (by positivity), ofReal_div]
  convert! integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr
  refine integral_ofReal.symm.trans <| setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
  norm_cast
  simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
congr 2

Goal state after:
case e_a
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)

case e_a
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b)) = -↑π / b * (↑t + I * c) ^ 2
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 : 𝕜
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F (c • g)) f = (c • fourierMultiplierCLM F g) f

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smul hg]

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

Goal state before:
pp: case e'_2.e'_7.e'_5
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
x✝ : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ‖e x✝‖ = ‖x✝‖

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip]

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

Goal state before:
pp: case e'_2.e'_7.e'_6
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
x✝ : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ⟪w, e x✝⟫ = ⟪e.symm w, x✝⟫

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip]

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

Goal state before:
pp: case e'_3.e'_5
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Module.finrank ℝ V = Fintype.card (Fin (Module.finrank ℝ V))

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip]

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

Goal state before:
pp: case e'_3.e'_6
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ‖w‖ = ‖e.symm w‖

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip]

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

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smul hg]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ↑(mFourierBasis.repr f) i = ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t

pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t = mFourierCoeff (↑↑f) i

Tactic:
· rw [mFourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_mFourierBasis]
    simp only [RCLike.inner_apply, mul_comm]

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t = mFourierCoeff (↑↑f) i
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ (starRingEnd ℂ) (mFourierCoeff (↑↑f) i) * mFourierCoeff (↑↑g) i)
    (∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑f t) * ↑↑g t)

Tactic:
simp_rw [mul_comm (conj _)]

Goal state after:
d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ mFourierCoeff (↑↑g) i * (starRingEnd ℂ) (mFourierCoeff (↑↑f) i))
    (∫ (t : UnitAddTorus d), ↑↑g t * (starRingEnd ℂ) (↑↑f t))
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Finite G
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
by
  obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)
  exact ⟨ι, inst, n, h₁, ⟨MulEquiv.toAdditive.symm <| h₂.some.trans <|
    (DirectSum.addEquivProd _).trans (MulEquiv.piMultiplicative _).toAdditiveRight⟩⟩

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
⊢ AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup ≤ B.toAddSubgroup

Tactic:
rw [SetLike.le_def] at h ⊢

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 : ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R ↑n) A → x ∈ B
this✝ : A.toAddSubgroup.FG
this : (AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup).IsFiniteRelIndex A.toAddSubgroup
⊢ ∀ ⦃x : K⦄, x ∈ AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup → x ∈ B.toAddSubgroup
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)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ (smulLeftCLM F (g * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2)))) (𝓕 f) =
    (smulLeftCLM F ((fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * ⇑g')) (𝓕 f)

Tactic:
congr 2

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)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ (g * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) = (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * ⇑g'
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e_f
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
x : ℝ
⊢ cexp (2 * ↑π * I * ↑(-m) * ↑x / ↑1) * f x = cexp (↑(-2 * π * x * ↑m) * I) * f x

Tactic:
congr 2

Goal state after:
case e_f.e_a
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
x : ℝ
⊢ 2 * ↑π * I * ↑(-m) * ↑x / ↑1 = ↑(-2 * π * x * ↑m) * I
Module: Mathlib.Data.PNat.Prime

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

Tactic:
by
  intro h; iterate 2 rw [gcd_comm]; symm
  apply Coprime.gcd_mul_left_cancel _ h

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

Goal state before:
pp: n : ℕ
hn : IsPrimePow n
hn' : ¬Nat.Prime n
⊢ μ n = 0

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ μ (p ^ k) = 0
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 : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = ↑(ζ p) + f p

Tactic:
zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = ↑1 + f p
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, μ (n / d) • G d = f n
⊢ ∀ x ∈ n.divisors, μ (n / x) • g x = μ (n / x) • G x

Tactic:
intro d

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, μ (n / d) • G d = f n
d : ℕ
⊢ d ∈ n.divisors → μ (n / d) • g d = μ (n / d) • G d
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
⊢ ∀ x ∈ n.divisors, f x = F x

Tactic:
intro d

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
d : ℕ
⊢ d ∈ n.divisors → f d = F d
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:
by
  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
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:
rw [← map_pow, h.pow_eq_one, map_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ }, (X - C ζ)

Tactic:
simp only [Finset.prod_mk]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ ↦ X - C ζ) (nthRoots n 1)).prod
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
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → k ∣ l

Tactic:
rw [h.eq_orderOf]

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
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l
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 (f ζ) k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

Tactic:
rw [h.eq_orderOf]

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 (f ζ) k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), ζ ^ l = 1 → orderOf (f ζ) ∣ l
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:
← dvd_neg,

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.RootsOfUnity.Complex

Goal state before:
pp: case e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + -↑n

Tactic:
sub_eq_add_neg

Goal state after:
case e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i + -↑n = ↑i + -↑n