mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ √(1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖

Tactic:
by
  rw [sqrt_le_left (by positivity)]
  simp [add_sq]

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

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✝
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
this : F =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
C : ℝ
C_nonneg : C ≥ 0
hC : ∀ (x : E) (i : ℕ) (h : i ≤ n), ‖F x ⟨i, ⋯⟩‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
exact ⟨k, C, C_nonneg, fun N hN x ↦ hC x N hN⟩

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := ⋯
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
⊢ ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n (fun x ↦ x ^ r) t x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
intro N

Goal state after:
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N : ℕ
⊢ ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n (fun x ↦ x ^ r) t x‖ ≤ C * (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case pos
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
⊢ |x| ^ (r - ↑n) ≤ (1 + |x|) ^ k

Tactic:
have : r - n ≤ k := by simpa using hk₁.trans (by simp)
    rw [← Real.rpow_natCast]
    exact (Real.rpow_le_rpow (by positivity) (by simp) h).trans
      (Real.rpow_le_rpow_of_exponent_le (by simp) this)

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

Goal state before:
pp: case coe
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
⊢ ∃ k, eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ∞

Tactic:
| coe p =>

Goal state after:
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
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
this :
  ∀ (w : PiLp 2 fun μ ↦ ↥(eigenspace T (↑T 1 μ))),
    T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ ↦ ↑T 1 μ • w.ofLp μ)
⊢ (hT.diagonalization (T v)).ofLp μ = ↑T 1 μ • (hT.diagonalization v).ofLp μ

Tactic:
by
    simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
      congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ { toFun := ⇑T ∘ ⇑(c • f), contDiff' := ⋯, zero_on_compl' := ⋯ } x =
    ((RingHom.id 𝕜) c • { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ }) x

Tactic:
exact map_smul T c (f x)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
⊢ ∀ (g : n → 𝕜), ∑ i, g i • v i = 0 → ∀ (i : n), g i = 0

Tactic:
intro y hy

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
y : n → 𝕜
hy : ∑ i, y i • v i = 0
⊢ ∀ (i : n), y i = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ abs a ^ (2 * x) = (star a * a) ^ x

Tactic:
rw [← nnrpow_nnrpow, abs_nnrpow_two]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
simp (discharger := positivity) only [ContDiffMapSupportedIn.seminorm_le_iff, monoLM_apply, H,
      and_self, ↓reduceIte]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ ↑i ≤ n₂ → ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ ↑i ≤ n₂ → ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
intro hik _ _

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
hik : ↑i ≤ n₂
x✝ : E
a✝ : x✝ ∈ K₂
⊢ ‖iteratedFDeriv ℝ i (⇑f) x✝‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
x✝¹ x✝ : ↥(Lp E 2 μ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_rw [inner_def, ← integral_conj, inner_conj_symm]

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₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = ∫ (x : E) in ↑K, (B (f x)) (φ x) ∂μ

Tactic:
by
  rw [integralAgainstBilinLM_eq_integral hφ, setIntegral_eq_integral_of_forall_compl_eq_zero]
  intro x hx
  rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, zero_apply]

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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
g : α → E
hg : eLpNorm (f - g) p μ ≤ ε
g_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
g_bd : IsBounded (range g)
⊢ ∃ g, eLpNorm (f - ⇑g) p μ ≤ ε ∧ MemLp (⇑g) p μ

Tactic:
exact ⟨⟨⟨g, g_cont⟩, Metric.isBounded_range_iff.1 g_bd⟩, hg, g_mem⟩

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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
⊢ (succSub D.P i) (D.e j) = Pi.single j 1 i • D.e i

Tactic:
← hx,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
⊢ (succSub D.P i) ((succSub D.P j) x) = Pi.single j 1 i • D.e i
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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(W₀.sum fun a b ↦ hV.linearIsometryEquiv ((V a) b)) = ⇑W₀

Tactic:
← map_dfinsuppSum

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(hV.linearIsometryEquiv (W₀.sum fun a ↦ ⇑(V a))) = ⇑W₀
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : ↑x.toCircle = ↑y.toCircle
⊢ x = y

Tactic:
rw [Subtype.coe_inj] at hxy

Goal state after:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x.toCircle = y.toCircle
⊢ x = y
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 : ι → E
hv : Orthonormal 𝕜 v
hsp : (span 𝕜 (Set.range v))ᗮ = ⊥
⊢ ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure

Tactic:
rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]

Goal state after:
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 μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
⊢ IntegrableOn (fun x ↦ φ i x • g x) s μ

Tactic:
have B : IntegrableOn (fun x => φ i x • g x) (s ∩ u) μ := by
    apply Integrable.smul_of_top_left
    · exact IntegrableOn.mono_set I ut
    · apply
        memLp_top_of_bound (hmg.mono_set inter_subset_left).aestronglyMeasurable (‖a‖ + 1)
      filter_upwards [self_mem_ae_restrict (hs.inter u_open.measurableSet)] with x hx
      rw [inter_comm] at hx
      exact (norm_lt_of_mem_ball (hu x hx)).le

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 μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
B : IntegrableOn (fun x ↦ φ i x • g x) (s ∩ u) μ
⊢ IntegrableOn (fun x ↦ φ i x • g x) s μ
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).smulRight (f v)‖ = 2 * π * ‖L v‖ * ‖f v‖

Tactic:
Complex.norm_of_nonneg pi_pos.le,

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
v : V
⊢ ‖2‖ * π * ‖(L v).smulRight (f v)‖ = 2 * π * ‖L v‖ * ‖f v‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]

Goal state after:
case hbc
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x + iteratedFDeriv ℝ n (⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case ha
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[ℝ] ℝ := ⋯
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)
⊢ 1 ≤ n + 1

pp: case hmn
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[ℝ] ℝ := ⋯
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)
⊢ i ≤ k

Tactic:
exacts [le_add_self, Finset.mem_range_succ_iff.mp hi]

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

Goal state before:
pp: case right
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑L ∘ ⇑f) x‖ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
calc
    _ = ‖x‖ ^ k * ‖(L.restrictScalars ℝ).compContinuousMultilinearMap
        (iteratedFDeriv ℝ n f x)‖ := by
      congr
      exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)
    _ ≤ ‖x‖ ^ k * (‖L‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le
    _ = ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by ring
    _ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f := by
      grw [le_seminorm 𝕜 k n f x]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ ∫ (x : V), ∫ (ξ : W), (M.flip (g ξ)) (e (-(L x) ξ) • f x) ∂ν ∂μ =
    ∫ (x : V), ∫ (ξ : W), (M (f x)) (e ((L.flip ξ) x) • g ξ) ∂ν ∂μ

Tactic:
by
    congr with x
    congr with ξ
    rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]
    simp only [map_smulₛₗ, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, RingHom.id_apply,
      Circle.smul_def, smul_eq_mul, mul_one, ← Circle.coe_inv_eq_conj, AddChar.map_neg_eq_inv,
      inv_inv]

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
v : V
w : W
⊢ 1 ≤ 2 * π

Tactic:
linarith [one_le_pi_div_two]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ a ∈ s, ‖f (a, x)‖ ≤ C * ‖g x‖

Tactic:
intro y hy

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ ‖𝓕 (↑↑f) x‖ ≤ ‖f‖

Tactic:
by
    rw [Real.fourier_eq]
    apply (norm_integral_le_integral_norm _).trans
    simp_rw [Circle.norm_smul]
    exact (L1.norm_eq_integral_norm f).symm.le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x)) * ↑x ^ (s - 1)‖

Tactic:
rw [norm_mul, Complex.norm_of_nonneg <| le_of_lt <| exp_pos <| -x,
      norm_cpow_eq_rpow_re_of_pos hx _]

Goal state after:
case right
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re