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

Goal state before:
pp: 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✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ |x| ^ (r - ↑n) = x ^ (-(↑n - r))

Tactic:
rw [neg_sub]

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 : ℕ
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✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ |x| ^ (r - ↑n) = x ^ (r - ↑n)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsSelfAdjoint T
a✝ : Nontrivial E
h : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T ∧ -(algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - c
⊢ False

Tactic:
grind [ciSup_le hc, norm_eq_iSup_rayleighQuotient T hT.isSymmetric]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
B : Matrix n n R
inst✝ : IsDomain R
hAps : B.charpoly.Splits
⊢ B.trace = B.charpoly.roots.sum

Tactic:
rcases isEmpty_or_nonempty n with h | _

Goal state after:
case inl
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
B : Matrix n n R
inst✝ : IsDomain R
hAps : B.charpoly.Splits
h : IsEmpty n
⊢ B.trace = B.charpoly.roots.sum

case inr
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
B : Matrix n n R
inst✝ : IsDomain R
hAps : B.charpoly.Splits
h✝ : Nonempty n
⊢ B.trace = B.charpoly.roots.sum
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
⊢ HasEigenvalue (↑T) μ ↔ μ ∈ spectrum 𝕜 T

Tactic:
constructor
  · intro hμ'
    rw [ContinuousLinearMap.spectrum_eq]
    exact hμ'.mem_spectrum
  · exact (hasEigenvalue_or_mem_resolventSet hT hμ).resolve_right

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A.rank = Fintype.card { i // hA.eigenvalues i ≠ 0 }

Tactic:
rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]

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
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn (⇑f + ⇑g) 0 (↑K)ᶜ

Tactic:
rw [← add_zero 0]
    exact f.zero_on_compl.comp_left₂ g.zero_on_compl

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

Goal state before:
pp: case neg
𝕜 : 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
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥⊥

Tactic:
finrank_bot,

Goal state after:
case neg
𝕜 : 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
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = 0
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
this : Fintype ↑(spectrum ℝ A) := Fintype.ofFinite ↑(spectrum ℝ A)
⊢ ‖⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩‖ = ‖f‖

Tactic:
rw [ContinuousMap.norm_eq_norm_coeFn]

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
this : Fintype ↑(spectrum ℝ A) := Fintype.ofFinite ↑(spectrum ℝ A)
⊢ ‖⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩‖ = ‖⇑f‖
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 b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
⊢ star b * b * (star a * a) = star b * star a * (a * b)

Tactic:
h₂.star_left.symm.mul_mul_mul_comm,

Goal state after:
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 b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
⊢ star b * star a * (b * a) = star b * star a * (a * b)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (‖r‖ • a) = ‖r‖ • abs a

Tactic:
lift ‖r‖ to ℝ≥0 using norm_nonneg _ with r

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r✝ : 𝕜
a : A
r : ℝ≥0
⊢ abs (↑r • a) = ↑r • abs a
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
hi : ↑i ≤ k
x : E
hx : x ∈ K
hi' : ↑i + 1 ≤ n
⊢ ‖iteratedFDeriv ℝ i (⇑((fderivLM 𝕜 n k) f)) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f

Tactic:
simpa [hk, norm_iteratedFDeriv_fderiv] using
      norm_iteratedFDeriv_apply_le_seminorm 𝕜 hi'

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
⊢ ∃ f,
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ

Tactic:
have ηpos : (0 : ℝ≥0∞) < η := ENNReal.coe_lt_coe.2 η_pos

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✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
⊢ ∃ f,
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
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
b : SchauderBasis 𝕜 X
x : X
this : Tendsto (fun A ↦ (GeneralSchauderBasis.proj b A) x) (SummationFilter.conditional ℕ).filter (𝓝 x)
⊢ Tendsto (fun n ↦ (b.proj n) x) atTop (𝓝 x)

Tactic:
SummationFilter.conditional_filter_eq_map_range

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
x : X
this : Tendsto (fun A ↦ (GeneralSchauderBasis.proj b A) x) (map Finset.range atTop) (𝓝 x)
⊢ Tendsto (fun n ↦ (b.proj n) x) atTop (𝓝 x)
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 𝕜 ↥(U ⊔ V) + Module.finrank 𝕜 ↥⊥ = Module.finrank 𝕜 ↥U + Module.finrank 𝕜 ↥V
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1

Tactic:
finrank_bot,

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 : Module.finrank 𝕜 ↥(U ⊔ V) + 0 = Module.finrank 𝕜 ↥U + Module.finrank 𝕜 ↥V
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ ‖{ toFun := fun f ↦ ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖

Tactic:
have H : 0 < (2 : ℝ≥0∞).toReal := by simp
    suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
      exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
    refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)
    convert! (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
    ext s
    exact mod_cast (hV.norm_sum f s).symm

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

Goal state before:
pp: case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(Circle.exp (2 * π / T * -n • z✝)) = ↑(Circle.exp (-(2 * π / T * n • z✝)))

Tactic:
neg_smul,

Goal state after:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(Circle.exp (2 * π / T * -(n • z✝))) = ↑(Circle.exp (-(2 * π / T * n • z✝)))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ‖fourier n‖ = 1

Tactic:
by
  rw [ContinuousMap.norm_eq_iSup_norm]
  have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => Circle.norm_coe _
  simp_rw [this]
  exact ciSup_const

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

Goal state before:
pp: a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ ↑(1 / (b - a)) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (↑(1 / (b - a)) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f' x))

Tactic:
ofReal_div,

Goal state after:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ ↑1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (↑1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f' x))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k : ℕ
d : ℝ
left✝ : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d
x : E
hx : x ≠ 0
⊢ ‖f x‖ ≤ d * (‖x‖ ^ ↑k)⁻¹

Tactic:
← div_eq_mul_inv,

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
⊢ ‖f x‖ ≤ d / ‖x‖ ^ ↑k
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
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)
⊢ n ^ i ≤ (n + 1) ^ i

Tactic:
gcongr; lia

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

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := ⋯
If : Integrable f μ
⊢ ContinuousAt f 0

Tactic:
have A : ContinuousAt g (x₀ - 0) := by simpa using h'g

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x ↦ g (x₀ - x)
If : Integrable f μ
A : ContinuousAt g (x₀ - 0)
⊢ ContinuousAt f 0
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
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hp₁ : p ≠ 0
hp₂ : p ≠ ∞
hμ : μ.HasTemperateGrowth
⊢ ‖f.toLp p μ‖ = (∫ (x : E), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹

Tactic:
rw [norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm hp₁ hp₂ (f.memLp p μ),
    ENNReal.toReal_ofReal (by positivity)]

Goal state after:
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
⊢ ∫ (v : V), Real.probChar (-(L v) w) • f v ∂μ = ∫ (v : V), Complex.exp (-↑((L v) w) * Complex.I) • f v ∂μ

Tactic:
Circle.smul_def,

Goal state after:
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
⊢ ∫ (v : V), ↑(Real.probChar (-(L v) w)) • f v ∂μ = ∫ (v : V), Complex.exp (-↑((L v) w) * Complex.I) • f v ∂μ
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‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl

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
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ
Module: Mathlib.Analysis.Fourier.FourierTransform

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

Tactic:
Circle.smul_def,

Goal state after:
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_5
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ ∫ (v : V), ↑(𝐞 (-(L v) w)) • f v ∂μ = ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = ∫ (v : V), Complex.exp (↑(-2 * π * ⟪v, w⟫) * Complex.I) • f v

Tactic:
Circle.smul_def,

Goal state after:
V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ ∫ (v : V), ↑(𝐞 (-⟪v, w⟫)) • f v = ∫ (v : V), Complex.exp (↑(-2 * π * ⟪v, w⟫) * Complex.I) • f v
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ ∫ (v : V), 𝐞 ⟪v, w⟫ • f v = ∫ (v : V), Complex.exp (↑(2 * π * ⟪v, w⟫) * Complex.I) • f v

Tactic:
Circle.smul_def,

Goal state after:
V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ ∫ (v : V), ↑(𝐞 ⟪v, w⟫) • f v = ∫ (v : V), Complex.exp (↑(2 * π * ⟪v, w⟫) * Complex.I) • f v
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕 (𝓕⁻ f) = 𝓕 fun x ↦ 𝓕 f (-x)

Tactic:
← fourierInv_eq_fourier_neg

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

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ IntegrableOn (fun t ↦ t⁻¹ / log t ^ 2) (Ioi c) volume

Tactic:
apply integrableOn_Ioi_deriv_of_nonneg' _ _ tendsto_log_atTop.inv_tendsto_atTop.neg

Goal state after:
c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun x ↦ -log⁻¹ x) (x⁻¹ / log x ^ 2) x

c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ioi c, 0 ≤ x⁻¹ / log x ^ 2
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ ∫ (v : ℝ), 𝐞 (-(v * w)) • f v = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
Circle.smul_def,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ ∫ (v : ℝ), ↑(𝐞 (-(v * w))) • f v = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v