mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : (i : Fin (n + 1)) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: case e_f
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2) = cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Tactic:
← Complex.exp_add,

Goal state after:
case e_f
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ cexp (-b * ↑p.1 ^ 2 + -b * ↑p.2 ^ 2) = cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ ∀ (i : ι), HasFDerivAt (fun x ↦ ↑polarCoord.symm (x i)) (fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj i) p

Tactic:
exact fun i ↦ HasFDerivAt.comp _ (hasFDerivAt_polarCoord_symm _) (hasFDerivAt_apply i _)

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ EqOn (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) (s + 1).partialGamma (Ici 0)

Tactic:
intro X hX

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = (s + 1).partialGamma X
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ GammaIntegral 1 = 1

pp: ⊢ 0 < re 1

Tactic:
<;>

Goal state after:
⊢ GammaIntegral 1 = 1

⊢ 0 < re 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ (0 + 1).GammaIntegral / 0 = 0

Tactic:
div_zero

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

Goal state before:
pp: case e'_3
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
h'f : Integrable (𝓕 f) volume
v : V
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w =
    (cexp (-↑c⁻¹ * ↑‖w‖ ^ 2) * cexp (↑(2 * π * ⟪w, v⟫) * I)) • 𝓕 f w

Tactic:
← Complex.exp_add,

Goal state after:
case e'_3
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
h'f : Integrable (𝓕 f) volume
v : V
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w = cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + ↑(2 * π * ⟪w, v⟫) * I) • 𝓕 f w
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 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
setIntegral_pos_iff_support_of_nonneg_ae

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

case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 ≤ᵐ[volume.restrict (Ioi 0)] fun x ↦ rexp (-x) * x ^ (s - 1)

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

Goal state before:
pp: case hφ
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 → ℝ := ⋯
⊢ ∀ (x : V), 0 ≤ φ x

Tactic:
exact fun x ↦ by positivity

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

Goal state before:
pp: case e_a.e_a.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
⊢ ↑(finrank ℝ V) / 2 = -↑(finrank ℝ V) / 2 + ↑2 * (↑(finrank ℝ V) / 2)

pp: case e_a.e_a.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
⊢ ↑(finrank ℝ V) = ↑2 * (↑(finrank ℝ V) / 2)

Tactic:
<;>

Goal state after:
case e_a.e_a.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
⊢ ↑(finrank ℝ V) / 2 = -↑(finrank ℝ V) / 2 + ↑2 * (↑(finrank ℝ V) / 2)

case e_a.e_a.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
⊢ ↑(finrank ℝ V) = ↑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:
← Complex.exp_add,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
| cexp (I * t * ↑x + -b * ↑x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I) * cexp (-↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
← Complex.exp_add,

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + (-↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v)) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_2
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x + 0)

pp: case e'_3
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i)) = (↑π / - -b i) ^ (1 / 2) * cexp (0 - c i ^ 2 / (4 * -b i))

Tactic:
<;>

Goal state after:
case e'_2
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x + 0)

case e'_3
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i)) = (↑π / - -b i) ^ (1 / 2) * cexp (0 - c i ^ 2 / (4 * -b i))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ ∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
rw [← (PiLp.volume_preserving_toLp ι).integral_comp
    (MeasurableEquiv.toLp 2 _).measurableEmbedding]
  simp only [neg_mul]
  convert! integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y
  · simp only [EuclideanSpace.norm_eq, norm_eq_abs, sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]
    norm_cast
    left
    rw [sq_sqrt]
    exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
  · simp only [PiLp.inner_apply, RCLike.inner_apply, conj_trivial, ofReal_sum, ofReal_mul,
      Finset.mul_sum, mul_assoc]
    simp_rw [mul_comm]
  · simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]
    congr
    norm_cast
    rw [sq_sqrt]
    exact Finset.sum_nonneg (fun i _hi ↦ by positivity)

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

Goal state before:
pp: case e'_2.e'_7.e'_5
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
x✝ : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ‖e x✝‖ = ‖x✝‖

pp: case e'_2.e'_7.e'_6
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
x✝ : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ⟪w, e x✝⟫ = ⟪e.symm w, x✝⟫

pp: case e'_3.e'_5
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Module.finrank ℝ V = Fintype.card (Fin (Module.finrank ℝ V))

