mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ T ((hT.eigenvectorBasis hn).repr.symm w) =
    (hT.eigenvectorBasis hn).repr.symm (toLp 2 fun i ↦ ↑(hT.eigenvalues hn i) * w.ofLp i)

Tactic:
simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, map_smul, apply_eigenvectorBasis]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∑ x, w.ofLp x • ↑(hT.eigenvalues hn x) • (hT.eigenvectorBasis hn) x =
    ∑ x, (↑(hT.eigenvalues hn x) * w.ofLp x) • (hT.eigenvectorBasis hn) x
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
S : ↥(⨆ μ, eigenspace (↑T) μ)ᗮ →L[𝕜] ↥(⨆ μ, eigenspace (↑T) μ)ᗮ := T.restrict ⋯
hS_compact : IsCompactOperator ⇑S
hS_symm : (↑S).IsSymmetric
hS : ∀ (μ : 𝕜), eigenspace (↑S) μ = ⊥
h : ∀ (μ : 𝕜), HasEigenvalue (↑S) μ → μ = 0
⊢ (⨆ μ, eigenspace (↑T) μ)ᗮ = ⊥

Tactic:
eq_zero_of_forall_hasEigenvalue_eq_zero hS_compact hS_symm

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
S : ↥(⨆ μ, eigenspace (↑T) μ)ᗮ →L[𝕜] ↥(⨆ μ, eigenspace (↑T) μ)ᗮ := T.restrict ⋯
hS_compact : IsCompactOperator ⇑S
hS_symm : (↑S).IsSymmetric
hS : ∀ (μ : 𝕜), eigenspace (↑S) μ = ⊥
h : S = 0
⊢ (⨆ μ, eigenspace (↑T) μ)ᗮ = ⊥
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : 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
A : 𝓓^{n₁}_{K₁}(E, F) → E → F'
hadd : ∀ (f g : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (f + g) x = A f x + A g x
hsmul : ∀ (c : 𝕜) (f : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (c • f) x = c • A f x
hsmooth : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), ContDiff ℝ (↑n₂) (A f)
hsupp : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), EqOn (A f) 0 (↑K₂)ᶜ
hbound :
  ∀ (i : ℕ),
    ↑i ≤ n₂ →
      ∃ s C,
        0 ≤ C ∧
          ∀ (f : 𝓓^{n₁}_{K₁}(E, F)),
            ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (A f) x‖ ≤ C * (s.sup fun j ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ j) f
Φ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F') :=
  { toFun := fun f ↦ { toFun := A f, contDiff' := ⋯, zero_on_compl' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
i : ℕ
hi : ¬↑i ≤ n₂
⊢ ∃ s C,
    ∀ (x : 𝓓^{n₁}_{K₁}(E, F)),
      (ContDiffMapSupportedIn.seminorm 𝕜 E F' n₂ K₂ i) (Φ x) ≤
        C * (s.sup (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)) x

Tactic:
exact ⟨∅, 0, fun f ↦ by
          simp [ContDiffMapSupportedIn.seminorm_eq_bot_of_gt 𝕜 (not_le.1 hi)]⟩

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 k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) ((fderivLM 𝕜 n k) f) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f

Tactic:
ContDiffMapSupportedIn.seminorm_le_iff 𝕜 (apply_nonneg ..)

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 k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ ↑i ≤ k →
    ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑((fderivLM 𝕜 n k) f)) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ (ENNReal.toReal 2).HolderConjugate (ENNReal.toReal 2)

Tactic:
rw [Real.holderConjugate_iff]

Goal state after:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ 1 < ENNReal.toReal 2 ∧ (ENNReal.toReal 2)⁻¹ + (ENNReal.toReal 2)⁻¹ = 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
⊢ ∀ {a : C(AddCircle T, ℂ)}, a ∈ (adjoin ℂ (range fourier)).carrier → star a ∈ (adjoin ℂ (range fourier)).carrier

Tactic:
by
    change Algebra.adjoin ℂ (range (fourier (T := T))) ≤
      star (Algebra.adjoin ℂ (range (fourier (T := T))))
    refine adjoin_le ?_
    rintro - ⟨n, rfl⟩
    exact subset_adjoin ⟨-n, ext fun _ => fourier_neg⟩

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑fourierSubalgebra.toSubalgebra, f x ≠ f y

Tactic:
refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩

Goal state after:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fun f ↦ ⇑f) (fourier 1) x ≠ (fun f ↦ ⇑f) (fourier 1) y
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 : ℕ
d : ℝ
left✝ : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d
x : E
hx : x ≠ 0
⊢ ‖f x‖ ≤ d / ‖x‖ ^ ↑k

Tactic:
le_div_iff₀' (by positivity)

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 * ‖f x‖ ≤ d
x : E
hx : x ≠ 0
⊢ ‖x‖ ^ ↑k * ‖f x‖ ≤ d
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : 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 μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ 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₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
obtain ⟨v, v_open, x₀_v, hv⟩ : ∃ v : Set α, IsOpen v ∧ x₀ ∈ v ∧ v ∩ s ⊆ c ⁻¹' Ioi t' :=
      _root_.continuousOn_iff.1 hc x₀ h₀ (Ioi t') isOpen_Ioi t'x₀

Goal state after:
α : 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 μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ 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₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h₁
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := ⋯
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ⋯
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
N : ℕ
hN₁ : 1 ≤ N
hN₂ : N ≤ n
hN₁' : N ≠ 0
⊢ C ≤ (C + 1) ^ N

pp: case h₂
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := ⋯
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ⋯
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
N : ℕ
hN₁ : 1 ≤ N
hN₂ : N ≤ n
hN₁' : N ≠ 0
⊢ (1 + ‖x‖) ^ l ≤ ((1 + ‖x‖) ^ l) ^ N

Tactic:
· exact le_trans (by simp) (le_self_pow₀ (by simp [hC]) hN₁')

Goal state after:
case h₂
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := ⋯
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ⋯
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
N : ℕ
hN₁ : 1 ≤ N
hN₂ : N ≤ n
hN₁' : N ≠ 0
⊢ (1 + ‖x‖) ^ l ≤ ((1 + ‖x‖) ^ l) ^ N
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h
ι : 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 : ℕ × ℕ := ⋯
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)
⊢ ∫ (x : D), (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f) ∂μ ≤
    (2 ^ n * ∫ (x : D), (1 + ‖x‖) ^ (-↑n) ∂μ) * ((Finset.Iic m).sup (schwartzSeminormFamily 𝕜 D V)) f

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 : ℕ × ℕ := ⋯
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 ↦ (1 + ‖i‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) μ

Tactic:
· unfold schwartzSeminormFamily
    rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]

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 : ℕ × ℕ := ⋯
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 ↦ (1 + ‖i‖) ^ (-↑n) * (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 : ℕ × ℕ := ⋯
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 ↦ (1 + ‖i‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) μ

Tactic:
apply h.mul_const

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
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm (↑↑f - g) p μ ≤ ENNReal.ofReal ε
⊢ ↑↑f - ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ) =ᵐ[μ] ↑↑f - g

Tactic:
filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]

Goal state after:
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✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm (↑↑f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∀ (a : E),
    ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ) a = (hg₁.toSchwartzMap hg₂) a →
      (↑↑f - ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ)) a = (↑↑f - g) a
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ioi c
⊢ 0 ≤ t⁻¹ / log t ^ 2

Tactic:
have : 0 < t := by grind

Goal state after:
c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ioi c
this : 0 < t
⊢ 0 ≤ t⁻¹ / log t ^ 2
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case inr.inr
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 * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((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
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (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:
mul_le_mul_iff_right₀ (pow_pos (by simp [hw]) n)

Goal state after:
case inr.inr
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
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (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‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
| ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
rw [this, ← _root_.integral_ofReal]

Goal state after:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
| ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ Gamma 1 = 1

Tactic:
rw [Gamma_eq_integral] <;> simp

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

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = ↑1 ^ (a - 1) * ↑x ^ (a - 1) * cexp (-(↑r * ↑x))

Tactic:
ofReal_one,

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = 1 ^ (a - 1) * ↑x ^ (a - 1) * cexp (-(↑r * ↑x))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 ≤ᵐ[volume.restrict (Ioi 0)] fun x ↦ rexp (-x) * x ^ (s - 1)

Tactic:
refine eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_
    exact fun x hx => (mul_pos (exp_pos _) (rpow_pos_of_pos hx _)).le

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

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬0 < b

Tactic:
not_lt

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ b ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ -b.re < 0

Tactic:
neg_lt_zero

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ 0 < b.re
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ ¬b.re < 0 ∨ ¬b.im = 0

Tactic:
not_lt

Goal state after:
case e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 0 ≤ b.re ∨ ¬b.im = 0
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
s : Set E
hxs : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
t : Set E := s ∩ ↑Ω
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htx : x ∈ t
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0

Tactic:
obtain ⟨u, h₁, h₂, h₃, -, h₄⟩ :=
    exists_contDiff_tsupport_subset (n := n) ((IsOpen.mem_nhds_iff ht).mpr htx)

Goal state after:
case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
s : Set E
hxs : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
t : Set E := s ∩ ↑Ω
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htx : x ∈ t
u : E → ℝ
h₁ : tsupport u ⊆ t
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑n) u
h₄ : u x = 1
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ (toTemperedDistribution (f.toLp p μ)) g = ((toTemperedDistributionCLM E F μ) f) g

Tactic:
simp only [Lp.toTemperedDistribution_apply, toTemperedDistributionCLM_apply_apply]

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ ∫ (x : E), g x • ↑↑(f.toLp p μ) x ∂μ = ∫ (x : E), g x • f x ∂μ
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
n : d → ℤ
x : UnitAddTorus d
⊢ (mFourier (-n)) x = (starRingEnd ℂ) ((mFourier n) x)

Tactic:
simp only [mFourier, Pi.neg_apply, fourier_neg, ContinuousMap.coe_mk, map_prod]

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
⊢ p.Prime → p ≠ 1

Tactic:
intro pp contra
  apply Nat.Prime.ne_one pp
  rw [PNat.coe_eq_one_iff]
  apply contra

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
| a

Tactic:
← am

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
| a.gcd m