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

Goal state before:
pp: 𝕜 : Type u_2
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    ↑((eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ).toNNReal * 2 ^ k) *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ∀ (x : ↑(Icc (↑n) (↑n + 1))), ‖f ↑x‖ ≤ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Tactic:
intro x

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
⊢ ‖f ↑x‖ ≤ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ DenseRange ⇑(toLpCLM ℝ F p μ)

Tactic:
intro f
  refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
  obtain ⟨g, hg₁, hg₂, hg₃⟩ := MemLp.exist_eLpNorm_sub_le hp hp'.out (Lp.memLp f) hε
  use (hg₁.toSchwartzMap hg₂).toLp p μ
  have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᵐ[μ] (f : E → F) - g := by
    filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]
    simp
  simp only [Set.mem_range, toLpCLM_apply, exists_apply_eq_apply, Metric.mem_closedBall', true_and,
    Lp.dist_def, eLpNorm_congr_ae this]
  grw [hg₃, ENNReal.toReal_ofReal hε.le]
  simp

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

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x

Tactic:
intro x

Goal state after:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
⊢ x ∈ Ici c → HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun t ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x

Tactic:
intro x

Goal state after:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
⊢ x ∈ Ici c → HasDerivAt (fun t ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
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
hf : MemLp f 1 volume
⊢ ⇑(Lp.fourierTransform (MemLp.toLp f hf)) = 𝓕 f

Tactic:
by
  simp only [Lp.coe_fourierTransform]
  ext x
  exact (Real.fourier_congr_ae hf.coeFn_toLp) x

Goal state after:
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), ‖({ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ } f) x‖ ≤ ‖f‖

Tactic:
intro x

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
⊢ ‖({ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ } f) x‖ ≤ ‖f‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
⊢ ∀ x ∈ Ioi 0, ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x

Tactic:
intro x

Goal state after:
case left
s : ℂ
hs : 0 < s.re
x : ℝ
⊢ x ∈ Ioi 0 → ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ EqOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (↑s - 1)) (fun x ↦ ↑(rexp (-x) * x ^ (s - 1))) (Ioi 0)

Tactic:
intro x

Goal state after:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
⊢ x ∈ Ioi 0 → (fun x ↦ ↑(rexp (-x)) * ↑x ^ (↑s - 1)) x = (fun x ↦ ↑(rexp (-x) * x ^ (s - 1))) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ x ∈ Ioc 0 Y, ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x

Tactic:
intro x

Goal state after:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
⊢ x ∈ Ioc 0 Y → ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case refine_1
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
z : ℂ
hz : z ∈ Complex.slitPlane
⊢ ContinuousWithinAt Complex.arg Complex.slitPlane z

Tactic:
exact (Complex.continuousAt_arg hz).continuousWithinAt

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x

Tactic:
intro x

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
⊢ x ∈ Ioo 0 X →
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker

Tactic:
intro x

Goal state after:
x : ℝ × ℝ
⊢ x ∈ polarCoord.sourceᶜ → x ∈ ↑(LinearMap.snd ℝ ℝ ℝ).ker
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
⊢ ∀ (x : ℂ), HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x

Tactic:
intro x

Goal state after:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ EqOn (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) (fun e ↦ e ^ s.re * rexp (-1 * e)) (Ioi 0)

Tactic:
intro x

Goal state after:
s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
⊢ x ∈ Ioi 0 → (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) x = (fun e ↦ e ^ s.re * rexp (-1 * e)) x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_7
b : ℝ
hb : 0 < b
x : ℝ
⊢ ↑(rexp (-b * x ^ 2)) = cexp (-↑b * ↑x ^ 2)

Tactic:
ofReal_exp,

Goal state after:
case e'_7
b : ℝ
hb : 0 < b
x : ℝ
⊢ cexp ↑(-b * x ^ 2) = cexp (-↑b * ↑x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

Tactic:
by
  -- First we deal with the crazy case where `b ≤ 0`: then both sides vanish.
  rcases le_or_gt b 0 with (hb | hb)
  · rw [integral_undef, sqrt_eq_zero_of_nonpos]
    · exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb
    · simpa only [not_lt, integrable_exp_neg_mul_sq_iff] using hb
  -- Assume now `b > 0`. Then both sides are non-negative and their squares agree.
  refine (sq_eq_sq₀ (by positivity) (by positivity)).1 ?_
  rw [← ofReal_inj, ofReal_pow, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, ← integral_ofReal,
    sq_sqrt (div_pos pi_pos hb).le, ← RCLike.algebraMap_eq_ofReal, coe_algebraMap, ofReal_div]
  convert! integral_gaussian_sq_complex (by rwa [ofReal_re] : 0 < (b : ℂ).re) with _ x
  rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))

Tactic:
intro x

Goal state after:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
x : ℝ
⊢ cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1)) * ((starRingEnd ℂ) s)⁻¹

Tactic:
← div_eq_mul_inv

Goal state after:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1)) / (starRingEnd ℂ) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
ofReal_exp,

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

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ Ioi 0 ⊆ Function.support fun x ↦ rexp (-x) * x ^ (s - 1)

Tactic:
intro x

Goal state after:
s : ℝ
hs : 0 < s
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ Function.support fun x ↦ rexp (-x) * x ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < ⊤

Tactic:
← ENNReal.ofReal_zero

Goal state after:
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ ENNReal.ofReal 0 < ⊤
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case hfi
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
exact GammaIntegral_convergent hs

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

Goal state before:
pp: s : ℝ
hs : 0 ≤ s
⊢ 0 ≤ Gamma s

Tactic:
obtain rfl | h := eq_or_lt_of_le hs

Goal state after:
case inl
hs : 0 ≤ 0
⊢ 0 ≤ Gamma 0

case inr
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) =
    π ^ (-↑(finrank ℝ V) / 2) * π ^ (↑2 * (↑(finrank ℝ V) / 2)) * ‖x‖ ^ (↑2 * (↑(finrank ℝ V) / 2))

Tactic:
← rpow_add pi_pos,

Goal state after:
case e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) =
    π ^ (-↑(finrank ℝ V) / 2 + ↑2 * (↑(finrank ℝ V) / 2)) * ‖x‖ ^ (↑2 * (↑(finrank ℝ V) / 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
| ∫ (x : ℝ), cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2)

Tactic:
2,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
| fun x ↦ cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑((c ^ (1 / 2)) ^ finrank ℝ V) * (↑(π ^ (↑(finrank ℝ V) / 2)) * ↑(rexp (-π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2))) =
    (↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)

Tactic:
ofReal_exp,

Goal state after:
case e_f.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑((c ^ (1 / 2)) ^ finrank ℝ V) * (↑(π ^ (↑(finrank ℝ V) / 2)) * cexp ↑(-π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2)) =
    (↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
by
  let e := (stdOrthonormalBasis ℝ V).repr.symm
  rw [← e.measurePreserving.integral_comp e.toHomeomorph.measurableEmbedding]
  convert! integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w) <;>
    simp [LinearIsometryEquiv.inner_map_eq_flip]

Goal state after:
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
inst✝ : CompleteSpace E
⊢ ∀ (f : 𝓢(V, E)), 𝓕⁻ (𝓕 f) = f

Tactic:
intro f
    ext x
    rw [fourierInv_coe, fourier_coe, f.continuous.fourierInv_fourier_eq f.integrable
      (𝓕 f).integrable]

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
x : α
⊢ x ∈ dsupport f ↔ ∃ᶠ (u : Set α) in (𝓝 x).smallSets, ¬IsVanishingOn f u

Tactic:
nhds_basis_opens x |>.frequently_smallSets not_isVanishingOn_mono

Goal state after:
α : 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
x : α
⊢ x ∈ dsupport f ↔ ∀ (i : Set α), x ∈ i ∧ IsOpen[inst✝²] i → ¬IsVanishingOn f i
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:
← Set.subset_compl_iff_disjoint_right,

Goal state after:
α : 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
⊢ s ⊆ (dsupport f)ᶜ
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s

Tactic:
by
  intro u hu
  apply hf ((SchwartzMap.smulLeftCLM ℂ g) u)
  rw [SchwartzMap.smulLeftCLM_apply hg]
  exact (tsupport_smul_subset_right g u).trans hu

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

Goal state before:
pp: case hp.hg
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ toTemperedDistribution (𝓕 y)

Tactic:
exact (toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s s' : ℝ
⊢ besselPotential E F s' ∘SL besselPotential E F s = besselPotential E F (s + s')

Tactic:
by
  ext f : 1
  exact besselPotential_besselPotential_apply s s' f

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

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

Goal state before:
pp: case e'_2.e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
e_2✝ : MeasureSpace.pi.toMeasurableSpace = MeasurableSpace.pi
⊢ volume = Measure.map (⇑(measurableEquivPiIoc a).symm) (Measure.comap Subtype.val volume)

Tactic:
exact (measurePreserving_equivPiIoc a).symm.map_eq.symm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
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✝² : NormedSpace 𝕜 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
⊢ 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₂ ⋆[B.flip, volume] f₁) ξ

Tactic:
convolution_flip

Goal state after:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
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✝² : NormedSpace 𝕜 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
⊢ 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₁ ⋆[B, volume] f₂) ξ
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case e'_2.e'_6
d : Type u_1
inst✝² : Fintype d
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
e_5✝ : MeasureSpace.pi.toMeasurableSpace = MeasurableSpace.pi
⊢ volume = Measure.map (⇑(measurableEquivPiIoc a).symm) (Measure.comap Subtype.val volume)

Tactic:
exact (measurePreserving_equivPiIoc a).symm.map_eq.symm

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ₑ < ∞
x✝ : E
⊢ ((1 + ‖x✝‖ ^ 2) ^ (-s / 2)) ^ 2 = (1 + ‖x✝‖ ^ 2) ^ (-s)

Tactic:
rw [← Real.rpow_mul_natCast (by positivity)]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ₑ < ∞
x✝ : E
⊢ (1 + ‖x✝‖ ^ 2) ^ (-s / 2 * ↑2) = (1 + ‖x✝‖ ^ 2) ^ (-s)
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ∀ (x y : ZMod n), zmod n (x + y) = zmod n x * zmod n y

Tactic:
simp [DFunLike.ext_iff, zmod, add_mul, map_add_eq_mul]

Goal state after: