mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x ↦ (-2 * ↑π * I * ↑x) • f x) w) w

Tactic:
have hf'' : Integrable (fun v : ℝ ↦ ‖v‖ * ‖f v‖) := by simpa only [norm_smul] using! hf'.norm
  let L := ContinuousLinearMap.mul ℝ ℝ |>.flip
  have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
    suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
      simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using! this.smul (-2 * π * I)
    convert! ((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
    apply ContinuousLinearMap.ext_ring
    rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]
    exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm
  convert! (VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt using 1
  rw [fourierIntegral_continuousLinearMap_apply' h_int, VectorFourier.fourierIntegral,
    fourier_real_eq]
  simp [fourierSMulRight, L, smul_apply,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.mul_apply', ← neg_mul, mul_smul]

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
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 → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
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 → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable ((fun x ↦ ∏ i, f i (x i)) ∘ ⇑(Fin.insertNthEquiv E 0))
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))

Tactic:
Fin.insertNthEquiv,

Goal state after:
case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
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 → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
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 → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable
    ((fun x ↦ ∏ i, f i (x i)) ∘
      ⇑{ toFun := fun f ↦ Fin.insertNth 0 f.1 f.2, invFun := fun f ↦ (f 0, Fin.removeNth 0 f), left_inv := ⋯,
          right_inv := ⋯ })
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : 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 : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      ∏ x_1, f x_1 ((Fin.insertNthEquiv E 0) x x_1) ∂(μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)

Tactic:
Fin.insertNthEquiv,

Goal state after:
𝕜 : 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 : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      ∏ x_1,
        f x_1
          ({ toFun := fun f ↦ Fin.insertNth 0 f.1 f.2, invFun := fun f ↦ (f 0, Fin.removeNth 0 f), left_inv := ⋯,
              right_inv := ⋯ }
            x x_1) ∂(μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:

Tactic:
_ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]

Goal state after:
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)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ ∫ (x : (i : ι) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
← (measurePreserving_piCongrLeft _ e).integral_comp'

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 : (b : Fin (card ι)) → E (e b)),
      ∏ i, f i ((MeasurableEquiv.piCongrLeft E e) x i) ∂Measure.pi fun i' ↦ μ (e i')) =
    ∏ i, ∫ (x : E i), f i x ∂μ i
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
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖-↑x ^ s * ↑(rexp (-x))‖ = x ^ s.re * rexp (-1 * x)

Tactic:
rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]

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

Goal state before:
pp: case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s * s.GammaIntegral / s

Tactic:
mul_comm,

Goal state after:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s.GammaIntegral * s / s
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x ↦ measurableEquivRealProd.symm
this : MeasurePreserving (fun a i ↦ measurableEquivRealProd.symm (a i)) volume volume
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ Complex.polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i ↦ ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Tactic:
← MeasurePreserving.lintegral_comp_emb this e.measurableEmbedding

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x ↦ measurableEquivRealProd.symm
this : MeasurePreserving (fun a i ↦ measurableEquivRealProd.symm (a i)) volume volume
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ Complex.polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i ↦ ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (a : ι → ℝ × ℝ), f fun i ↦ measurableEquivRealProd.symm (a i) ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ -s.re < ↑n

Tactic:
simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)

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))
| 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
conv =>
        congr
        rw [mul_comm]
      rw [mul_assoc]

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))
| |c| * (2 * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2)))
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 : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
⊢ 1 * ‖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:
one_mul,

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
absy : |y| ≤ |c|
⊢ ‖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.Fourier.Inversion

Goal state before:
pp: 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
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
⊢ Tendsto (fun c ↦ ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop
    (𝓝 (𝓕⁻ (𝓕 f) v))

Tactic:
have B : Tendsto (fun (c : ℝ) ↦ (∫ w : V,
        𝓕 (fun w ↦ cexp (- c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) w • f w)) atTop
      (𝓝 (𝓕⁻ (𝓕 f) v)) := by
    apply A.congr'
    filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
    have J : Integrable (fun w ↦ cexp (- c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) :=
      GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (by simpa) _ _
    simpa using! (VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ V)
      Real.continuous_fourierChar continuous_inner J hf).symm

Goal state after:
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
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto (fun c ↦ ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
⊢ Tendsto (fun c ↦ ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop
    (𝓝 (𝓕⁻ (𝓕 f) v))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
by
    apply this
    swap
    · exact ⌊-s⌋₊ + 1
    rw [neg_lt, Nat.cast_add, Nat.cast_one]
    exact Nat.lt_floor_add_one _

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

Goal state before:
pp: case e'_3
⊢ √π = 2 * √π / 2

Tactic:
mul_comm,

Goal state after:
case e'_3
⊢ √π = √π * 2 / 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (0 - (I * t) ^ 2 / (4 * -b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
zero_sub,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (-((I * t) ^ 2 / (4 * -b))) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.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 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)) = ↑π ^ (↑(finrank ℝ V) / 2) * ↑c ^ (↑(finrank ℝ V) / 2)

Tactic:
mul_comm,

Goal state after:
case e_f.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 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
⊢ ↑(π ^ (↑(finrank ℝ V) / 2)) * ↑(c ^ (1 / 2 * ↑(finrank ℝ V))) = ↑π ^ (↑(finrank ℝ V) / 2) * ↑c ^ (↑(finrank ℝ V) / 2)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case h₁
𝕜 : 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
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (SchwartzMap.seminorm 𝕜 0 p.2) f ≤
    ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f

Tactic:
have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all

Goal state after:
case h₁
𝕜 : 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
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
this : (0, p.2) ∈ Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)
⊢ (SchwartzMap.seminorm 𝕜 0 p.2) f ≤
    ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ‖(𝓕 f).toBoundedContinuousFunction‖ ≤ ‖f.toLp 1 volume‖

Tactic:
rw [BoundedContinuousFunction.norm_le (by positivity)]
  simpa using norm_fourier_apply_le_toLp_one f

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

Goal state before:
pp: E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
⊢ dsupport ⇑(delta x) = {x}

Tactic:
apply subset_antisymm
  · intro x' hx'
    rw [mem_dsupport_iff] at hx'
    exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)
  rintro x rfl
  rw [mem_dsupport_iff_forall_exists_ne]
  intro s hxs hs
  set t := s ∩ Ω
  have ht : IsOpen t := hs.inter Ω.isOpen
  have htx : x ∈ t := Set.mem_inter hxs hx
  obtain ⟨u, h₁, h₂, h₃, -, h₄⟩ :=
    exists_contDiff_tsupport_subset (n := n) ((IsOpen.mem_nhds_iff ht).mpr htx)
  exact ⟨⟨u, h₃, h₂, by aesop⟩, ⟨by aesop, by simp [h₄]⟩⟩

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
n : d → ℤ
x : UnitAddTorus d
m : d → ℤ
⊢ (mFourier (m + n)) x = (mFourier m) x * (mFourier n) x

Tactic:
simp only [mFourier, Pi.add_apply, fourier_add, ContinuousMap.coe_mk, ← Finset.prod_mul_distrib]

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹⁷ : RCLike 𝕜
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : InnerProductSpace ℝ E
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
inst✝¹¹ : NormedAddCommGroup F₁
inst✝¹⁰ : NormedSpace ℂ F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : SMulCommClass ℂ 𝕜 F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace ℂ F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : SMulCommClass ℂ 𝕜 F₂
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace ℂ F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
⊢ ∀ (m : 𝕜) (x : 𝓢(E, F₁)),
    fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 (m • x)) ∘SL fourierCLM 𝕜 𝓢(E, F₂) =
      (RingHom.id 𝕜) m • fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 x) ∘SL fourierCLM 𝕜 𝓢(E, F₂)

Tactic:
by simp [FourierTransform.fourier_smul]

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

Goal state before:
pp: p q : Primes
h : ↑p = ↑q
⊢ ↑p = ↑q

Tactic:
by injection h

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

Goal state before:
pp: l : ℕ
hl : Squarefree l
⊢ (-1) ^ (cardFactors l * 2) = 1

Tactic:
mul_comm,

Goal state after:
l : ℕ
hl : Squarefree l
⊢ (-1) ^ (2 * cardFactors l) = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: ⊢ ↑ζ * μ = 1

Tactic:
mul_comm,

Goal state after:
⊢ μ * ↑ζ = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
⊢ (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
refine
      Iff.trans
        (Iff.trans (forall_congr' fun n => ?_)
          (@prod_eq_iff_prod_pow_moebius_eq_on Rˣ _
            (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1)
            (fun n => if h : 0 < n then Units.mk0 (g n) (hg n h) else 1)
            s hs))
        (forall_congr' fun n => ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
⊢ n > 0 → n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n > 0 →
      n ∈ s →
        (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
⊢ (n > 0 →
      n ∈ s →
        ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
          if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n > 0 → n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) ⟨y, hy⟩‖ =
    ‖(ContinuousMap.restrict (Icc (x - r) (x + r)) f) ⟨y + x, ?refine_2⟩‖

Tactic:
ContinuousMap.restrict_apply,

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖(f.comp (ContinuousMap.addRight x)) y‖ = ‖f (y + x)‖
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (↑q.num / ↑q.den / 2).den

Tactic:
mul_comm,

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ q.den * 2 = (↑q.num / ↑q.den / 2).den
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
    cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
by rw [mul_comm]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ i_1,
    (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))).arg = ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ i_1.natAbs < n

Tactic:
mul_comm,

Goal state after:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ i_1,
    (Complex.exp (↑i / ↑n * (2 * ↑Real.pi * Complex.I))).arg = ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ i_1.natAbs < n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case left
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ B * cyclotomic' k K = X ^ k - 1

Tactic:
mul_comm,

Goal state after:
case left
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ cyclotomic' k K * B = X ^ k - 1
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable

Tactic:
by
  have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 := by
    convert! _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
    simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
  refine Separable.of_dvd (separable_X_pow_sub_C 1 ?_ one_ne_zero) hdvd
  by_contra hzero
  exact hdiv ((ZMod.natCast_eq_zero_iff n p).1 hzero)

Goal state after: