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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMinOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
⊢ HasEigenvalue T ↑(⨅ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)

Tactic:
have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀'

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMinOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ HasEigenvalue T ↑(⨅ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
Module: Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
h : IsCompactOperator id
⊢ FiniteDimensional 𝕜 E

Tactic:
have := LocallyCompactSpace.of_isCompactOperator_id h

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
h : IsCompactOperator id
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
⊢ diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = 0

Tactic:
simp only [LinearMap.coe_coe, cfcAux_apply, conjStarAlgAut_apply] at hf

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf :
  ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary =
    0
⊢ diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = 0
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ IsClosedEmbedding ⇑hA.cfcAux

Tactic:
by
  have h0 : FiniteDimensional ℝ C(spectrum ℝ A, ℝ) :=
    FiniteDimensional.of_injective (ContinuousMap.coeFnLinearMap ℝ (M := ℝ)) DFunLike.coe_injective
  refine LinearMap.isClosedEmbedding_of_injective (𝕜 := ℝ) (E := C(spectrum ℝ A, ℝ))
    (F := Matrix n n 𝕜) (f := hA.cfcAux) <| LinearMap.ker_eq_bot'.mpr fun f hf ↦ ?_
  have h2 :
      diagonal (RCLike.ofReal ∘ f ∘ fun i ↦ ⟨hA.eigenvalues i, hA.eigenvalues_mem_spectrum_real i⟩)
        = (0 : Matrix n n 𝕜) := by
    simp only [LinearMap.coe_coe, cfcAux_apply, conjStarAlgAut_apply] at hf
    replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))
    simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf
    simpa [← mul_assoc] using congr((star hA.eigenvectorUnitary : Matrix n n 𝕜) * $hf)
  ext x
  simp only [ContinuousMap.zero_apply]
  obtain ⟨x, hx⟩ := x
  obtain ⟨i, rfl⟩ := hA.spectrum_real_eq_range_eigenvalues ▸ hx
  rw [← diagonal_zero] at h2
  have := diagonal_eq_diagonal_iff.mp h2
  exact RCLike.ofReal_eq_zero.mp (this i)

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A

Tactic:
by
  conv_rhs => rw [hA.spectral_theorem]
  rfl

Goal state after:
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : M *ᵥ x ⬝ᵥ star x = 0
⊢ x = 0

Tactic:
by_contra! h
      simpa [hx, lt_irrefl, dotProduct_comm] using hM.re_dotProduct_pos h

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
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvalue T ↑(hT.unsortedEigenvalues hn i)

Tactic:
by
  unfold unsortedEigenvalues
  let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
    hT.orthogonalFamily_eigenspaces'
  rwa [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]

Goal state after:
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
ha : IsStarNormal a
⊢ abs (a * a) = star a * a

Tactic:
rw [Commute.cfcAbs_mul_eq (.refl a) ha.star_comm_self.symm, abs_mul_abs]

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

Goal state before:
pp: case neg
𝕜 : 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 [monoLM_eq_zero, H]

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

Goal state before:
pp: 𝕜 : 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)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
by_cases H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
  · simp (discharger := positivity) only [ContDiffMapSupportedIn.seminorm_le_iff, monoLM_apply, H,
      and_self, ↓reduceIte]
    intro hik _ _
    exact norm_iteratedFDeriv_apply_le_seminorm _ (hik.trans (mod_cast H.1))
  · simp [monoLM_eq_zero, H]

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓓^{n}_{K}(E, F)
⊢ StronglyMeasurable ⇑f

Tactic:
exact f.continuous.stronglyMeasurable_of_hasCompactSupport f.hasCompactSupport

Goal state after:
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
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
⊢ ∫ (a : α), ⟪↑↑(indicatorConstLp 2 hs hμs c) a, ↑↑f a⟫ ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫ ∂μ

Tactic:
← integral_indicator hs

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
⊢ ∫ (a : α), ⟪↑↑(indicatorConstLp 2 hs hμs c) a, ↑↑f a⟫ ∂μ = ∫ (x : α), s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x ∂μ
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ ∀ (a : AddCircle T), ‖(fourier n) a‖ ≤ 1

Tactic:
intro t

Goal state after:
case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
⊢ ‖(fourier n) t‖ ≤ 1
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)
h : ∫ (a : α) in t, φ i a ∂μ = 0
⊢ False

Tactic:
by simp [h] at h'i

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 : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
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₀) (𝓝 a)
h : α → E := g - t.indicator fun x ↦ a
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
⊢ Integrable (t.indicator fun a_1 ↦ φ i a_1 • a) (μ.restrict s)

Tactic:
rw [integrable_indicator_iff ht]

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 : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
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₀) (𝓝 a)
h : α → E := g - t.indicator fun x ↦ a
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
⊢ IntegrableOn (fun a_1 ↦ φ i a_1 • a) t (μ.restrict s)
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 : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
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₀) (𝓝 a)
h✝ : α → E := g - t.indicator fun x ↦ a
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h✝ x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h : ∫ (a : α) in t, φ i a ∂μ = 0
⊢ False

Tactic:
by simp [h] at h'i

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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (fun x ↦ (B (f x)) (g x)) x‖ ≤
    ‖B‖ * (↑n + 1) * ↑(n.choose (n / 2)) * (C * 2 ^ (l + k)) *
      ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f

Tactic:
have hxk : 0 ≤ ‖x‖ ^ k := by positivity

Goal state after:
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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (fun x ↦ (B (f x)) (g x)) x‖ ≤
    ‖B‖ * (↑n + 1) * ↑(n.choose (n / 2)) * (C * 2 ^ (l + k)) *
      ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f
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
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
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
⊢ ‖iteratedFDeriv ℝ k
        (fun v ↦
          (-(2 * ↑π * I)) ^ n •
            ((smulRightL ℝ (fun x ↦ W) E)
                ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x ↦ L v))
              (f v))
        v‖ ≤
    (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C

Tactic:
have I₃ m : ‖iteratedFDeriv ℝ m (T ∘ (ContinuousLinearMap.pi (fun (_ : Fin n) ↦ L))) v‖ ≤
      n.descFactorial m * ‖L‖ ^ n * ‖v‖ ^ (n - m) := by
    apply (I₂ m).trans (le_of_eq _)
    rcases le_or_gt m n with hm | hm
    · rw [show ‖L‖ ^ n = ‖L‖ ^ (m + (n - m)) by rw [Nat.add_sub_cancel' hm], pow_add]
      ring
    · simp only [Nat.descFactorial_eq_zero_iff_lt.mpr hm, CharP.cast_eq_zero, mul_one, zero_mul]

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
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
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)
⊢ ‖iteratedFDeriv ℝ k
        (fun v ↦
          (-(2 * ↑π * I)) ^ n •
            ((smulRightL ℝ (fun x ↦ W) E)
                ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x ↦ L v))
              (f v))
        v‖ ≤
    (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
⊢ HasFDerivAt
    (fun y ↦ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n.succ) w).curryLeft w

Tactic:
have I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ :=
      integrable_fourierPowSMulRight L (hf n hn.le) h'f

Goal state after:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
⊢ HasFDerivAt
    (fun y ↦ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n.succ) w).curryLeft w
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
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
⊢ ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F)) (x : E),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (⇑L ∘ ⇑f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
by
  intro ⟨k, n⟩
  use {⟨k, n⟩}, ‖L‖, by positivity
  intro f x
  simp only [Finset.sup_singleton, schwartzSeminormFamily_apply]
  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.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k✝ n : ℕ
hk : ↑k✝ ≤ K
hn : ↑n ≤ N
w : W
k : ℕ
⊢ ↑k ≤ K → Integrable (fun v ↦ ‖v‖ ^ k * ‖f v‖) μ

Tactic:
hk

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k✝ n : ℕ
hk✝ : ↑k✝ ≤ K
hn : ↑n ≤ N
w : W
k : ℕ
hk : ↑k ≤ K
⊢ Integrable (fun v ↦ ‖v‖ ^ k * ‖f v‖) μ
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: case neg
𝕜 : 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
⊢ ∫ (ξ : W), (M (fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (fourierIntegral e ν L.flip g x) ∂μ

Tactic:
simp [integral, hG]

Goal state after: