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

Goal state before:
pp: ι : 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✝¹⁰ : NormedField 𝕜
inst✝⁹ : NormedField 𝕜'
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜' G
inst✝¹ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = σ a • A f
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun x ↦ A x, map_add' := hadd, map_smul' := hsmul }
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h : ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
⊢ ∃ s C,
    (normSeminorm 𝕜' G).comp { toFun := fun x ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
      C • s.sup (schwartzSeminormFamily 𝕜 D E)

Tactic:
exact ⟨s, ⟨C, hC⟩, h⟩

Goal state after:
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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
⊢ ‖(-(2 * ↑π * I)) ^ n‖ *
      ‖iteratedFDeriv ℝ k (fun x ↦ ((smulRightL ℝ (fun x ↦ W) E) (T fun x_1 ↦ L x, f x).1) (T fun x_1 ↦ L x, f x).2)
          v‖ ≤
    (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C

Tactic:
simp only [mul_assoc, norm_pow, norm_neg, Complex.norm_mul, Complex.norm_ofNat, norm_real,
    Real.norm_eq_abs, abs_of_nonneg pi_nonneg, norm_I, mul_one, smulRightL_apply, ge_iff_le]

Goal state after:
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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
⊢ (2 * π) ^ n * ‖iteratedFDeriv ℝ k (fun x ↦ (T fun x_1 ↦ L x).smulRight (f x)) v‖ ≤
    (2 * π) ^ n * ((2 * ↑n + 2) ^ k * (‖L‖ ^ n * C))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : 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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
⊢ ∀ (f g : 𝓢(E, F)) (x : E), (L x).smulRight ((f + g) x) = (L x).smulRight (f x) + (L x).smulRight (g x)

Tactic:
intros

Goal state after:
ι : 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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
f✝ g✝ : 𝓢(E, F)
x✝ : E
⊢ (L x✝).smulRight ((f✝ + g✝) x✝) = (L x✝).smulRight (f✝ x✝) + (L x✝).smulRight (g✝ x✝)
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: case e_f
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
⊢ ↑(e ((-L (v - v₀)) w)) • f v = ↑(e ((L v₀) w - (L v) w)) • f v

Tactic:
← LinearMap.sub_apply,

Goal state after:
case e_f
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
⊢ ↑(e ((-L (v - v₀)) w)) • f v = ↑(e ((L v₀ - L v) w)) • f v
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : 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✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (f g : 𝓢(E, F)), (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction

Tactic:
intros

Goal state after:
ι : 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✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f✝ g✝ : 𝓢(E, F)
⊢ (f✝ + g✝).toBoundedContinuousFunction = f✝.toBoundedContinuousFunction + g✝.toBoundedContinuousFunction
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : 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✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (a : 𝕜) (f : 𝓢(E, F)), (a • f).toBoundedContinuousFunction = (RingHom.id 𝕜) a • f.toBoundedContinuousFunction

Tactic:
intros

Goal state after:
ι : 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✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
a✝ : 𝕜
f✝ : 𝓢(E, F)
⊢ (a✝ • f✝).toBoundedContinuousFunction = (RingHom.id 𝕜) a✝ • f✝.toBoundedContinuousFunction
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : 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✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (f g : 𝓢(E, F)), (f + g).toZeroAtInfty = f.toZeroAtInfty + g.toZeroAtInfty

Tactic:
intros

Goal state after:
ι : 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✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f✝ g✝ : 𝓢(E, F)
⊢ (f✝ + g✝).toZeroAtInfty = f✝.toZeroAtInfty + g✝.toZeroAtInfty
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : 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✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (a : 𝕜) (f : 𝓢(E, F)), (a • f).toZeroAtInfty = (RingHom.id 𝕜) a • f.toZeroAtInfty

Tactic:
intros

Goal state after:
ι : 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✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
a✝ : 𝕜
f✝ : 𝓢(E, F)
⊢ (a✝ • f✝).toZeroAtInfty = (RingHom.id 𝕜) a✝ • f✝.toZeroAtInfty
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm ((fun x ↦ (1 + ‖x‖) ^ (-↑k)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ ≤
    eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ∞ μ

Tactic:
refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ AEStronglyMeasurable (fun x ↦ (1 + ‖x‖) ^ (-↑k)) μ
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
| ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ

Tactic:
← integral_add_left_eq_self x₀ (μ := μ)
    (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)),

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
| ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + x))) • g (x₀ - (x₀ + x)) ∂μ
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ 0 ≤ ↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
simp [mul_nonneg]

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

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

Tactic:
mul_rpow,

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

case hx
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

pp: case hx
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

pp: case hy
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

Tactic:
mul_rpow,

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

case hx
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

case hx
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
B : volume ↑(LinearMap.snd ℝ ℝ ℝ).ker = 0
⊢ polarCoord.source =ᵐ[volume] univ

Tactic:
simp only [ae_eq_univ]

Goal state after:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
B : volume ↑(LinearMap.snd ℝ ℝ ℝ).ker = 0
⊢ volume polarCoord.sourceᶜ = 0
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.source, f p

Tactic:
rw [← setIntegral_univ]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in univ, f x = ∫ (p : ℝ × ℝ) in polarCoord.source, f p
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
E : Fin n → Type u_3
mE : (i : Fin n) → MeasurableSpace (E i)
μ : (i : Fin n) → Measure (E i)
inst✝ : ∀ (i : Fin n), SigmaFinite (μ i)
f : (i : Fin n) → E i → 𝕜
⊢ ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
induction n with
  | zero => simp [measureReal_def]
  | succ n n_ih =>
      calc
        _ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]

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

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

Tactic:
have aux : (1 / r : ℂ) ^ a = 1 / r * (1 / r) ^ (a - 1) := by
    nth_rewrite 2 [← cpow_one (1 / r : ℂ)]
    rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Gamma a
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume

Tactic:
simp_rw [norm_cexp_neg_mul_sq_add_mul_I' hb.ne', neg_sub _ (c ^ 2 * _),
    sub_eq_add_neg _ (b.re * _), Real.exp_add]

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a ↦ rexp (c ^ 2 * (b.im ^ 2 / b.re + b.re)) * rexp (-(b.re * (a - b.im * c / b.re) ^ 2)))
    volume
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : Multiplicative W
v : V
⊢ ((charMonoidHom he hL) w) v = ↑(e ((L v) (Multiplicative.toAdd w)))

Tactic:
by simp [charMonoidHom]

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

Goal state before:
pp: case e'_3
d : Type u_1
inst✝ : Fintype d
a : d → ℝ
this :
  Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map (fun x i ↦ ↑(↑x i)) (Measure.comap Subtype.val volume)
⊢ (Measure.pi fun i ↦ volume.restrict (Ioc (a i) (a i + 1))) =
    volume.restrict {f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}

Tactic:
convert! (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm

Goal state after:
case e'_4
d : Type u_1
inst✝ : Fintype d
a : d → ℝ
this :
  Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map (fun x i ↦ ↑(↑x i)) (Measure.comap Subtype.val volume)
⊢ {f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} = univ.pi fun i ↦ Ioc (a i) (a i + 1)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case pos
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (n + -m)) x = 1

Tactic:
simpa only [h, add_neg_cancel, mFourier_zero, probReal_univ, one_smul] using!
      integral_const (α := UnitAddTorus d) (μ := volume) (1 : ℂ)

Goal state after:
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 _)]
  refine HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)
  simp only [← mFourierBasis_repr, HilbertBasis.repr_apply_apply, inner_conj_symm,
    mul_comm (inner ℂ f _)]

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

Goal state before:
pp: ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ p i ^ n i = 1

Tactic:
by rw [h, pow_zero]

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

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), ‖e x‖ = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ⨆ x, ‖(ContinuousMap.restrict (↑K) (e * g)) x‖ = ⨆ x, ‖(ContinuousMap.restrict (↑K) g) x‖

Tactic:
restrict_apply,

Goal state after:
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 := ⋯ }
this : ∀ (x : ℝ), ‖e x‖ = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ⨆ x, ‖(e * g) ↑x‖ = ⨆ x, ‖g ↑x‖
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight ↑n)) x = ∫ (x : ℝ), e x * f x

Tactic:
suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
      apply integrable_of_summable_norm_Icc
      convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
      simp_rw [mul_comp] at eadd ⊢
      simp_rw [eadd]
      exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val

Tactic:
exact roots_prod_X_sub_C (primitiveRoots n R)

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).degree = ↑n.totient

Tactic:
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n ℤ).degree = ↑n.totient

n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0