mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : ↥(Lp E 2 μ)
⊢ ∫ (a : α), ⟪↑↑f a, ↑↑f a⟫ ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal

Tactic:
simp_rw [inner_self_eq_norm_sq_to_K]
  norm_cast
  rw [integral_eq_lintegral_of_nonneg_ae]
  rotate_left
  · exact Filter.Eventually.of_forall fun x => sq_nonneg _
  · exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable
  congr
  ext1 x
  have h_two : (2 : ℝ) = ((2 : ℕ) : ℝ) := by simp
  rw [← Real.rpow_natCast _ 2, ← h_two, ←
    ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) zero_le_two, ofReal_norm]
  norm_cast

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : CompleteSpace A
⊢ Continuous fun a ↦ star a * a

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁶ : NormedAddCommGroup F₁
inst✝⁵ : NormedSpace 𝕜 F₁
inst✝⁴ : NormedSpace ℝ F₁
inst✝³ : NormedAddCommGroup F₂
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedAddCommGroup F₃
inst✝ : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (↑K) μ
⊢ (support fun x ↦ (B (f x)) (φ x)) ⊆ support ⇑f

Tactic:
exact fun x hx hfx ↦ hx (by simp [hfx])

Goal state after:
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
⊢ Continuous fun x ↦ ε

Tactic:
by fun_prop

Goal state after:
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 < ε'
hε₂ : ENNReal.ofReal ε' * μ (tsupport f) ^ (1 / p.toReal) ≤ ENNReal.ofReal ε
⊢ Continuous fun x ↦ ε'

Tactic:
by fun_prop

Goal state after:
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‖
x : α
hx : x ∉ v
⊢ g x • c = 0

Tactic:
simp only [hgv hx, Pi.zero_apply, zero_smul]

Goal state after:
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
gc_mem : MemLp (fun x ↦ g x • c) p μ
⊢ Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ g x • c

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
⊢ ∑ i ∈ B ∩ A, (b.coord i) x • ↑b i = ∑ i ∈ A ∩ B, (b.coord i) x • ↑b i

Tactic:
congr 1

Goal state after:
case e_s
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
⊢ B ∩ A = A ∩ B
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),
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ IsBounded (range f) →
      Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g) →
        Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f + g) ∧
          MemLp (f + g) p μ ∧ IsBounded (range (f + g))

Tactic:
rintro f g ⟨f_cont, f_mem, f_bd⟩ ⟨g_cont, g_mem, g_bd⟩
    refine ⟨f_cont.add g_cont, f_mem.add g_mem, ?_⟩
    let f' : α →ᵇ E := ⟨⟨f, f_cont⟩, Metric.isBounded_range_iff.1 f_bd⟩
    let g' : α →ᵇ E := ⟨⟨g, g_cont⟩, Metric.isBounded_range_iff.1 g_bd⟩
    exact (f' + g').isBounded_range

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
congr 1

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ 2 * ↑π / ↑T * (↑n * ↑x) * Complex.I = 2 * ↑π * Complex.I * ↑n * ↑x / ↑T
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 : IsHilbertSum 𝕜 G V
w : ↥(lp G 2)
⊢ hV.linearIsometryEquiv.symm w = ∑' (i : ι), (V i) (↑w i)

Tactic:
by
  simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
congr 1

Goal state after:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + (b - a))

Tactic:
rwa [add_sub, add_sub_cancel_left]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
congr 1

Goal state after:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
congr 1

Goal state after:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
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)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a)) -
      1 / ↑(b - a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a) -
      1 / (-2 * ↑π * I * ↑n) * (↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))

Tactic:
congr 1

Goal state after:
case e_a
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)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a)) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a)

case e_a
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)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x) =
    1 / (-2 * ↑π * I * ↑n) * (↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑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)
k : ℕ
⊢ ⇑f =O[cocompact E] fun x ↦ ‖x‖ ^ (-↑k)

Tactic:
obtain ⟨d, _, hd'⟩ := f.decay k 0

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)
k : ℕ
d : ℝ
left✝ : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ d
⊢ ⇑f =O[cocompact E] fun x ↦ ‖x‖ ^ (-↑k)
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)
k : ℕ
⊢ ⇑f =O[cocompact E] fun x ↦ ‖x‖ ^ (-↑k)

