mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
w : Set E
hws : w ⊇ s
hw_ortho : Orthonormal 𝕜 Subtype.val
hw_max : ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
⊢ (span 𝕜 (Set.range Subtype.val))ᗮ = ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
w : Set E
hws : w ⊇ s
hw_ortho : Orthonormal 𝕜 Subtype.val
hw_max : ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
⊢ (span 𝕜 w)ᗮ = ⊥
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:
simpa using

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ (starRingEnd ℂ) (cexp (2 * ↑π * I * ↑n * ↑y / ↑T)))
    (-(2 * ↑π * I * ↑n) / ↑T * (starRingEnd ℂ) (cexp (2 * ↑π * I * ↑n * ↑x / ↑T))) x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
div_div_eq_mul_div

Goal state after:
case e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y * ↑T / (-2 * ↑π * I * ↑n)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ ↑b = ↑a

Tactic:
simpa using

Goal state after:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ ↑b = ↑a
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 α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ 1

Tactic:
simpa using

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 α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ 1
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case hbc
α : 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
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ δ

Tactic:
simpa using

Goal state after:
case hbc
α : 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
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ δ
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: x : ℝ
h1 : ∀ (y : ℝ), ↑(𝐞 y) = (fourier 1) ↑y
⊢ HasDerivAt (fun x ↦ ↑(𝐞 x)) (2 * ↑π * I * ↑(𝐞 x)) x

Tactic:
simpa using

Goal state after:
x : ℝ
h1 : ∀ (y : ℝ), ↑(𝐞 y) = (fourier 1) ↑y
⊢ HasDerivAt (fun x ↦ (fourier 1) ↑x) (2 * ↑π * I * (fourier 1) ↑x) 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
f : 𝓢(E, F)
inst✝ : ProperSpace E
k : ℤ
⊢ ⇑f =O[cocompact E] fun x ↦ ‖x‖ ^ k

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
k : ℤ
⊢ ⇑f =O[cocompact E] fun x ↦ ‖x‖ ^ k
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) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ Integrable B μ

Tactic:
simpa using

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) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ Integrable B μ
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₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (univ \ u)

Tactic:
simpa using

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₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
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
f : 𝓢(E, F)
n : ℕ
C : ℝ
Cpos : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ 0

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
Cpos : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 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✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (fun x ↦ (f x) m) x‖ ≤ ‖x‖ ^ k * (‖m‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖)

Tactic:
by
      gcongr
      exact norm_iteratedFDeriv_clm_apply_const (f.smooth _).contDiffAt le_rfl

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

Goal state before:
pp: case pos
𝕜 : 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 : E → 𝕜
f : 𝓢(E, F)
hg : Function.HasTemperateGrowth g
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

Tactic:
simpa using

Goal state after:
case pos
𝕜 : 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 : E → 𝕜
f : 𝓢(E, F)
hg : Function.HasTemperateGrowth g
⊢ (tsupport fun x ↦ g x • f x) ⊆ tsupport ⇑f ∧ (tsupport fun x ↦ g x • f x) ⊆ tsupport g
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[ℝ] ℝ
c : 𝕜
g : 𝓢(E, F)
x : E
v : G
⊢ ((L x).smulRight ((c • g) x)) v = ((RingHom.id 𝕜) c • (L x).smulRight (g x)) v

Tactic:
simpa using

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[ℝ] ℝ
c : 𝕜
g : 𝓢(E, F)
x : E
v : G
⊢ (L x) v • c • g x = c • (L x) v • g x
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[ℝ] ℝ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) +
      ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) =
    2 * ‖L‖ * ↑(max 1 n) * ({(k + 1, n), (k, n - 1)}.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
by
          simp only [Finset.sup_insert, schwartzSeminormFamily_apply, Finset.sup_singleton,
            Seminorm.coe_sup, Pi.sup_apply]
          ring

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

Goal state before:
pp: case h₂
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure[inst✝⁷] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
u : Set α
u_open : IsOpen[inst✝⁷] u
x₀_u : x₀ ∈ u
⊢ interior s ⊆ s

Tactic:
apply interior_subset

Goal state after:
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
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
x : F
hx : M < ‖x‖ ∧ 1 < ‖x‖
⊢ x ∈ (closedBall 0 M)ᶜ

Tactic:
simpa using

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
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
x : F
hx : M < ‖x‖ ∧ 1 < ‖x‖
⊢ M < ‖x‖
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✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
x : D
⊢ (1 + ‖x‖) ^ n * ‖f x‖ ≤ 2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f

Tactic:
simpa using

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✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
x : D
⊢ (1 + ‖x‖) ^ n * ‖f x‖ ≤ 2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f
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✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' : ∀ (x : D), ‖f x‖ ≤ (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)
⊢ Integrable (fun i ↦ ‖f i‖) μ

Tactic:
simpa using

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✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' : ∀ (x : D), ‖f x‖ ≤ (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)
⊢ Integrable (fun i ↦ ‖f i‖) μ
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 ν
⊢ ∫ (ξ : W), ∫ (x : V), (M (g ξ)) (e (-(L x) ξ) • f x) ∂μ ∂ν =
    ∫ (x : V), ∫ (ξ : W), (M (g ξ)) (e (-(L x) ξ) • f x) ∂ν ∂μ

Tactic:
by
  rw [integral_integral_swap]
  have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
    (hg.norm.mul_prod hf.norm).const_mul _
  apply this.mono
  · change AEStronglyMeasurable (fun p : W × V ↦ (M (g p.1) (e (-(L p.2) p.1) • f p.2))) _
    have A : AEStronglyMeasurable (fun (p : W × V) ↦ e (-L p.2 p.1) • f p.2) (ν.prod μ) := by
      refine (Continuous.aestronglyMeasurable ?_).fun_smul hf.1.comp_snd
      exact he.comp (hL.comp continuous_swap).neg
    have A' : AEStronglyMeasurable (fun p ↦ (g p.1, e (-(L p.2) p.1) • f p.2) : W × V → F × E)
      (Measure.prod ν μ) := hg.1.comp_fst.prodMk A
    have hM : Continuous (fun q ↦ M q.1 q.2 : F × E → G) :=
      -- There is no `Continuous.clm_apply` for semilinear continuous maps
      (M.flip.cont.comp continuous_snd).clm_apply continuous_fst
    apply hM.comp_aestronglyMeasurable A' -- `exact` works, but `apply` is 10x faster!
  · filter_upwards with ⟨ξ, x⟩
    simp only [Function.uncurry_apply_pair, norm_mul, norm_norm, ge_iff_le, ← mul_assoc]
    convert! M.le_opNorm₂ (g ξ) (e (-L x ξ) • f x) using 2
    simp

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✝¹ : 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
k : ℕ
hk : ↑k ≤ K
⊢ Integrable (fun v ↦ ‖v‖ ^ k * ‖f v‖) μ

Tactic:
simpa using

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
k : ℕ
hk : ↑k ≤ K
⊢ Integrable (fun v ↦ ‖v‖ ^ k * ‖f v‖) μ