pp: case e'_3.e'_6
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ‖w‖ = ‖e.symm w‖

Tactic:
<;>

Goal state after:
case e'_2.e'_7.e'_5
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
x✝ : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ‖e x✝‖ = ‖x✝‖

case e'_2.e'_7.e'_6
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
x✝ : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ⟪w, e x✝⟫ = ⟪e.symm w, x✝⟫

case e'_3.e'_5
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Module.finrank ℝ V = Fintype.card (Fin (Module.finrank ℝ V))

case e'_3.e'_6
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
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ‖w‖ = ‖e.symm w‖
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case mp
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 : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F (-s)) f = g → (besselPotential E F s) g = f

pp: case mpr
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 : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F s) g = f → (besselPotential E F (-s)) f = g

Tactic:
<;>

Goal state after:
case mp
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 : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F (-s)) f = g → (besselPotential E F s) g = f

case mpr
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 : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F s) g = f → (besselPotential E F (-s)) f = g
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case mp
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 : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F (-s)) f = g
⊢ (besselPotential E F s) g = f

pp: case mpr
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 : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F s) g = f
⊢ (besselPotential E F (-s)) f = g

Tactic:
<;>

Goal state after:
case mp
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 : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F (-s)) f = g
⊢ (besselPotential E F s) g = f

case mpr
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 : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F s) g = f
⊢ (besselPotential E F (-s)) f = g
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ (∫⁻ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}, f fun i ↦ ↑(x i)) =
    ∫⁻ (a_1 : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm a_1) ∂Measure.comap Subtype.val volume

Tactic:
rw [← lintegral_subtype_comap (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc))]
    rfl

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
w : ι → ℝ
f : ι → 𝕜
a : 𝕜
⊢ ⟪f, const ι a⟫_[𝕜, w] = a * ∑ i, w i • (starRingEnd 𝕜) (f i)

Tactic:
by simp [wInner, const_apply, mul_sum]

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

Goal state before:
pp: case h
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ Continuous (⇑f ⋆[B, volume] ⇑g)

Tactic:
refine BddAbove.continuous_convolution_right_of_integrable B ?_ f.integrable g.continuous
      exact ⟨SchwartzMap.seminorm ℝ 0 0 g, fun x ⟨y, hy⟩ ↦ hy ▸ norm_le_seminorm ℝ g y⟩

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

Goal state before:
pp: case h'f
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ Integrable (𝓕 (⇑f ⋆[B, volume] ⇑g)) volume

Tactic:
· have : Integrable (fun ξ ↦ B (𝓕 f ξ) (𝓕 g ξ)) volume := (pairing B (𝓕 f) (𝓕 g)).integrable
      convert! this
      rw [← fourier_convolution_apply B f g, fourier_convolution, pairing_apply_apply]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

pp: case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ 1 / 2

pp: case hy
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ x

Tactic:
<;>

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ 1 / 2

case hy
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ x
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
n : ℕ
⊢ μ n ≠ 0 → Squarefree n

pp: case mpr
n : ℕ
⊢ Squarefree n → μ n ≠ 0

Tactic:
<;>

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

case mpr
n : ℕ
⊢ Squarefree n → μ n ≠ 0
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 < 1 / 2 * x

pp: case hxy
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 1 / 2 * x ≤ y

pp: case hz
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ -b ≤ 0

Tactic:
<;>

Goal state after:
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 < 1 / 2 * x

case hxy
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 1 / 2 * x ≤ y

case hz
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ -b ≤ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (↑ζ • f') (n + 1) = g' (n + 1)

Tactic:
rw [coe_zeta_smul_apply]
      simp only [forall_prop_of_true, succ_pos', f', g', coe_mk, succ_ne_zero, ite_false]
      rw [sum_congr rfl fun x hx => if_neg (pos_of_mem_divisors hx).ne']

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' → μ • g' = f'

pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' → ↑ζ • f' = g'

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' → μ • g' = f'

case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' → ↑ζ • f' = g'
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : ↑ζ • f' = g'
⊢ μ • g' = f'

pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : μ • g' = f'
⊢ ↑ζ • f' = g'

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : ↑ζ • f' = g'
⊢ μ • g' = f'

case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : μ • g' = f'
⊢ ↑ζ • f' = g'