mathlib-initiative/mathlib-tactics huggingface dataset:
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
A : W ≃ₗᵢ[ℝ] V
f : V → E
w : W
⊢ 𝓕 (f ∘ ⇑A) w = 𝓕 f (A w)

Tactic:
by
  simp only [fourier_eq, ← A.inner_map_map, Function.comp_apply,
    ← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding]

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

Goal state before:
pp: a b : ℝ
h : 0 < b
⊢ Tendsto (fun x ↦ rexp (-b * x)) atTop (𝓝 0)

Tactic:
exact tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (neg_neg_iff_pos.2 h))

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

Goal state before:
pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ⋯
v : ℝ
⊢ ((L v).smulRight (f v)) 1 = (↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (v • f v)) 1

Tactic:
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]

Goal state after:
case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
v : ℝ
⊢ v • f v = (v • ↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (f v)) 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume

Tactic:
have hib : 0 < b ^ (-p⁻¹) := rpow_pos_of_pos hb _
  suffices IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * exp (-x ^ p))) (Ioi 0) by
    rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]
    refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi
    #adaptation_note /-- 2026-05-17(kmill) added `dsimp only` because a slightly different
    instantiation order leads to a term with a beta redex.
    https://github.com/leanprover/lean4/pull/13762
    This will be removed once app elaboration itself does beta reduction. -/
    dsimp only
    rw [← mul_assoc, mul_rpow, mul_rpow, ← rpow_mul (z := p), neg_mul, neg_mul, inv_mul_cancel₀,
      rpow_neg_one, mul_inv_cancel_left₀]
    all_goals linarith [mem_Ioi.mp hx]
  refine Integrable.const_mul ?_ _
  rw [← IntegrableOn]
  exact integrableOn_rpow_mul_exp_neg_rpow hs hp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i ↦ polarCoord.source) =ᵐ[volume] Set.univ

Tactic:
volume_pi,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i ↦ polarCoord.source) =ᵐ[Measure.pi fun x ↦ volume] Set.univ
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
⊢ Tendsto (fun X ↦ -↑X ^ s * ↑(rexp (-X))) atTop (𝓝 0)

Tactic:
tendsto_zero_iff_norm_tendsto_zero

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

Goal state before:
pp: case inr
b : ℝ
hb : 0 < b
⊢ ↑(∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = ↑(√(π / b) ^ 2)

Tactic:
← coe_algebraMap,

Goal state after:
case inr
b : ℝ
hb : 0 < b
⊢ (algebraMap ℝ ℂ) (∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = (algebraMap ℝ ℂ) (√(π / b) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
← coe_algebraMap,

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

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (1 / ↑r) ^ a = (1 / ↑r) ^ (1 + (a - 1))

Tactic:
add_sub_cancel

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (1 / ↑r) ^ a = (1 / ↑r) ^ a
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (verticalIntegral b c) atTop (𝓝 0)

Tactic:
tendsto_zero_iff_norm_tendsto_zero

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ ‖verticalIntegral b c x‖) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T ↦ b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2) atTop atTop

Tactic:
apply tendsto_atTop_add_const_right

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ b.re * x ^ 2 - 2 * |b.im| * |c| * x) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
rw [Function.mem_support]

Goal state after:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s - 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_2
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ ↑(∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)

Tactic:
change ofRealLI (∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)
    rw [← ofRealLI.integral_comp_comm]
    simp [ofRealLI]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
g : E → ℂ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F g) ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ((SchwartzMap.fourierMultiplierCLM F g) f)

Tactic:
ext u
  simp [SchwartzMap.integral_fourier_smul_eq, SchwartzMap.fourierMultiplierCLM_apply g f,
    ← SchwartzMap.integral_fourierInv_smul_eq, hg, smul_smul, mul_comm]

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

Goal state before:
pp: 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)
⊢ 𝓕 (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)

Tactic:
set p := fun f : Lp (α := E) F 2 ↦ 𝓕 (f : 𝓢'(E, F)) = (𝓕 f : Lp (α := E) F 2)

Goal state after:
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 := fun f ↦ 𝓕 (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ 𝓕 (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : Multiplicative W
v : V
⊢ ((charMonoidHom he hL) w) v = ↑(e ((L v) (Multiplicative.toAdd w)))

Tactic:
simp [charMonoidHom]

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

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ (derivCLM F) ((toTemperedDistributionCLM ℝ F volume) f) =
    (toTemperedDistributionCLM ℝ F volume) ((SchwartzMap.derivCLM 𝕜 F) f)

Tactic:
by
  ext1 g
  simp [integral_smul_deriv_right_eq_neg_left, integral_neg]

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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ MemSobolev s' 2 f

Tactic:
rw [hs, ← memSobolev_besselPotential_iff]

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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ MemSobolev s 2 ((besselPotential E F (s' - s)) f)
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x

Tactic:
· simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]

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

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n

Tactic:
apply Nat.Coprime.coprime_dvd_left

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

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : ξ ∈ rootsOfUnity k R
⊢ ∃ n, ζ ^ n = ξ

Tactic:
rwa [← h.zpowers_eq] at hξ

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

Goal state before:
pp: case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one

Goal state after:
case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a

Tactic:
rw [← Finset.range_val,
      ← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα), Finset.val_le_iff_val_subset]

Goal state after:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (image (fun x ↦ ζ ^ x * α) (range n)).val ⊆ nthRoots n a
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
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this✝ : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B
bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * volume.real A
this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ volume.real A < 2 * ↑B

Tactic:
refine (ENNReal.toReal_mono ENNReal.coe_ne_top hB_vol).trans_lt ?_

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
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this✝ : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B
bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * volume.real A
this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ (↑B).toReal < 2 * ↑B
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case pos
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : dist (∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) 0 < ε / 2
⊢ dist (∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) 0 < ε

Tactic:
rw [dist_eq_norm] at hI ⊢

Goal state after:
case pos
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - 0‖ < ε
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ cyclotomic n R = (cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
(div_modByMonic_unique (cyclotomic n R) 0 prod_monic _).1

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ cyclotomic n R = cyclotomic n R

R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * cyclotomic n R =
      cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case pos.e_a
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ n = #(nthRootsFinset n 1)

Tactic:
h.card_nthRootsFinset

Goal state after:
case pos.e_a
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ n = n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case e'_2
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = eval (x / y) (X ^ n - 1) * y ^ #(nthRootsFinset n 1)

Tactic:
simp [sub_mul, div_pow, hy, h.card_nthRootsFinset]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ IsIntegral R ((B.basis.repr ((algebraMap K S) ((algebraMap R K) (P.coeff n)) * B.gen ^ n)) i)

Tactic:
← Algebra.smul_def,

Goal state after:
K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ IsIntegral R ((B.basis.repr ((algebraMap R K) (P.coeff n) • B.gen ^ n)) i)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
hn : ¬n = 2
⊢ (Algebra.norm K) ζ = 1

Tactic:
· exact hζ.norm_eq_one hn hirr

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ ↑(eval (↑1) (cyclotomic n ℤ)) = ↑(eval 1 (cyclotomic n ℤ))

Tactic:
Int.cast_id

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ ↑(eval 1 (cyclotomic n ℤ)) = ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_2.e_a
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
⊢ (p ^ (k - s + 1)).minFac = p

Tactic:
rw [Nat.pow_minFac, hpri.1.minFac_eq]
    exact Nat.succ_ne_zero _

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

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
x : K'
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype K'
⊢ x ^ ∑ i, Fintype.card K ^ ↑i = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))

Tactic:
Fin.sum_univ_eq_sum_range,

Goal state after:
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
x : K'
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype K'
⊢ x ^ ∑ i ∈ range (Module.finrank K K'), Fintype.card K ^ i = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
x : K'
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype K'
⊢ x ^ ((Fintype.card K ^ Module.finrank K K' - 1) / (Fintype.card K - 1)) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))

Tactic:
← Module.card_eq_pow_finrank

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ a, ψ (b + a) = ∑ a, ψ a
⊢ ∑ a, ψ a = 0

Tactic:
map_add_eq_mul

Goal state after:
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ x, ψ b * ψ x = ∑ a, ψ a
⊢ ∑ a, ψ a = 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝¹ : Finite F
this✝ : Fintype F
this : Module.Finite F K
⊢ Nonempty (K →ₐ[F] L)

Tactic:
have := Module.finite_of_finite F (M := K)

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝² : Finite F
this✝¹ : Fintype F
this✝ : Module.Finite F K
this : Finite K
⊢ Nonempty (K →ₐ[F] L)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case refine_1
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ (χ ^ 2) ↑x = 1 ↑x

Tactic:
rw [one_apply_coe, χ.pow_apply_coe]

Goal state after:
case refine_1
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ χ ↑x ^ 2 = 1
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
⊢ e.mulShift (↑u - 1) = 1

Tactic:
have : u.val - 1 = ↑(u.val.val - 1 : ℤ) := by simp only [ZMod.natCast_val, Int.cast_sub,
      ZMod.intCast_cast, ZMod.cast_id', id_eq, Int.cast_one]
    rw [this, ha]
    ext1 y
    simpa only [Int.cast_mul, Int.cast_natCast, mulShift_apply, mul_assoc, one_apply]
      using DFunLike.ext_iff.mp he (a * y)

Goal state after: