mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
gc_support : (Function.support fun x ↦ g x • c) ⊆ v
⊢ eLpNorm (⇑g) p μ < ∞

Tactic:
have : eLpNorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
      (eLpNorm_indicator_const_le _ _).trans_lt <| by simp [lt_top_iff_ne_top, hμv.ne]

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
gc_support : (Function.support fun x ↦ g x • c) ⊆ v
this : eLpNorm (v.indicator fun _x ↦ 1) p μ < ∞
⊢ eLpNorm (⇑g) p μ < ∞
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g,
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
suffices H :
      ∃ g : α → E, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ HasCompactSupport g by
    rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
    exact ⟨g, g_support, hg, g_cont, g_mem⟩

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g,
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
v w : E
f : 𝓢(E, F)
⊢ ∂_{v + w} f = ∂_{v} f + ∂_{w} f

Tactic:
ext x

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F✝ : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
v w : E
f : 𝓢(E, F)
x : E
⊢ (∂_{v + w} f) x = (∂_{v} f + ∂_{w} f) x
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
r : ℝ
y : E
f : 𝓢(E, F)
⊢ ∂_{r • y} f = r • ∂_{y} f

Tactic:
ext x

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F✝ : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
r : ℝ
y : E
f : 𝓢(E, F)
x : E
⊢ (∂_{r • y} f) x = (r • ∂_{y} f) x
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: 𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_8
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedSpace ℝ E
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
m : D
g : D ≃L[ℝ] E
f : 𝓢(E, F)
⊢ ∂_{m} ((compCLMOfContinuousLinearEquiv 𝕜 g) f) = (compCLMOfContinuousLinearEquiv 𝕜 g) (∂_{g m} f)

Tactic:
ext x

Goal state after:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_8
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedSpace ℝ E
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
m : D
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
⊢ (∂_{m} ((compCLMOfContinuousLinearEquiv 𝕜 g) f)) x = ((compCLMOfContinuousLinearEquiv 𝕜 g) (∂_{g m} f)) x
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable fun i ↦ (V i) (↑f i)

Tactic:
hV.summable_iff_norm_sq_summable

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable fun i ↦ ‖↑f i‖ ^ 2
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
⊢ fourierCoeff (f + g) = fourierCoeff f + fourierCoeff g

Tactic:
ext x

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
x : ℤ
⊢ fourierCoeff (f + g) x = (fourierCoeff f + fourierCoeff g) x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ (fourier n) ↑y) (2 * ↑π * I * ↑n / ↑T * (fourier n) ↑x) x

Tactic:
by
  simp_rw [fourier_coe_apply]
  refine (?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal
  rw [(fun α β => by ring : ∀ α β : ℂ, α * exp β = exp β * α)]
  refine (hasDerivAt_exp _).comp (x : ℂ) ?_
  convert! hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1
  ext1 y; ring

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✝ : ProperSpace E
f : 𝓢(E, F)
⊢ Tendsto (fun x ↦ ‖x‖ ^ (-1)) (cocompact E) (𝓝 0)

Tactic:
simp_rw [Real.rpow_neg_one]

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : ProperSpace E
f : 𝓢(E, F)
⊢ Tendsto (fun x ↦ ‖x‖⁻¹) (cocompact E) (𝓝 0)
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✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (c • ⇑f)

Tactic:
exact (f.smooth _).const_smul c

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✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : ℕ
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (c • ⇑f)

Tactic:
exact (f.smooth _).const_smul c

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✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : ℤ
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (c • ⇑f)

Tactic:
exact (f.smooth _).const_smul c

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
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun i ↦
    ((smulRightL ℝ (fun x ↦ W) E)
        ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x ↦ L i))
      (f i)

Tactic:
apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp₂ _ hf

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
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun w ↦
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x ↦ L w
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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ (smulLeftCLM F g₁) ((smulLeftCLM F g₂) f) = (smulLeftCLM F (g₁ * g₂)) f

