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

Goal state before:
pp: case pos
𝕜 : 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
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₂
f g : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (B (f x)) (φ x) + (B (g x)) (φ x) ∂μ = ∫ (x : E), (B (f x)) (φ x) ∂μ + ∫ (x : E), (B (g x)) (φ x) ∂μ

Tactic:
integral_add (f.integrable_bilin B hφ) (g.integrable_bilin B hφ)

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₁)
x : E
hx : x ∉ ↑K
⊢ 0 (φ x) = 0

Tactic:
zero_apply

Goal state after:
𝕜 : 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₁)
x : E
hx : x ∉ ↑K
⊢ 0 = 0
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case neg.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : ¬i = j
h' : i > j
⊢ (P (j + 1)) x - (P j.succ) x - ((P (min (i + 1) j)) x - (P j) x) = 0

Tactic:
min_eq_right_of_lt (Nat.lt_succ_of_lt h')

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : ¬i = j
h' : i > j
⊢ (P (j + 1)) x - (P j.succ) x - ((P j) x - (P j) x) = 0
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: case hf
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : MeasurableSpace D
μ : Measure D
inst✝² : BorelSpace D
inst✝¹ : FiniteDimensional ℝ D
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ ∀ x ∈ tsupport ⇑g, HasLineDerivAt ℝ (⇑f) ((∂_{v} f) x) x v

Tactic:
exact fun x _ ↦ (hasFDerivAt _ x).hasLineDerivAt v

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

Goal state before:
pp: case hg
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : MeasurableSpace D
μ : Measure D
inst✝² : BorelSpace D
inst✝¹ : FiniteDimensional ℝ D
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ ∀ x ∈ tsupport ⇑f, HasLineDerivAt ℝ (⇑g) ((∂_{v} g) x) x v

Tactic:
exact fun x _ ↦ (hasFDerivAt _ x).hasLineDerivAt v

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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ (P n) x = 0

Tactic:
rw [← hy, ContinuousLinearMap.coe_coe]; simp [succSub, map_sub, hcomp]

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✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ MemLp.toLp (⇑g) g_mem ∈ Metric.closedEBall f ε

Tactic:
Metric.mem_closedEBall',

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✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ edist f (MemLp.toLp (⇑g) g_mem) ≤ ε
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this✝¹ : FiniteDimensional 𝕜 ↥W
this✝ : FiniteDimensional 𝕜 ↥U
this : FiniteDimensional 𝕜 ↥V
h_dim : Module.finrank 𝕜 ↥W = Module.finrank 𝕜 ↥U + Module.finrank 𝕜 ↥V
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1

Tactic:
hrank,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this✝¹ : FiniteDimensional 𝕜 ↥W
this✝ : FiniteDimensional 𝕜 ↥U
this : FiniteDimensional 𝕜 ↥V
h_dim : n + 1 = Module.finrank 𝕜 ↥U + Module.finrank 𝕜 ↥V
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this✝¹ : FiniteDimensional 𝕜 ↥W
this✝ : FiniteDimensional 𝕜 ↥U
this : FiniteDimensional 𝕜 ↥V
h_dim : n + 1 = Module.finrank 𝕜 ↥U + Module.finrank 𝕜 ↥V
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1

Tactic:
hrank,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this✝¹ : FiniteDimensional 𝕜 ↥W
this✝ : FiniteDimensional 𝕜 ↥U
this : FiniteDimensional 𝕜 ↥V
h_dim : n + 1 = Module.finrank 𝕜 ↥U + n
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(-n • ↑z✝).toCircle = (starRingEnd ℂ) ↑(n • ↑z✝).toCircle

Tactic:
toCircle

Goal state after:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift (-n • ↑z✝)) = (starRingEnd ℂ) ↑(⋯.lift (n • ↑z✝))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑((m + n) • x).toCircle = (fourier m) x * (fourier n) x

Tactic:
by
  rw [← fourier_apply]; exact fourier_add

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
⊢ (span ℂ (range (fourierLp p))).topologicalClosure = ⊤

Tactic:
convert!
    (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
      span_fourier_closure_eq_top

Goal state after:
case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (range (fourierLp p)) = Submodule.map (↑(toLp p haarAddCircle ℂ)) (span ℂ (range fourier))
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)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun x ↦ 𝕜) 2)
h : (fun b i ↦ b.repr.symm (lp.single 2 i 1)) { repr := b₁ } = (fun b i ↦ b.repr.symm (lp.single 2 i 1)) { repr := b₂ }
⊢ { repr := b₁ } = { repr := b₂ }

