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

Goal state before:
pp: 𝕜 : Type u_2
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ k C,
    ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
rcases hμ.exists_eLpNorm_lt_top p with ⟨k, hk⟩
  refine ⟨k, (eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ).toNNReal * 2 ^ k, fun f ↦ ?_⟩
  have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
  calc eLpNorm (⇑f) p μ
  _ = eLpNorm ((fun x : E ↦ (1 + ‖x‖) ^ (-k : ℝ)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ := by
    refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
    simp [(h_one_add x).ne']
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ⊤ μ := by
    refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
    refine Continuous.aestronglyMeasurable ?_
    exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) := by
    gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using!
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x
  _ = _ := by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    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
⊢ MemLp ⇑f ∞ μ

Tactic:
refine memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
⊢ IntegrableOn (fun x ↦ (x + m) ^ a) (Ioi c) volume

Tactic:
by
  have hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x := by
    intro x hx
    convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
    · simp [show a + 1 ≠ 0 by linarith]
    left; linarith [mem_Ici.mp hx, id_eq x]
  have ht : Tendsto (fun t ↦ ((t + m) ^ (a + 1)) / (a + 1)) atTop (nhds (0 / (a + 1))) := by
    rw [← neg_neg (a + 1)]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp
      (tendsto_atTop_add_const_right _ m tendsto_id) |>.div_const _
  exact integrableOn_Ioi_deriv_of_nonneg' hd
    (fun t ht ↦ rpow_nonneg (by linarith [mem_Ioi.mp ht]) a) ht

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

Goal state before:
pp: case hg
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
f g : ↥(Lp E 1 volume)
x : V
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, x⟫) • ↑↑g v) volume

Tactic:
· rw [Real.fourierIntegral_convergent_iff]
          exact L1.integrable_coeFn g

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x ↦ x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) volume
⊢ AEStronglyMeasurable f volume

Tactic:
simpa using (hf 0 zero_le).1

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

Goal state before:
pp: r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
          ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
      (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg) =
    (r, θ)

Tactic:
ext <;> dsimp at hr hθ ⊢

Goal state after:
case fst
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ √((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r

case snd
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (Complex.equivRealProd.symm (r * cos θ, r * sin θ)).arg = θ
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : Type u_3
f : E → 𝕜
mE : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
⊢ (∫ (x : ι → E), ∏ i, f (x i) ∂Measure.pi fun x ↦ μ) = (∫ (x : E), f x ∂μ) ^ card ι

Tactic:
rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]

Goal state after:
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:
rw [← 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.Gaussian.GaussianIntegral

Goal state before:
pp: b✝ : ℂ
hb✝ : 0 < b✝.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : b ∈ {c | 0 < c.re}
⊢ 0 < (↑π).re * b.re / normSq b + 0 * b.im / normSq b

Tactic:
ofReal_re,

Goal state after:
b✝ : ℂ
hb✝ : 0 < b✝.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : b ∈ {c | 0 < c.re}
⊢ 0 < π * b.re / normSq b + 0 * b.im / normSq b
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ 1 / ↑r * (1 / ↑r) ^ (a - 1) * ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-↑t) = (1 / ↑r) ^ a * Gamma a

Tactic:
rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]

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

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

Tactic:
induction n generalizing s with
  | zero =>
    intro hs
    refine (Gamma_pos_of_pos ?_).ne'
    rwa [Nat.cast_zero, neg_zero] at hs
  | succ _ n_ih =>
    intro hs'
    have : Gamma (s + 1) ≠ 0 := by
      apply n_ih
      · intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring
      · rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith
    rw [Gamma_add_one, mul_ne_zero_iff] at this
    · exact this.2
    · simpa using hs 0

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

Goal state before:
pp: case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
⊢ Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)

Tactic:
have B := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (finrank ℝ V / 2) 1
        zero_lt_one |>.comp A |>.const_mul (π ^ (-finrank ℝ V / 2 : ℝ))

Goal state after:
case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 (π ^ (-↑(finrank ℝ V) / 2) * 0))
⊢ Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
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
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
exact hf.fourierInv_fourier_eq h'f hv

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

Goal state before:
pp: case h
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✝ f : 𝓢(E, F)
⊢ ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F)).symm) f‖ ≤ ‖↑(toLpCLM ℂ F 2 volume) f‖

Tactic:
convert! (norm_fourier_toL2_eq (𝓕⁻ f)).symm.le

Goal state after:
case e'_4.e'_3
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✝ f : 𝓢(E, F)
⊢ ↑(toLpCLM ℂ F 2 volume) f = (𝓕 (𝓕⁻ f)).toLp 2 volume
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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)
f' : ↥(Lp F 2 volume)
hf' : 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)) = 𝓕⁻ (Lp.toTemperedDistribution f')
⊢ 𝓕⁻ (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
Lp.fourierInv_toTemperedDistribution_eq f'

Goal state after:
case h
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)
f' : ↥(Lp F 2 volume)
hf' : 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)) = 𝓕⁻ (Lp.toTemperedDistribution f')
⊢ Lp.toTemperedDistribution (𝓕⁻ f') = Lp.toTemperedDistribution (𝓕⁻ f')
Module: Mathlib.Analysis.Fourier.Convolution

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

Tactic:
have : Integrable (fun ξ ↦ B (𝓕 f ξ) (𝓕 g ξ)) volume := (pairing B (𝓕 f) (𝓕 g)).integrable

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

Goal state before:
pp: case intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

pp: case intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
· have : Unique (Fin Nat.zero →₀ ℤ) :=
      { uniq := by subsingleton }
    exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩

Goal state after:
case intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e 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
⊢ ∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm

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
⊢ Summable fun i ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ }) (e * f.comp (ContinuousMap.addRight ↑i))‖
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
pp : p.Prime
⊢ ¬p ∣ 1

Tactic:
rw [dvd_iff]

Goal state after:
p : ℕ+
pp : p.Prime
⊢ ¬↑p ∣ ↑1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ⟨p, ⋯⟩ ∣ n

Tactic:
rw [dvd_iff]

Goal state after:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
rw [dvd_iff]

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (X ^ n - 1).IsRoot ζ

Tactic:
simp [hζ.pow_eq_one]

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

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n n' : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ n ∣ n' → (X ^ n' - 1).IsRoot ζ

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
R : Type u_4
inst✝ : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
k : ℕ
⊢ (X ^ (n * k) - 1).IsRoot ζ
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ 2 = orderOf (-1)

Tactic:
rw [orderOf_neg_one, if_neg <| by rwa [ringChar.eq_iff.mpr h]]

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

Goal state before:
pp: case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ minpoly ℤ μ ∣ X ^ n - 1

Tactic:
apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)

Goal state after:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ (Polynomial.aeval μ) (X ^ n - 1) = 0
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ (Polynomial.aeval μ) ((expand ℤ p) (minpoly ℤ (μ ^ p))) = 0

Tactic:
rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X,
    eval_comp, eval_X_pow, ← eval₂_eq_eval_map, ← aeval_def]

Goal state after:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ (Polynomial.aeval (μ ^ p)) (minpoly ℤ (μ ^ p)) = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (cyclotomic n R).natDegree ≤ n.totient

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
a✝ : Nontrivial R
⊢ (cyclotomic n R).natDegree ≤ n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∏ i ∈ {1, p}.erase 1, cyclotomic i ℤ

Tactic:
erase_insert (mem_singleton.not.2 hp.out.ne_one.symm),

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∏ i ∈ {p}, cyclotomic i ℤ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
⊢ cyclotomic n R = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
⊢ cyclotomic n R = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
⊢ orderOf μ' = n

Tactic:
refine Eq.trans ?_ hμ.eq_orderOf.symm

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
⊢ orderOf μ' = orderOf μ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
⊢ P = cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
⊢ P = cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
(div_modByMonic_unique P 0 prod_monic _).1

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P = P

R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
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✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝² : MeasurableSpace V' := borel V'
this✝¹ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this✝ : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : StrongDual ℝ V
this : ∫ (v : V), 𝐞 (-w v) • f v ∂μ = ∫ (x : V), 𝐞 (-w (A.symm (Aₘ x))) • f (A.symm (Aₘ x)) ∂μ
⊢ ∫ (v : V), 𝐞 (-w v) • f v ∂μ =
    ((fun w ↦ ∫ (v : V'), 𝐞 (-w v) • (f ∘ ⇑A.symm) v ∂Measure.map (⇑Aₘ) μ) ∘ Adual.toHomeomorph.toCocompactMap.toFun) w

Tactic:
simpa [Function.comp_apply, integral_map_equiv, Adual]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ (cyclotomic n R).roots = (primitiveRoots n R).val

Tactic:
rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : 0 = (cyclotomic m R).natDegree
⊢ 0 = m

Tactic:
natDegree_cyclotomic,

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : 0 = m.totient
⊢ 0 = m