Tactic:
by
  obtain ⟨d, _, hd'⟩ := f.decay k 0
  simp only [norm_iteratedFDeriv_zero] at hd'
  simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]
  refine ⟨d, Filter.Eventually.filter_mono Filter.cocompact_le_cofinite ?_⟩
  refine (Filter.eventually_cofinite_ne 0).mono fun x hx ↦ ?_
  rw [Real.norm_of_nonneg (by positivity), zpow_neg, ← div_eq_mul_inv, le_div_iff₀' (by positivity)]
  exact hd' x

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)
⊢ ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ ≤ C

Tactic:
by simpa [← Nat.cast_smul_eq_nsmul ℝ] using! ((c : ℝ) • f).decay'

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
⊢ HasFDerivAt (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fourierSMulRight L f) w) w

Tactic:
let F : W → V → E := fun w' v ↦ 𝐞 (-L v w') • f v
  let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • fourierSMulRight L f v
  let B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
  have h0 (w' : W) : Integrable (F w') μ :=
    (fourierIntegral_convergent_iff continuous_fourierChar
      (by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₁₂ p.1 p.2)) w').2 hf
  have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ :=
    Eventually.of_forall (fun w' ↦ (h0 w').aestronglyMeasurable)
  have h3 : AEStronglyMeasurable (F' w) μ := by
    refine .fun_smul ?_ hf.1.fourierSMulRight
    refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
    fun_prop
  have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by
    filter_upwards with v w' _
    rw [Circle.norm_smul _ (fourierSMulRight L f v)]
    exact norm_fourierSMulRight_le L f v
  have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
  have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=
    ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourierChar_smul L f v w')
  exact hasFDerivAt_integral_of_dominated_of_fderiv_le (Metric.ball_mem_nhds _ one_pos) h1 (h0 w)
    h3 h4 h5 h6

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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : E → ℝ := fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖
⊢ Continuous fun x ↦ ‖x‖ ^ k

Tactic:
by fun_prop

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

Tactic:
by fun_prop

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
𝕜' : Type u_10
inst✝¹ : RCLike 𝕜'
inst✝ : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ Function.HasTemperateGrowth g

Tactic:
by fun_prop

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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
⊢ ∀ (f : 𝓢(E, F)), ContDiff ℝ ∞ fun x ↦ (L x).smulRight (f x)

Tactic:
by fun_prop

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✝⁶ : 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
⊢ ContDiff ℝ ∞ ⇑L

Tactic:
by fun_prop

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✝⁶ : 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
⊢ ‖x‖ ^ k * ‖L x‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ↑n * ‖L‖ * ‖iteratedFDeriv ℝ (n - 1) (⇑f) x‖ ≤
    ‖L‖ * 1 * (SchwartzMap.seminorm 𝕜 (k + 1) n) f + ‖L‖ * ↑n * (SchwartzMap.seminorm 𝕜 k (n - 1)) f

Tactic:
by
          grw [le_opNorm, ← le_seminorm 𝕜 (k + 1) n f x, ← le_seminorm 𝕜 k (n - 1) f x]
          apply le_of_eq
          ring

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

Goal state before:
pp: case hf.hf
𝕜 : 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 μ)
⊢ AEStronglyMeasurable (Function.uncurry fun ξ x ↦ (M (g ξ)) (e (-(L x) ξ) • f x)) (ν.prod μ)

Tactic:
change AEStronglyMeasurable (fun p : W × V ↦ (M (g p.1) (e (-(L p.2) p.1) • f p.2))) _

Goal state after:
case hf.hf
𝕜 : 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 μ)
⊢ AEStronglyMeasurable (fun p ↦ (M (g p.1)) (e (-(L p.2) p.1) • f p.2)) (ν.prod μ)
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
a : E
⊢ Function.HasTemperateGrowth fun x ↦ x - a

Tactic:
by fun_prop

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)
a b x : E
⊢ f (x - b - a) = f (x - (a + b))

Tactic:
congr 1

Goal state after:
case e_6
𝕜 : 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
⊢ x - b - a = x - (a + b)