Tactic:
ext x

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
x : E
⊢ ((smulLeftCLM F g₁) ((smulLeftCLM F g₂) f)) x = ((smulLeftCLM F (g₁ * g₂)) f) x
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
𝕜' : Type u_10
inst✝¹ : RCLike 𝕜'
inst✝ : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ (smulLeftCLM F fun x ↦ ↑(g x)) f = (smulLeftCLM F g) f

Tactic:
ext x

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
𝕜' : Type u_10
inst✝¹ : RCLike 𝕜'
inst✝ : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ ((smulLeftCLM F fun x ↦ ↑(g x)) f) x = ((smulLeftCLM F g) f) x
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case hbc
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
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ n.descFactorial i ≤ (n + 1) ^ k

Tactic:
calc n.descFactorial i ≤ n ^ i := Nat.descFactorial_le_pow _ _
      _ ≤ (n + 1) ^ i := by gcongr; lia
      _ ≤ (n + 1) ^ k := by gcongr; exacts [le_add_self, Finset.mem_range_succ_iff.mp hi]

Goal state after:
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:
← sub_eq_add_neg,

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₀) w - (L v) w)) • f v
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedSpace 𝕜 F
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra ℝ 𝕜'
inst✝ : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
⊢ (smulLeftCLM F u) ((compCLMOfContinuousLinearEquiv 𝕜 g) f) =
    (compCLMOfContinuousLinearEquiv 𝕜 g) ((smulLeftCLM F (u ∘ ⇑g.symm)) f)

Tactic:
ext x

Goal state after:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedSpace 𝕜 F
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra ℝ 𝕜'
inst✝ : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
⊢ ((smulLeftCLM F u) ((compCLMOfContinuousLinearEquiv 𝕜 g) f)) x =
    ((compCLMOfContinuousLinearEquiv 𝕜 g) ((smulLeftCLM F (u ∘ ⇑g.symm)) f)) 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✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b : E
⊢ (compSubConstCLM 𝕜 b) ((compSubConstCLM 𝕜 a) f) = (compSubConstCLM 𝕜 (a + b)) f

Tactic:
ext x

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✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
⊢ ((compSubConstCLM 𝕜 b) ((compSubConstCLM 𝕜 a) f)) x = ((compSubConstCLM 𝕜 (a + b)) f) x
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
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
w : W
m : ℕ
hm : ↑m ≤ N
⊢ Integrable (iteratedFDeriv ℝ m fun v ↦ fourierPowSMulRight L f v k) μ

Tactic:
have I : Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ := by
      apply integrable_finsetSum _ (fun p hp ↦ ?_)
      simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
      exact h'f _ _ ((Nat.cast_le.2 hp.1).trans hk) ((Nat.cast_le.2 hp.2).trans hm)

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
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
w : W
m : ℕ
hm : ↑m ≤ N
I : Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
⊢ Integrable (iteratedFDeriv ℝ m fun v ↦ fourierPowSMulRight L f v k) μ
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_5
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ ∫ (v : V), ↑(𝐞 (-(L v) w)) • f v ∂μ = ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ

Tactic:
Real.fourierChar_apply,

Goal state after:
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_5
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ ∫ (v : V), Complex.exp (↑(2 * π * -(L v) w) * Complex.I) • f v ∂μ =
    ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ ∫ (v : V), ↑(𝐞 (-⟪v, w⟫)) • f v = ∫ (v : V), Complex.exp (↑(-2 * π * ⟪v, w⟫) * Complex.I) • f v

Tactic:
Real.fourierChar_apply,

Goal state after:
V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ ∫ (v : V), Complex.exp (↑(2 * π * -⟪v, w⟫) * Complex.I) • f v =
    ∫ (v : V), Complex.exp (↑(-2 * π * ⟪v, w⟫) * Complex.I) • f v
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k : ℕ
hk : ↑k ≤ K
w : V
hn : ↑0 ≤ N
Z :
  ‖w‖ ^ 0 * (‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ 0 *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ 0 *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ 0 *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
hn : n ≠ 0
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ ∫ (v : ℝ), ↑(𝐞 (-(v * w))) • f v = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
Real.fourierChar_apply,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ ∫ (v : ℝ), Complex.exp (↑(2 * π * -(v * w)) * Complex.I) • f v =
    ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v