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✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
N : ℕ
hN₁ : 1 ≤ N
hN₂ : N ≤ n
hN₁' : N ≠ 0
⊢ C ≤ C + 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : 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✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v ↦ e (-(L v) x) • g v) μ
hf : Integrable (fun v ↦ e (-(L v) w) • f v) μ
this : Integrable (fun v ↦ e (-(L v) (-w)) • e (-(L v) w) • f v) μ
⊢ Integrable f μ

Tactic:
simp_rw [← mul_smul (e _) (e _) (f _), ← e.map_add_eq_mul, map_neg, neg_add_cancel,
    e.map_zero_eq_one, one_smul] at this

Goal state after:
𝕜 : 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✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v ↦ e (-(L v) x) • g v) μ
hf : Integrable (fun v ↦ e (-(L v) w) • f v) μ
this : Integrable (fun v ↦ f v) μ
⊢ Integrable f μ
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‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v (n + 1)) w).curryLeft =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fourierSMulRight L fun v ↦ fourierPowSMulRight L f v n) w

Tactic:
ext w' m

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
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ
w' : W
m : Fin n → W
⊢ ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v (n + 1)) w).curryLeft
        w')
      m =
    ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fourierSMulRight L fun v ↦ fourierPowSMulRight L f v n)
          w)
        w')
      m
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case zero
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
hn : ↑0 ≤ N
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ 0 f) = fun w ↦
    fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w 0

Tactic:
ext w m

Goal state after:
case zero
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
hn : ↑0 ≤ N
w : W
m : Fin 0 → V
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ 0 f) w) m =
    (fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w 0) m
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case succ
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ (n + 1) f) = fun w ↦
    fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w (n + 1)

Tactic:
ext w m

Goal state after:
case succ
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ (n + 1) f) w) m =
    (fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w (n + 1)) m
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✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
x✝² x✝¹ : 𝓢(E, F)
x✝ : E
⊢ (⇑L ∘ ⇑(x✝² + x✝¹)) x✝ = (⇑L ∘ ⇑x✝²) x✝ + (⇑L ∘ ⇑x✝¹) x✝

Tactic:
simp

Goal state after:
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✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
x✝² : 𝕜
x✝¹ : 𝓢(E, F)
x✝ : E
⊢ (⇑L ∘ ⇑(x✝² • x✝¹)) x✝ = (RingHom.id 𝕜) x✝² • (⇑L ∘ ⇑x✝¹) x✝

Tactic:
simp

Goal state after:
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✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(E, F)
x : E
⊢ ((compSubConstCLM 𝕜 0) f) x = ((ContinuousLinearMap.id 𝕜 𝓢(E, F)) f) x

Tactic:
simp

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

Goal state before:
pp: D : Type u_4
V : Type u_9
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
x : D
⊢ ‖f x‖ = ‖iteratedFDeriv ℝ 0 (⇑f) x‖

Tactic:
simp

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

Goal state before:
pp: D : Type u_4
V : Type u_9
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
x✝ : D
⊢ ‖f x✝‖ ≤ ‖‖x✝‖ ^ 0 * ‖f x✝‖‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : 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
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℂ F
inst✝¹² : NormedAddCommGroup G
inst✝¹¹ : NormedSpace ℂ G
inst✝¹⁰ : TopologicalSpace 𝕜
inst✝⁹ : IsTopologicalRing 𝕜
inst✝⁸ : TopologicalSpace V
inst✝⁷ : BorelSpace V
inst✝⁶ : TopologicalSpace W
inst✝⁵ : MeasurableSpace W
inst✝⁴ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝³ : SigmaFinite μ
inst✝² : SigmaFinite ν
inst✝¹ : SecondCountableTopologyEither W V
σ : ℂ →+* ℂ
inst✝ : RingHomIsometric σ
f : V → E
g : W → F
M : F →L[ℂ] E →SL[σ] G
he : Continuous[inst✝¹⁰, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹⁰] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun p ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
ξ : W
x : V
⊢ ‖f x‖ = ‖e (-(L x) ξ) • f x‖

Tactic:
simp

Goal state after:
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)
x✝ : E
⊢ (f✝ + g✝).toBoundedContinuousFunction x✝ = (f✝.toBoundedContinuousFunction + g✝.toBoundedContinuousFunction) x✝

Tactic:
simp

Goal state after:
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)
x✝ : E
⊢ (a✝ • f✝).toBoundedContinuousFunction x✝ = ((RingHom.id 𝕜) a✝ • f✝.toBoundedContinuousFunction) x✝

Tactic:
simp

Goal state after:
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)
x✝ : E
⊢ (f✝ + g✝).toZeroAtInfty x✝ = (f✝.toZeroAtInfty + g✝.toZeroAtInfty) x✝

Tactic:
simp

Goal state after:
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)
x✝ : E
⊢ (a✝ • f✝).toZeroAtInfty x✝ = ((RingHom.id 𝕜) a✝ • f✝.toZeroAtInfty) x✝

Tactic:
simp

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

Goal state before:
pp: case hiφ
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
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (fun i ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)

Tactic:
have : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1) := by
      rw [← h'φ]
      exact (aecover_closedBall tendsto_id).integral_tendsto_of_countably_generated I
    apply this.congr'
    filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
    rw [integral_const_mul, setIntegral_comp_smul_of_pos _ _ _ hc, smul_eq_mul, ← mul_assoc,
      mul_inv_cancel₀ (by positivity), _root_.smul_closedBall _ _ zero_le_one]
    simp [abs_of_nonneg hc.le]

Goal state after:
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)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    ↑((eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ).toNNReal * 2 ^ k) *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]

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‖
⊢ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ * ↑(2 ^ k) *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 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✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: 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✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ 1 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: 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✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm (↑↑f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∀ (a : E),
    ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ) a = (hg₁.toSchwartzMap hg₂) a →
      (↑↑f - ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ)) a = (↑↑f - g) a

Tactic:
simp

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

Goal state before:
pp: case hb
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✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm (↑↑f - g) p μ ≤ ENNReal.ofReal ε
this : ↑↑f - ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ) =ᵐ[μ] ↑↑f - g
⊢ ENNReal.ofReal ε ≠ ∞

Tactic:
simp

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

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

Tactic:
hf

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

Goal state before:
pp: a : ℂ
ha : 0 < a.re
c : ℝ
⊢ IntegrableOn (fun x ↦ Complex.exp (a * ↑x)) (Iic c) volume

Tactic:
simpa using Iff.mpr integrableOn_Iic_iff_integrableOn_Iio
    (integrableOn_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)).comp_neg_Iio

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

Goal state before:
pp: case φ_int
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ Integrable (fun v ↦ e (-((ContinuousLinearMap.toLinearMap₁₂ L) v) w) • f v) μ

Tactic:
apply (fourierIntegral_convergent_iff he _ _).2 hf
    exact L.continuous₂

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

Goal state before:
pp: case h₂
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
v : V
w : W
⊢ ∏ x, ‖v‖ ≤ ‖v‖ ^ n

Tactic:
simp

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

Goal state before:
pp: a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)

Tactic:
have ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1))) := by
    apply Tendsto.div_const
    simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))

Goal state after:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun t ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: case φ_int
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst✝¹¹ : Fintype ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ Integrable (fun v ↦ e (-((ContinuousLinearMap.toLinearMap₁₂ L) v) w) • f v) μ

Tactic:
apply (fourierIntegral_convergent_iff he _ _).2 hf
    exact L.continuous₂

Goal state after: