mathlib-initiative/mathlib-tactics huggingface dataset:
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

Goal state after:
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 μ
v : V
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ e (-(L v) x) • f v
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‖
⊢ c ^ finrank ℝ F * φ (c • x) < ε

Tactic:
suffices δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε by
      rwa [mul_lt_mul_iff_of_pos_left (by positivity)] at this

Goal state after:
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‖
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
m : ℕ
hm : ↑m ≤ N
I : Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
⊢ ∀ᵐ (a : V) ∂μ,
    ‖iteratedFDeriv ℝ m (fun v ↦ fourierPowSMulRight L f v k) a‖ ≤
      (2 * π) ^ k * (2 * ↑k + 2) ^ m * ‖L‖ ^ k *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖a‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f a‖

Tactic:
filter_upwards with v

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
m : ℕ
hm : ↑m ≤ N
I : Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
⊢ ‖iteratedFDeriv ℝ m (fun v ↦ fourierPowSMulRight L f v k) v‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ m * ‖L‖ ^ k *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
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
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ eLpNorm (⇑f) p μ < ∞

Tactic:
by
  rcases eLpNorm_le_seminorm ℝ F p μ with ⟨k, C, hC⟩
  exact lt_of_le_of_lt (hC f) (ENNReal.mul_lt_top ENNReal.coe_lt_top ENNReal.ofReal_lt_top)

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
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
p : ℕ × ℕ
hp : p.1 ≤ k ∧ p.2 ≤ n
⊢ ↑p.2 ≤ ↑n

Tactic:
simpa using hp.2

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

Goal state before:
pp: case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
⊢ (fun a ↦ ‖iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k) a‖) ≤ᵐ[μ] fun a ↦
    (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖

Tactic:
filter_upwards with v

Goal state after:
case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
⊢ ‖iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k) v‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖v‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f v‖
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
x : ℝ
hx : x ∈ Ioi t
⊢ deriv (fun x ↦ ‖↑x ^ s‖) x = ?m.36 x

Tactic:
rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]

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

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕⁻ f y = 𝓕 (fun x ↦ f (-x)) y

Tactic:
rw [fourierInv_eq_fourier_neg]

Goal state after:
V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f (-y) = 𝓕 (fun x ↦ f (-x)) y
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: a : ℂ
⊢ ↑Complex.polarCoord a = (√(a.re * a.re + a.im * a.im), a.arg)

Tactic:
← pow_two

Goal state after:
a : ℂ
⊢ ↑Complex.polarCoord a = (√(a.re ^ 2 + a.im ^ 2), a.arg)
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
hf : Integrable f volume
⊢ ∀ᵐ (a : V), Tendsto (fun n ↦ cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) atTop (𝓝 (f a))

Tactic:
filter_upwards with v

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
hf : Integrable f volume
v : V
⊢ Tendsto (fun n ↦ cexp (-↑n⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (f v))
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
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
⊢ ∀ᵐ (a : V), ‖cexp (-↑c⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖

Tactic:
filter_upwards with v

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
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v‖ ≤ ‖f v‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ Gamma s = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
by
  rw [Gamma, Complex.Gamma_eq_integral (RCLike.ofReal_pos.mp hs), Complex.GammaIntegral_ofReal,
    Complex.ofReal_re]

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

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

Tactic:
div_one,

Goal state after:
case e'_3
⊢ √π = 2 * (√π / 2)
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
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
⊢ ∑ i, ∂_{b i} (∂_{b i} f) = -(2 * π) ^ 2 • (∑ i, fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f

Tactic:
sum_apply,

Goal state after:
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
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
⊢ ∑ i, ∂_{b i} (∂_{b i} f) = -(2 * π) ^ 2 • ∑ i, (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
x : α
⊢ x ∉ dsupport f ↔ ∃ s, IsVanishingOn f s ∧ IsOpen[inst✝²] s ∧ x ∈ s

Tactic:
by
  simp [← Set.mem_compl_iff, dsupport_compl_eq, Set.mem_sUnion, and_assoc]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
hf : MemSobolev s p f
⊢ MemSobolev s p (-f)

Tactic:
obtain ⟨f', hf⟩ := hf
  use -f'
  rw [← Lp.toTemperedDistributionCLM_apply]
  simp [map_neg, hf]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ inner ℂ (mFourierLp 2 m) (mFourierLp 2 n) = if m = n then 1 else 0

Tactic:
simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]

Goal state after:
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ ∫ (x : UnitAddTorus d), (mFourier (n + -m)) x = if m = n then 1 else 0
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)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ ∑ x, w x • ⟪c • f x, g x⟫_𝕜 = star c • ∑ i, w i • ⟪f i, g i⟫_𝕜

Tactic:
inner_smul_left_eq_star_smul,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → InnerProductSpace 𝕜 (E i)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ ∑ x, w x • (starRingEnd 𝕝) c • ⟪f x, g x⟫_𝕜 = star c • ∑ i, w i • ⟪f i, g i⟫_𝕜
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ (1 / 1) • ∫ (x : ℝ) in 0..0 + 1, (fourier (-m)) ↑x • ⋯.lift ↑x =
    ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
div_one,

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ 1 • ∫ (x : ℝ) in 0..0 + 1, (fourier (-m)) ↑x • ⋯.lift ↑x =
    ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → n.Coprime k → (m * n).Coprime k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (m * n).Coprime k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → k.Coprime n → k.Coprime (m * n)
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → k.Coprime (m * n)
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
h : k.Coprime n
⊢ ↑((k * m).gcd n) = ↑(m.gcd n)

Tactic:
simp only [gcd_coe, mul_coe]

Goal state after:
m n k : ℕ+
h : k.Coprime n
⊢ (↑k * ↑m).gcd ↑n = (↑m).gcd ↑n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → m.Coprime n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
← coprime_coe

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: k m n : ℕ+
h : m.Coprime n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n

Tactic:
← coprime_coe

Goal state after:
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ ↑(k.gcd (m * n)) = ↑(k.gcd m * k.gcd n)

Tactic:
simp only [gcd_coe, mul_coe]

Goal state after:
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ (↑k).gcd (↑m * ↑n) = (↑k).gcd ↑m * (↑k).gcd ↑n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
k l : ℕ
h : m.Coprime n
⊢ (↑m ^ k).Coprime (↑n ^ l)

Tactic:
← coprime_coe

Goal state after:
m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m ^ k).Coprime (↑n ^ l)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ μ n = 0 ∨ μ n = 1 ∨ μ n = -1

Tactic:
by
  simp only [moebius, coe_mk]
  split_ifs
  · right
    exact neg_one_pow_eq_or ..
  · left
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ ↑μ * ↑ζ = 1

Tactic:
by
  rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
by
  have : ∀ P : ℕ → Prop, ((∀ n ∈ s, P n) ↔ (∀ n > 0, n ∈ s → P n)) := fun P ↦ by
    refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
    contrapose! hs₀
    simpa [nonpos_iff_eq_zero.mp hs₀] using hn
  simpa only [this] using sum_eq_iff_sum_smul_moebius_eq_on s hs

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

Goal state before:
pp: case left
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

pp: case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Tactic:
· use i
    simp (discharger := norm_cast) [field]

Goal state after:
case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))

Tactic:
nth_rw 1 [← q.num_div_den, hn, Int.nsmul_eq_mul]
    push_cast
    ring_nf

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

Goal state before:
pp: case refine_3
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := ⋯
Q : ℤ[X] := ⋯
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ Q ∣ X ^ n - 1

Tactic:
exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R =
    (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Tactic:
← Nat.insert_self_properDivisors,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ (X ^ d - 1) * ∏ x ∈ insert n n.properDivisors \ d.divisors, cyclotomic x R =
    (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ (X ^ d - 1) * ∏ x ∈ insert n (n.properDivisors \ d.divisors), cyclotomic x R =
    (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

pp: case h.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

pp: case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0

Tactic:
Finset.prod_insert,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ (X ^ d - 1) * (cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R) =
    (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ n.properDivisors \ d.divisors

case h.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0