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

Goal state before:
pp: case succ
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ (k + 1))

Tactic:
pow_succ

Goal state after:
case succ
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ k * f)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case succ
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ (k + 1))

Tactic:
rw [pow_succ]; fun_prop

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

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
⊢ x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)

Tactic:
have : 0 ≤ C₂ := le_trans (by positivity) h₂

Goal state after:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this : 0 ≤ C₂
⊢ x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : E), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)

Tactic:
rw [← integral_const_mul, ← integral_mul_const]

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ ∫ (a : E), 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂) ∂μ
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: case mp
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
⊢ HasEigenvalue (↑T) μ → μ ∈ spectrum 𝕜 T

Tactic:
intro hμ'

Goal state after:
case mp
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T) μ
⊢ μ ∈ spectrum 𝕜 T
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ OrthogonalFamily 𝕜 (fun μ ↦ ↥(eigenspace T μ)) fun μ ↦ (eigenspace T μ).subtypeₗᵢ

Tactic:
rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
⊢ ⟪((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩, ((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩⟫ = 0
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
g : C^↑n⟮I, M; 𝓘(ℝ, F), F⟯
g_approx : ∀ (x : M), dist (g x) (f x) < ε x
g_supp : support ⇑g ⊆ support f
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ support ⇑g ⊆ support f

Tactic:
exact ⟨g, g_approx, g_supp⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
s t : Set α
inst✝ : CompleteSpace E
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
⊢ μ.real (t ∩ s) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫

Tactic:
Set.inter_comm

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
s t : Set α
inst✝ : CompleteSpace E
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
⊢ μ.real (s ∩ t) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ ⟪(BoundedContinuousFunction.toLp 2 μ 𝕜) f, (BoundedContinuousFunction.toLp 2 μ 𝕜) g⟫ =
    ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
apply integral_congr_ae

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a ↦ ⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a⟫) =ᵐ[μ]
    fun a ↦ g a * (starRingEnd 𝕜) (f a)
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ ⟪(BoundedContinuousFunction.toLp 2 μ 𝕜) f, (BoundedContinuousFunction.toLp 2 μ 𝕜) g⟫ =
    ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
apply integral_congr_ae
  have hf_ae := f.coeFn_toLp 2 μ 𝕜
  have hg_ae := g.coeFn_toLp 2 μ 𝕜
  filter_upwards [hf_ae, hg_ae] with _ hf hg
  rw [hf, hg]
  simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ ⟪(ContinuousMap.toLp 2 μ 𝕜) f, (ContinuousMap.toLp 2 μ 𝕜) g⟫ = ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
apply integral_congr_ae

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ (fun a ↦ ⟪↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a, ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a⟫) =ᵐ[μ] fun a ↦
    g a * (starRingEnd 𝕜) (f a)
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ENNReal.ofReal ε' * ENNReal.ofReal ((μ (tsupport f)).toReal ^ (1 / p.toReal)) ≤ ENNReal.ofReal ε

Tactic:
← ofReal_mul hε'.le,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ENNReal.ofReal (ε' * (μ (tsupport f)).toReal ^ (1 / p.toReal)) ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal) + 1 / p.toReal) ≤ ε

Tactic:
neg_add_cancel,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ε * (μ (tsupport f)).toReal ^ 0 ≤ ε
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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
f_bd : IsBounded (range f)
g_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
g_bd : IsBounded (range g)
f' : α →ᵇ E := { toFun := f, continuous_toFun := f_cont, map_bounded' := ⋯ }
⊢ IsBounded (range (f + g))

Tactic:
let g' : α →ᵇ E := ⟨⟨g, g_cont⟩, Metric.isBounded_range_iff.1 g_bd⟩

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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
f_bd : IsBounded (range f)
g_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
g_bd : IsBounded (range g)
f' : α →ᵇ E := { toFun := f, continuous_toFun := f_cont, map_bounded' := ⋯ }
g' : α →ᵇ E := { toFun := g, continuous_toFun := g_cont, map_bounded' := ⋯ }
⊢ IsBounded (range (f + g))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i

Tactic:
apply integral_congr_ae

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ (fun a ↦ (starRingEnd ℂ) (↑↑(fourierLp 2 i) a) * ↑↑f a) =ᵐ[haarAddCircle] fun a ↦ (fourier (-i)) a • ↑↑f a
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ ∫ (t : AddCircle (b - a)), ‖liftIoc (b - a) a f t‖ ^ 2 ∂haarAddCircle =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle

Tactic:
apply integral_congr_ae

Goal state after:
case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (fun a_1 ↦ ‖liftIoc (b - a) a f a_1‖ ^ 2) =ᵐ[haarAddCircle] fun a_1 ↦ ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) a_1‖ ^ 2
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
⊢ ∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε

Tactic:
filter_upwards [this] with i hi

Goal state after:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
i : ι
hi : ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
⊢ dist (∫ (x : α) in s, φ i x • g x ∂μ) 0 < ε
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
v : V
⊢ 2 * π * ‖L v‖ * ‖f v‖ ≤ 2 * π * (‖L‖ * ‖v‖) * ‖f v‖

Tactic:
gcongr; exact L.le_opNorm _

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
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
⊢ ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v

Tactic:
filter_upwards with v w' _

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✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
a✝ : w' ∈ Metric.ball w 1
⊢ ‖F' w' v‖ ≤ B v
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc
ι : 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
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
⊢ ∑ i ∈ Finset.range (n + 1), ‖x‖ ^ k * (↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖) ≤
    ∑ i ∈ Finset.range (n + 1),
      1 * (↑(n.choose (n / 2)) * C * 2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f)

Tactic:
refine Finset.sum_le_sum fun i hi => ?_

Goal state after:
case hbc
ι : 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
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ‖x‖ ^ k * (↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖) ≤
    1 * (↑(n.choose (n / 2)) * C * 2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f)
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
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f₁ f₂ : V → E
hf : f₁ =ᵐ[μ] f₂
x✝ : W
⊢ fourierIntegral e μ L f₁ x✝ = fourierIntegral e μ L f₂ x✝

Tactic:
apply integral_congr_ae

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
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f₁ f₂ : V → E
hf : f₁ =ᵐ[μ] f₂
x✝ : W
⊢ (fun a ↦ e (-(L a) x✝) • f₁ a) =ᵐ[μ] fun a ↦ e (-(L a) x✝) • f₂ a
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hab
ι : 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
⊢ 1 + ‖x‖ ≤ 1 * (1 + ‖g x‖) ^ kg + Cg * (1 + ‖g x‖) ^ kg

Tactic:
refine add_le_add ?_ (hg_upper' x)

Goal state after:
case hab
ι : 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
⊢ 1 ≤ 1 * (1 + ‖g x‖) ^ kg
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) μ
v : V
⊢ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)

Tactic:
pow_succ

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) μ
v : V
⊢ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) = (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖v‖ * ‖f v‖)