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

Goal state before:
pp: c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, rexp (-x) = rexp (-c)

Tactic:
simpa only [integral_comp_neg_Ioi] using integral_exp_Iic (-c)

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

Goal state before:
pp: case refine_2
a : ℂ
ha : a.re < 0
c : ℝ
⊢ Integrable (fun a_1 ↦ ‖Complex.exp (a * ↑a_1)‖) (volume.restrict (Ioi c))

Tactic:
simpa [Complex.norm_exp] using!
      (integrableOn_Ioi_comp_mul_left_iff (fun x => exp (-x)) c (a := -a.re) (by simpa)).mpr <|
        integrableOn_exp_neg_Ioi _

Goal state after:
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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
⊢ y ∈ s → ‖f (y, x)‖ ≤ C * ‖g x‖

Tactic:
hy

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
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun t ↦ ↑t ^ a) (volume.restrict (Ioi c))

Tactic:
refine ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi

Goal state after:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (fun t ↦ ↑t ^ a) (Ioi c) t
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (deriv fun x ↦ ↑x ^ s) (Ioi t) volume

Tactic:
have h : IntegrableOn (fun x : ℝ ↦ s * x ^ (s - 1)) (Set.Ioi t) := by
    refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
    rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
  refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi
  rw [Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)]

Goal state after:
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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
⊢ f₁ a✝ = f₂ a✝ → 𝐞 (-((innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((innerₗ V) a✝) x) • f₂ a✝

Tactic:
hf'

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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((innerₗ V) a✝) x) • f₂ a✝
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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((innerₗ V) a✝) x) • f₂ a✝

Tactic:
hf'

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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((innerₗ V) a✝) x) • f₂ a✝ = 𝐞 (-((innerₗ V) a✝) x) • f₂ a✝
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x ↦ (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ (-1).re

Tactic:
rw [Complex.neg_re, Complex.one_re]

Goal state after:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x ↦ (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ -1
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

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

Tactic:
simp_rw [neg_neg, Complex.norm_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]

Goal state after:
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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
⊢ f₁ a✝ = f₂ a✝ → 𝐞 (-((-innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((-innerₗ V) a✝) x) • f₂ a✝

Tactic:
hf'

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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((-innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((-innerₗ V) a✝) x) • f₂ a✝
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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((-innerₗ V) a✝) x) • f₁ a✝ = 𝐞 (-((-innerₗ V) a✝) x) • f₂ a✝

Tactic:
hf'

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₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x a✝ : V
hf' : f₁ a✝ = f₂ a✝
⊢ 𝐞 (-((-innerₗ V) a✝) x) • f₂ a✝ = 𝐞 (-((-innerₗ V) a✝) x) • f₂ a✝
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case e'_6
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
v : ℝ
⊢ v • f v = (v • ↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (f v)) 1

Tactic:
exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x ↦ fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Tactic:
have : 𝓕 (deriv f) x = 𝓕 (fderiv ℝ f) x 1 := by
    simp only [fourier_continuousLinearMap_apply I, fderiv_apply_one_eq_deriv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x ↦ fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x ↦ fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Tactic:
rw [this, fourier_fderiv hf h'f I]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x ↦ fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ (fourierSMulRight (-innerSL ℝ) (𝓕 f) x) 1 = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)

Tactic:
let e := (equivFin ι).symm

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ ∫ (x : (i : ι) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
let e := (equivFin ι).symm

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ ∫ (x : (i : ι) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
⊢ |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
hy

Goal state after:
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (fun {b} ↦ (↑π / b) ^ (1 / 2)) {c | 0 < c.re}

Tactic:
refine
      continuousOn_of_forall_continuousAt fun b hb =>
        (continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))

Goal state after:
b✝ : ℂ
hb✝ : 0 < b✝.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : b ∈ {c | 0 < c.re}
⊢ 0 < (↑π / b).re
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b✝ : ℂ
hb✝ : 0 < b✝.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : b ∈ {c | 0 < c.re}
⊢ 0 < π * b.re / normSq b

Tactic:
exact div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
⊢ y ∈ uIoc 0 c →
    ‖I * (cexp (-b * (↑T + ↑y * I) ^ 2) - cexp (-b * (↑T - ↑y * I) ^ 2))‖ ≤
      2 * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
hy

Goal state after:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
hy : y ∈ uIoc 0 c
⊢ ‖I * (cexp (-b * (↑T + ↑y * I) ^ 2) - cexp (-b * (↑T - ↑y * I) ^ 2))‖ ≤
    2 * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ 0 = 0 / 2

pp: case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Tactic:
zero_div

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ 0 = 0

case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) (volume.restrict (Ioi 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
⊢ 0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b)) = -↑π / b * (↑t + I * c) ^ 2

Tactic:
field_simp
    ring_nf
    simp only [I_sq]
    ring

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ‖x‖ ^ 2) f

Tactic:
simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, fourierMultiplierCLM_sum F this,
    _root_.sum_apply, Finset.smul_sum]

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
⊢ ∑ i, ∂_{b i} (∂_{b i} f) = ∑ x, -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x_1 ↦ inner ℝ x_1 (b x) ^ 2) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
⊢ (fderivCLM 𝕜 V E) (𝓕 f) = 𝓕 (-(2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) f)

Tactic:
ext1 x
  change fderiv ℝ (𝓕 ⇑f) x = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) f) x
  rw [fderiv_fourier f.integrable]
  simpa using f.integrable_pow_mul volume 1

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

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
ι : Sort u_11
p : ι → Prop
s : ι → Set α
x : α
hl : (𝓝 x).HasBasis p s
⊢ x ∉ dsupport f ↔ ∃ i, p i ∧ IsVanishingOn f (s i)

Tactic:
simp [hl.mem_dsupport]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
s : Set α
h : IsVanishingOn f s
s_open : IsOpen[inst✝²] s
⊢ Disjoint s (dsupport f)

Tactic:
rw [← Set.subset_compl_iff_disjoint_right, dsupport_compl_eq]
  exact Set.subset_sUnion_of_mem ⟨h, s_open⟩

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

Goal state before:
pp: case hf
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✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : (toTemperedDistributionCLM F μ p) f = 0
⊢ LocallyIntegrable (↑↑f) μ

Tactic:
exact (Lp.memLp f).locallyIntegrable hp.elim

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

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F₁
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedAddCommGroup F₃
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : BorelSpace E
inst✝⁵ : NormedSpace ℂ F₃
inst✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace F₃
inst✝¹ : NormedSpace ℂ F₁
inst✝ : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ ∫ (y : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) =
    (B (∫ (x : E), 𝐞 (-inner ℝ x ξ) • f₁ x)) (∫ (y : E), 𝐞 (-inner ℝ y ξ) • f₂ y)

Tactic:
← integral_comp_comm _ (by simpa using hf₂),

Goal state after:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F₁
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedAddCommGroup F₃
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : BorelSpace E
inst✝⁵ : NormedSpace ℂ F₃
inst✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace F₃
inst✝¹ : NormedSpace ℂ F₁
inst✝ : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ ∫ (y : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) =
    ∫ (x : E), (B (∫ (x : E), 𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ x ξ) • f₂ x)
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case add
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : { i // n i ≠ 0 }), ZMod (p ↑i ^ n ↑i)
hx :
  (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) x) =
    x
hy :
  (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) y) =
    y
⊢ x +
      (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
        ((directSumNeZeroMulHom p n) y) =
    x + y

Tactic:
hy

Goal state after:
case add
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : { i // n i ≠ 0 }), ZMod (p ↑i ^ n ↑i)
hx :
  (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) x) =
    x
hy :
  (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) y) =
    y
⊢ x + y = x + y
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case add
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : ι), ZMod (p i ^ n i)
hx :
  (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    x
hy :
  (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) y) =
    y
⊢ x +
      (directSumNeZeroMulHom p n)
        ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
          y) =
    x + y

Tactic:
hy

Goal state after:
case add
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : ι), ZMod (p i ^ n i)
hx :
  (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    x
hy :
  (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) y) =
    y
⊢ x + y = x + y
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: case intro
α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
val✝ : Fintype α
⊢ Fintype.card (AddChar α ℂ) = finrank ℂ (α → ℂ)

Tactic:
rw [card_eq, Module.finrank_fintype_fun_eq_card]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
⊢ Bijective ⇑doubleDualEmb

Tactic:
cases nonempty_fintype α
  exact (Fintype.bijective_iff_injective_and_card _).2
    ⟨doubleDualEmb_injective, card_eq.symm.trans card_eq.symm⟩

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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v

Tactic:
have :
    (fun v : V => 𝐞 (-⟪v, w⟫) • f (v + i w)) =
      fun v : V => (fun x : V => -(𝐞 (-⟪x, w⟫) • f x)) (v + i w) := by
    ext1 v
    simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
      ofReal_add, add_mul, exp_add]
    match_scalars
    have H : exp (- (π * I)) = (-1)⁻¹ := by rw [exp_neg, exp_pi_mul_I]
    linear_combination (norm := ring_nf) cexp (-2 * π * ⟪v, w⟫ * I) * H

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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this : (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + i w)) = fun v ↦ (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n

Tactic:
by
  intro h; apply eq; simp only [gcd_coe, mul_coe]
  apply Nat.Coprime.gcd_mul_left_cancel; simpa

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

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
rw [← gcd_eq_left_iff_dvd] at am

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a = (a * b).gcd m
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ μ n ≠ 0 ↔ Squarefree n

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
h : μ n ≠ 0
⊢ Squarefree n

case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0