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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
hg_upper : ∃ k C, ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
⊢ ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F)) (x : D),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (⇑f ∘ g) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
rintro ⟨k, n⟩
  rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩
  rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
  have hCg : 1 ≤ 1 + Cg := by
    refine le_add_of_nonneg_right ?_
    specialize hg_upper' 0
    rw [norm_zero] at hg_upper'
    exact nonneg_of_mul_nonneg_left hg_upper' (by positivity)
  let k' := kg * (k + l * n)
  use Finset.Iic (k', n), (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * n ! * 2 ^ k'), by positivity
  intro f x
  let seminorm_f := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 _ _)) f
  have hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k' := by
    rw [pow_mul, ← mul_pow]
    gcongr
    rw [add_mul]
    refine add_le_add ?_ (hg_upper' x)
    nth_rw 1 [← one_mul (1 : ℝ)]
    gcongr
    apply one_le_pow₀
    simp only [le_add_iff_nonneg_right, norm_nonneg]
  have hbound (i) (hi : i ≤ n) :
      ‖iteratedFDeriv ℝ i f (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k' := by
    have hpos : 0 < (1 + ‖g x‖) ^ k' := by positivity
    rw [le_div_iff₀' hpos]
    change i ≤ (k', n).snd at hi
    exact one_add_le_sup_seminorm_apply le_rfl hi _ _
  have hgrowth' (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n) :
      ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N := by
    refine (hgrowth N hN₂ x).trans ?_
    rw [mul_pow]
    have hN₁' := (lt_of_lt_of_le zero_lt_one hN₁).ne'
    gcongr
    · exact le_trans (by simp) (le_self_pow₀ (by simp [hC]) hN₁')
    · refine le_self_pow₀ (one_le_pow₀ ?_) hN₁'
      simp only [le_add_iff_nonneg_right, norm_nonneg]
  have := norm_iteratedFDeriv_comp_le (f.smooth ⊤) hg.1 (mod_cast le_top) x hbound hgrowth'
  have hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k :=
    pow_le_pow_left₀ (norm_nonneg _) (by simp only [zero_le_one, le_add_iff_nonneg_left]) _
  grw [hxk, this]
  have rearrange :
    (1 + ‖x‖) ^ k *
        (n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
      (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' *
        ((C + 1) ^ n * n ! * 2 ^ k' * seminorm_f) := by
    rw [mul_pow, pow_add, ← pow_mul]
    ring
  rw [rearrange]
  have hgxk' : 0 < (1 + ‖g x‖) ^ k' := by positivity
  rw [← div_le_iff₀ hgxk'] at hg_upper''
  grw [hg_upper'', ← mul_assoc]

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

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

Tactic:
filter_upwards with v
    fun_prop

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

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) = ‖c • x‖ ^ finrank ℝ F * φ (c • x)

Tactic:
by
        simp [norm_smul, abs_of_pos cpos, mul_pow]; ring

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
C : ℝ
left✝ : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
x : E
⊢ ‖f x‖ ≤ C

Tactic:
simpa using hC x

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
this :
  |((innerSL ℝ) w) w| ^ n *
      ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 volume (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f) w‖ ≤
    ‖w‖ ^ n * (2 * π * ‖innerSL ℝ‖) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume
⊢ ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))

Tactic:
simp only [innerSL_apply_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
      mul_assoc] at this

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
this :
  (‖w‖ ^ 2) ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 volume (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f) w‖ ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume))
⊢ ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ (fun x ↦ rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-x)

Tactic:
exact exp_neg_mul_rpow_isLittleO_exp_neg hb one_lt_two

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

Goal state before:
pp: case inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

Tactic:
right

Goal state after:
case inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | q.2 ≠ 0}
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ AEStronglyMeasurable (fun x ↦ (-x) ^ s * rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Tactic:
apply Measurable.aestronglyMeasurable
    exact (measurable_id'.neg.pow measurable_const).mul
      ((measurable_id'.pow measurable_const).const_mul (-b)).exp

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

Goal state before:
pp: case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ 0 ≤ ↑k

Tactic:
rw [← Nat.cast_zero, Nat.cast_le]

Goal state after:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ 0 ≤ k
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e'_5
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
⊢ 𝓕⁻ (𝓕 f) v = ∫ (v_1 : V), 𝐞 ⟪v_1, v⟫ • 𝓕 f v_1

Tactic:
simp [fourierInv_eq]

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

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ ∏ x, (↑π / b) ^ 2⁻¹ * cexp (c x ^ 2 / (4 * b)) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))

Tactic:
Finset.prod_mul_distrib,

Goal state after:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ (∏ x, (↑π / b) ^ 2⁻¹) * ∏ x, cexp (c x ^ 2 / (4 * b)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

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

Tactic:
simp [fourier_evalCLM_eq ℝ, fourier_fderivCLM_eq, this, innerSL_apply_apply ℝ]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
r : ℝ
x : E
f : 𝓢'(E, F)
⊢ ∂_{r • x} f = r • ∂_{x} f

Tactic:
ext u
    simp [lineDerivOp_left_smul, map_smul_of_tower f]

Goal state after:
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
⊢ MemSobolev s 2 f → ∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'

Tactic:
intro ⟨f', hf'⟩
    use 𝓕 f'
    apply_fun 𝓕 at hf'
    rw [fourier_besselPotential_eq_smulLeftCLM_fourier_apply] at hf'
    rw [hf', Lp.fourier_toTemperedDistribution_eq f']

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ↑(mFourierBasis.repr f) i = mFourierCoeff (↑↑f) i

Tactic:
trans ∫ t, conj (mFourierLp 2 i t) * f t
  · rw [mFourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_mFourierBasis]
    simp only [RCLike.inner_apply, mul_comm]
  · apply integral_congr_ae
    filter_upwards [coeFn_mFourierLp 2 i] with _ ht
    rw [ht, ← mFourier_neg, smul_eq_mul]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ ⟪f₁, g⟫_[𝕜, w] + ⟪-f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + -⟪f₂, g⟫_[𝕜, w]

Tactic:
wInner_neg_left

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

Goal state before:
pp: case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ cardFactors n = 0 ∨ (-1) ^ cardFactors n = 1 ∨ (-1) ^ cardFactors n = -1

Tactic:
right

Goal state after:
case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ cardFactors n = 1 ∨ (-1) ^ cardFactors n = -1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ d ∈ n.divisors, ↑μ d * f d = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
intCoe_apply

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

Goal state before:
pp: case coprime
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ 1 a * 1 b = 1 (a * b)

pp: a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ).IsMultiplicative

Tactic:
IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab

Goal state after:
case coprime
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ 1 a * 1 b = 1 a * 1 b

a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ).IsMultiplicative
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
⊢ ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε

Tactic:
obtain ⟨δ, hδ1, hδ2⟩ :=
    Metric.uniformContinuous_iff.mp (hf2.uniformContinuous_of_continuous hf1) (ε / B)
      (div_pos hε hB_pos)

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

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ -l

Tactic:
← hl'

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i / ↑n - ↑n / ↑n) * (2 * ↑Real.pi)

Tactic:
div_self

Goal state after:
case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i / ↑n - 1) * (2 * ↑Real.pi)

case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i / ↑n - ↑n / ↑n) * (2 * ↑Real.pi)

Tactic:
div_self

Goal state after:
case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i / ↑n - 1) * (2 * ↑Real.pi)

case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ μ.addHaarScalarFactor volume • ∫ (v : V), 𝐞 (-w v) • f v ∂volume) (cocompact (StrongDual ℝ V))
    (𝓝 (μ.addHaarScalarFactor volume • 0))

Tactic:
apply Tendsto.const_smul

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun x ↦ ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (StrongDual ℝ V)) (𝓝 0)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case refine_2
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
a✝ : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ m)) i)
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n * x)) i)

Tactic:
exact repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ False

Tactic:
replace h : n * p = n * 1 := by simp [h]

Goal state after:
case inr.refine_1.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n * 1
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'

Goal state after:
case inr.refine_1.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b n✝
⊢ IsPrimitiveRoot ((algebraMap B C) b) n✝

Tactic:
exact hb.map_of_injective h

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
right

Goal state after:
case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = adjoin A (Subtype.val ⁻¹' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

Tactic:
preimage_ofPred_eq

Goal state after:
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = adjoin A {a | ∃ a_1 ∈ S, a_1 ≠ 0 ∧ ↑a ^ a_1 = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₁ : Finite ↑S
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B

Tactic:
rw [finite_coe_iff] at h₁
  induction S, h₁ using Set.Finite.induction_on generalizing h₂ A B with
  | empty =>
    refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
    simp [← top_toSubmodule, ← subsingleton_iff_bot_eq_top.mpr inferInstance,
      toSubmodule_bot, Submodule.one_eq_span]
  | @insert n S _ _ H =>
    by_cases hn : n = 0
    · have : insert n S \ {0} = S \ {0} := by simp_all
      rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂
      exact H A B
    have : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) :=
        union_left _ (insert n S) _ _ (subset_insert n S)
    have := H A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1})
    have : Module.Finite (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) B := by
      rw [← union_singleton] at h₂
      let _ := union_right S {n} A B
      have : NeZero n := ⟨hn⟩
      exact finite_of_singleton n _ _
    exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _

Goal state after:
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this : Finite K
⊢ (algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
have := ofFinite K

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this✝ : Finite K
this : Fintype K
⊢ (algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this : Finite K
⊢ (algebraMap K L) ((Algebra.norm K) x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
have := ofFinite K

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this✝ : Finite K
this : Fintype K
⊢ (algebraMap K L) ((Algebra.norm K) x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i