Tactic:
congr
    apply LinearIsometryEquiv.symm_bijective.injective
    apply LinearIsometryEquiv.toContinuousLinearEquiv_injective
    apply ContinuousLinearEquiv.coe_injective
    refine lp.ext_continuousLinearMap (ENNReal.ofNat_ne_top (n := nat_lit 2)) fun i => ?_
    ext
    exact congr_fun h i

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
c : ℂ
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n

Tactic:
apply fourierCoeff.const_smul

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 α
φ : ι → α → ℝ
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, IsOpen[inst✝³] u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball 0 δ

Tactic:
rcases mem_nhdsWithin.1 (Filter.inter_mem h'ts (hcg (ball_mem_nhds _ δpos)))
      with ⟨u, u_open, x₀u, hu⟩
    refine ⟨u, u_open, x₀u, ?_, hu.trans inter_subset_right⟩
    rw [inter_comm]
    exact hu.trans inter_subset_left

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

Goal state before:
pp: case hab
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
m : ℕ
this : ‖T‖ ≤ 1
x✝ : Fin n
⊢ ‖L v‖ ≤ ‖L‖ * ‖v‖

Tactic:
exact ContinuousLinearMap.le_opNorm _ _

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
c : ℝ
⊢ smulLeftCLM F (c • g) = c • smulLeftCLM F g

Tactic:
RCLike.real_smul_eq_coe_smul (K := 𝕜') c,

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
𝕜' : Type u_10
inst✝¹ : RCLike 𝕜'
inst✝ : NormedSpace 𝕜' F
g : E → 𝕜'
hg : Function.HasTemperateGrowth g
c : ℝ
⊢ smulLeftCLM F (↑c • g) = c • smulLeftCLM F g
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h₂
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖(1 + ‖x‖) ^ k • f x‖.toNNReal ≤ ↑2 ^ k * (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f).toNNReal

Tactic:
Real.toNNReal_le_iff_le_coe

Goal state after:
case h₂
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖(1 + ‖x‖) ^ k • f x‖ ≤ ↑(↑2 ^ k * (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f).toNNReal)
Module: Mathlib.Analysis.Fourier.FourierTransform

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

Tactic:
simp_rw [fourierIntegral, Circle.smul_def, Real.probChar_apply, Complex.ofReal_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
ht✝ : Tendsto (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
t : ℝ
ht : t ∈ Ioi c
⊢ 0 ≤ t + m

Tactic:
by linarith [mem_Ioi.mp ht]

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst✝¹¹ : Fintype ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ (fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) m =
    fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (f x) m) w

Tactic:
rw [fourierIntegral, ContinuousMultilinearMap.integral_apply]
  · rfl
  · apply (fourierIntegral_convergent_iff he _ _).2 hf
    exact L.continuous₂

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ s.re - 1 < -1

Tactic:
sub_lt_iff_lt_add,

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ s.re < -1 + 1
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ s.re - 1 < -1

Tactic:
sub_lt_iff_lt_add,

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ s.re < -1 + 1
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
⊢ x ^ (- -(a.re + 1)) = ‖↑x ^ (a + 1)‖

Tactic:
neg_neg,

Goal state after:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
⊢ x ^ (a.re + 1) = ‖↑x ^ (a + 1)‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

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

Tactic:
rw [← mul_one π]

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

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

Tactic:
rw [← mul_one π]

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

Goal state before:
pp: p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p

Tactic:
by
  unfold fderivPolarCoordSymm
  rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]
  convert!
    HasFDerivAt.prodMk (𝕜 := ℝ)
      (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
      (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
    2 <;>
  simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]

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

Goal state before:
pp: case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -↑0 < s
⊢ 0 < s

Tactic:
rwa [Nat.cast_zero, neg_zero] at hs

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T = I₂ T + (I * I₄ T - I * I₅ T)

Tactic:
← C

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T = I₂ T + (I * I₄ T - (I₂ T - I₁ T + I * I₄ T))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / - -b) ^ (1 / 2) * cexp (0 - (I * t) ^ 2 / (4 * -b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
neg_neg,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (0 - (I * t) ^ 2 / (4 * -b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (- -((I * t) ^ 2 / (4 * b))) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
neg_neg,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp ((I * t) ^ 2 / (4 * b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : NormedSpace ℂ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℂ 𝕜 F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F g₁ ∘SL fourierMultiplierCLM F g₂) f = (fourierMultiplierCLM F (g₁ * g₂)) f

Tactic:
simp [fourierMultiplierCLM_fourierMultiplierCLM_apply hg₁ hg₂]

Goal state after: