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

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖star a * a‖ = ‖a‖ * ‖a‖

Tactic:
CStarRing.norm_star_mul_self

Goal state after:
A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖a‖ * ‖a‖ = ‖a‖ * ‖a‖
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ ⟪(ContinuousMap.toLp 2 μ 𝕜) f, (ContinuousMap.toLp 2 μ 𝕜) g⟫ = ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
apply integral_congr_ae
  have hf_ae := f.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
  have hg_ae := g.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
  filter_upwards [hf_ae, hg_ae] with _ hf hg
  rw [hf, hg]
  simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ENNReal.ofReal ε' * ENNReal.ofReal (μ (tsupport f)).toReal ^ (1 / p.toReal) ≤ ENNReal.ofReal ε

Tactic:
ofReal_rpow_of_pos hs₂,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ENNReal.ofReal ε' * ENNReal.ofReal ((μ (tsupport f)).toReal ^ (1 / p.toReal)) ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case neg
𝕜 : 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
⊢ (P (min i j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P (min i j)) x) = 0

Tactic:
rcases Nat.lt_or_gt_of_ne h with h' | h'

Goal state after:
case neg.inl
𝕜 : 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 (min i j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P (min i j)) x) = 0

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 (min i j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P (min i j)) x) = 0
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace ℝ E
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
x✝ : ℕ × ℕ
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (deriv ⇑f) x‖ ≤ 1 * ({(k, n + 1)}.sup (schwartzSeminormFamily 𝕜 ℝ F)) f

Tactic:
by
      simpa only [Real.norm_eq_abs, Finset.sup_singleton, schwartzSeminormFamily_apply, one_mul,
        norm_iteratedFDeriv_eq_norm_iteratedDeriv, ← iteratedDeriv_succ'] using
        f.le_seminorm' 𝕜 k (n + 1) x

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

Goal state before:
pp: 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 : D), (L (f x)) ((∂_{v} g) x) ∂μ = -∫ (x : D), (L ((∂_{v} f) x)) (g x) ∂μ

Tactic:
apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable (v := v)
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable
    (bilinLeftCLM L (∂_{v} g).hasTemperateGrowth _).integrable
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable

Goal state after:
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

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
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ fourierSubalgebra.SeparatesPoints

Tactic:
intro x y hxy

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ cexp (2 * ↑π * I * ↑n * ↑y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) x

Tactic:
refine (?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ cexp (2 * ↑π * I * ↑n * y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) ↑x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ HasDerivAt (fun y ↦ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) ((fourier (-n)) ↑x) x

Tactic:
convert! (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1

Goal state after:
case e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fun y ↦ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) = fun x ↦ (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

case e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)
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 : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
⊢ ∫ (x : α) in s \ u, ‖φ i x • g x‖ ∂μ ≤ ∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ

Tactic:
by
        refine setIntegral_mono_on ?_ ?_ (hs.diff u_open.measurableSet) fun x hx => ?_
        · exact IntegrableOn.mono_set h''i.norm sdiff_subset
        · exact IntegrableOn.mono_set (hmg.norm.const_mul _) sdiff_subset
        rw [norm_smul]
        gcongr
        simpa only [Pi.zero_apply, dist_zero_left] using (hi x hx).le

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
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
x : ℝ
hx : 1 ≤ x
⊢ ‖x ^ (-↑k)‖ ≤ 1 * ‖x ^ s‖

Tactic:
rw [one_mul, Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity),
    ← Real.rpow_intCast, Int.cast_neg, Int.cast_natCast]

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)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
x : ℝ
hx : 1 ≤ x
⊢ x ^ (-↑k) ≤ x ^ s
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ∫ (a : V), ‖e (-(L a) w) • f a‖ ∂μ = ∫ (v : V), ‖f v‖ ∂μ

Tactic:
simp_rw [Circle.norm_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v ↦ e (-(L v) x) • g v) μ
hf : Integrable (fun v ↦ e (-(L v) w) • f v) μ
this : Integrable (fun v ↦ e (-(L v) (-w)) • e (-(L v) w) • f v) μ
⊢ Integrable f μ

Tactic:
← mul_smul (e _) (e _) (f _),

Goal state after:
𝕜 : 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
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v ↦ e (-(L v) x) • g v) μ
hf : Integrable (fun v ↦ e (-(L v) w) • f v) μ
this : Integrable (fun v ↦ (e (-(L v) (-w)) * e (-(L v) w)) • f v) μ
⊢ Integrable f μ
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₀
⊢ Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
let f := fun x ↦ g (x₀ - x)
  have If : Integrable f μ := by simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg
  have : Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • x)) • f x ∂μ)
      atTop (𝓝 (f 0)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If
    have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
    exact A.comp <| by fun_prop
  simp only [f, sub_zero] at this
  convert! this using 2 with c
  conv_rhs => rw [← integral_add_left_eq_self x₀ (μ := μ)
    (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ← integral_neg_eq_self]
  simp [sub_eq_add_neg]

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

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x ↦ s * ↑x ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
⊢ (fun x ↦ s * ↑x ^ (s - 1)) x = deriv (fun x ↦ ↑x ^ s) x

Tactic:
Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x ↦ s * ↑x ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
⊢ (fun x ↦ s * ↑x ^ (s - 1)) x = s * ↑x ^ (s - 1)
Module: Mathlib.Analysis.Fourier.FourierTransform

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

Tactic:
simp_rw [Circle.norm_smul]

Goal state after:
V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ ∫ (a : V), ‖↑↑f a‖ ≤ ‖f‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (log ↑x * ((starRingEnd ℂ) s - 1)) =
    ↑(rexp (-x)) * cexp ((starRingEnd ℂ) (log ↑x) * (starRingEnd ℂ) (s - 1))

Tactic:
← ofReal_log (le_of_lt hx),

Goal state after:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (↑(Real.log x) * ((starRingEnd ℂ) s - 1)) =
    ↑(rexp (-x)) * cexp ((starRingEnd ℂ) ↑(Real.log x) * (starRingEnd ℂ) (s - 1))
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case e'_9
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
h_int : Integrable (fun v ↦ fourierSMulRight L f v) volume
⊢ 𝓕 (fun x ↦ (-2 * ↑π * I * ↑x) • f x) w =
    ∫ (v : ℝ), 𝐞 (-((ContinuousLinearMap.toLinearMap₁₂ L) v) w) • (fourierSMulRight L f v) 1

Tactic:
fourier_real_eq

Goal state after:
case e'_9
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
h_int : Integrable (fun v ↦ fourierSMulRight L f v) volume
⊢ ∫ (v : ℝ), 𝐞 (-(v * w)) • (-2 * ↑π * I * ↑v) • f v =
    ∫ (v : ℝ), 𝐞 (-((ContinuousLinearMap.toLinearMap₁₂ L) v) w) • (fourierSMulRight L f v) 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
⊢ IntegrableOn (fun x ↦ rexp (-b * x ^ 2)) (Ioi 0) volume ↔ 0 < b

Tactic:
by
  refine ⟨fun h => ?_, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩
  by_contra! hb
  have : ∫⁻ _ : ℝ in Ioi 0, 1 ≤ ∫⁻ x : ℝ in Ioi 0, ‖exp (-b * x ^ 2)‖₊ := by
    apply lintegral_mono (fun x ↦ _)
    simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
      Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]
    exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)
  simpa using this.trans_lt h.2

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume] Set.univ

Tactic:
rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]
  exact ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ

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

Goal state before:
pp: b : ℂ
c T : ℝ
⊢ ‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

Tactic:
by
  rw [Complex.norm_exp, neg_mul, neg_re, ← re_add_im b]
  simp only [sq, re_add_im, mul_re, mul_im, add_re, add_im, ofReal_re, ofReal_im, I_re, I_im]
  ring_nf

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

Goal state before:
pp: case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ ≤ n

Tactic:
Nat.floor_of_nonpos

Goal state after:
case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 0 ≤ n

case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 1 - s.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e_a
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⁻¹ ^ (1 / 2) = 1 / b ^ (1 / 2)

Tactic:
inv_cpow,

Goal state after:
case e_a
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 ^ (1 / 2))⁻¹ = 1 / b ^ (1 / 2)

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.arg ≠ π
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ 𝓕⁻ (∂_{m} f) = -(2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) (𝓕⁻ f)

Tactic:
by
  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
  simp [fourierInv_apply_eq, fourier_lineDerivOp_eq,
    smulLeftCLM_compCLMOfContinuousLinearEquiv ℂ this, Function.comp_def, smulLeftCLM_fun_neg this]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ (mFourierSubalgebra d).SeparatesPoints

Tactic:
intro x y hxy

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : x ≠ y
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (starRingEnd ℂ) ((mFourier i) a✝) * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝

Tactic:
← mFourier_neg,

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (mFourier (-i)) a✝ * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
x : UnitAddTorus d
⊢ HasSum (fun i ↦ mFourierCoeff (⇑f) i • (mFourier i) x) (f x)

Tactic:
simpa only [map_smul] using! (ContinuousMap.evalCLM ℂ x).hasSum
    (hasSum_mFourier_series_of_summable h)

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) ↔ a ≠ 0

Tactic:
refine ⟨?_, fun ha ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) → a ≠ 0

case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
⊢ ∃ ψ, ψ a ≠ 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n m : ℕ+
h : 0 < (↑n).lcm ↑m * (↑n).gcd ↑m
⊢ 0 < (↑n).lcm ↑m

Tactic:
exact pos_of_dvd_of_pos (Dvd.intro (Nat.gcd (n : ℕ) (m : ℕ)) rfl) h

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

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

Tactic:
contra

Goal state after:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case prime_pow
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

Tactic:
| prime_pow p n hp hn =>

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

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ∫ (a : V), ‖𝐞 (-⟪a, w⟫) • (f a - f (a + i w))‖ < 2 * ε

Tactic:
simp_rw [Circle.norm_smul]

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ∫ (a : V), ‖f a - f (a + (1 / (2 * ‖w‖ ^ 2)) • w)‖ < 2 * ε