mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
⊢ ∀ x ∈ Ioi 0, ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x

Tactic:
intro x hx

Goal state after:
case left
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : x ∈ Ioi 0
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p

Tactic:
rw [mem_Ioi] at hx

Goal state after:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ EqOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (↑s - 1)) (fun x ↦ ↑(rexp (-x) * x ^ (s - 1))) (Ioi 0)

Tactic:
intro x hx

Goal state after:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x ↦ ↑(rexp (-x)) * ↑x ^ (↑s - 1)) x = (fun x ↦ ↑(rexp (-x) * x ^ (s - 1))) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ x ∈ Ioc 0 Y, ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x

Tactic:
intro x hx

Goal state after:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (fun x ↦ ↑x ^ (s - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x

Tactic:
intro x hx

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
⊢ HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker

Tactic:
intro x hx

Goal state after:
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.snd ℝ ℝ ℝ).ker
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
this : Tendsto (fun X ↦ -↑X ^ s * ↑(rexp (-X))) atTop (𝓝 0)
⊢ Tendsto (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) atTop (𝓝 (s * s.GammaIntegral))

Tactic:
simpa using! Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this

Goal state after:
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
⊢ EqOn (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) (fun e ↦ e ^ s.re * rexp (-1 * e)) (Ioi 0)

Tactic:
intro x hx

Goal state after:
s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) x = (fun e ↦ e ^ s.re * rexp (-1 * e)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
⊢ Gamma (-0) = 0

Tactic:
neg_zero,

Goal state after:
case zero
⊢ Gamma 0 = 0
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)
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = (1 / ↑r) ^ (a - 1) * (↑r * ↑x) ^ (a - 1) * cexp (-(↑r * ↑x))

Tactic:
rw [mem_Ioi] at hx

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = (1 / ↑r) ^ (a - 1) * (↑r * ↑x) ^ (a - 1) * cexp (-(↑r * ↑x))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : c ∈ {c | 0 < c.re}
⊢ (↑π / c) ^ (1 / 2) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or]
    exact Or.inl (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))

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

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

Tactic:
intro x hx

Goal state after:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ x ∈ Function.support fun x ↦ rexp (-x) * x ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

Tactic:
rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]
    · exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb
    · rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]

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

Goal state before:
pp: case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ Gamma (↑(k + 1) + 1 + 1 / 2) = ↑(2 * (k + 1) + 1)‼ * √π / 2 ^ (k + 1 + 1)

Tactic:
rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
    simp
    ring

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)
⊢ π ^ 0 = 1

Tactic:
exact rpow_zero _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
⊢ 𝓕 ((fderivCLM 𝕜 V E) f) = (2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (𝓕 f)

Tactic:
ext x m
  change 𝓕 (fderiv ℝ ⇑f) x m = _
  simp [fourier_fderiv f.integrable f.differentiable (fderivCLM ℝ V E f).integrable,
    innerSL_apply_apply ℝ, fourier_coe]

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

Goal state before:
pp: case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ dsupport ⇑(TemperedDistribution.delta x)

Tactic:
mem_dsupport_iff_forall_exists_ne

Goal state after:
case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ ∀ (s : Set E),
    x ∈ s →
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
        ∃ u, tsupport ⇑u ⊆ s ∧ (TemperedDistribution.delta x) u ≠ 0
Module: Mathlib.Analysis.Distribution.Support

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

Tactic:
mem_dsupport_iff_forall_exists_ne

Goal state after:
case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
⊢ ∀ (s : Set E),
    x ∈ s → IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0
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
x : V →ᵇ ℂ
hx : x ∈ (charAlgHom he hL).range
⊢ star x ∈ (charAlgHom he hL).range

Tactic:
simp only [AlgHom.mem_range] at hx ⊢
  obtain ⟨y, rfl⟩ := hx
  let z := y.map (starRingEnd _).toAddMonoidHom
  let f : W ↪ W := ⟨fun x ↦ -x, (fun _ _ ↦ neg_inj.mp)⟩
  refine ⟨.ofCoeff <| z.coeff.embDomain f, ?_⟩
  ext
  simp [charAlgHom_apply, Finsupp.sum_embDomain, z, Finsupp.sum_mapRange_index, f]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g : E → ℂ
hg : Function.HasTemperateGrowth g
c : ℂ
⊢ smulLeftCLM F (c • g) = c • smulLeftCLM F g

Tactic:
by
  ext f u
  simp [SchwartzMap.smulLeftCLM_smul hg]

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

Goal state before:
pp: case right
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞

Tactic:
suffices h : ∫⁻ a : E, ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ⊤ from by
        norm_cast
        simp_rw [ofReal_norm] at h
        simp_rw [← enorm_pow]
        convert h
        rw [← Real.rpow_mul_natCast (by positivity)]
        simp

Goal state after:
case right
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ ∫⁻ (a : E), ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ∞
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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ 1 + ‖x‖ ^ 2 = ((1 + ‖x‖ ^ 2) ^ (1 / 2)) ^ 2

Tactic:
rw [← Real.rpow_mul (by positivity)]; simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisors, f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ =
    ‖(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }))
        ⟨-x, ?refine_2⟩‖

Tactic:
rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisors, f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1

Tactic:
intro x hx

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : ⇑f =O[atBot ⊔ atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot ⊔ atTop] fun x ↦ |x| ^ (-b)

Tactic:
isBigO_sup

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ ((fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot] fun x ↦ |x| ^ (-b)) ∧
    (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atTop] fun x ↦ |x| ^ (-b)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
← inv_iff,

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i)⁻¹ k
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
⊢ ∀ c ∈ k.properDivisors, cyclotomic' c K ∈ lifts (Int.castRingHom K)

Tactic:
intro x hx

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
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
⊢ eval μ ((map (algebraMap ℤ K) (minpoly ℤ (μ ^ p))).comp (map (algebraMap ℤ K) (X ^ p))) = 0

Tactic:
Polynomial.map_pow,

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
⊢ eval μ ((map (algebraMap ℤ K) (minpoly ℤ (μ ^ p))).comp (map (algebraMap ℤ K) X ^ p)) = 0
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
⊢ (image (fun x ↦ ζ ^ x * α) (range n)).val ⊆ nthRoots n a

Tactic:
intro x hx

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
x : R
hx : x ∈ (image (fun x ↦ ζ ^ x * α) (range n)).val
⊢ x ∈ nthRoots n a
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg
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] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ map (Int.castRingHom (ZMod p)) (X ^ n) - 1
⊢ False

Tactic:
Polynomial.map_pow,

Goal state after:
case neg
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] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ map (Int.castRingHom (ZMod p)) X ^ n - 1
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 2 R = X + 1

Tactic:
simp [cyclotomic_prime]

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

Goal state before:
pp: case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
intro x hx

Goal state after:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
⊢ x ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this✝ :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
this : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

Tactic:
simp [cyclotomic_prime]

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

Goal state before:
pp: 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 y : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R ((B.basis.repr y) I.2 * ((B.basis.repr x) I.1 * (B.basis.repr (B.basis I.1 * B.basis I.2)) i))

Tactic:
refine (hy _).mul ((hx _).mul ?_)

Goal state after:
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 y : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R ((B.basis.repr (B.basis I.1 * B.basis I.2)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
⊢ (expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R

Tactic:
by
  rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
  · simp
  have := NeZero.of_pos hnpos
  suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ by
    rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]
  refine eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ ℤ))
    ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_
  · refine (IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast _ _
      ((cyclotomic.isPrimitive (n * p) ℤ).mul (cyclotomic.isPrimitive n ℤ))).2 ?_
    rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int]
    refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_
    · replace h : n * p = n * 1 := by simp [h]
      exact Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)
    · have hpos : 0 < n * p := mul_pos hnpos hp.pos
      have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
      rw [cyclotomic_eq_minpoly_rat hprim hpos]
      refine minpoly.dvd ℚ _ ?_
      rw [← eval_map_algebraMap, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
        @isRoot_cyclotomic_iff]
      convert! IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
      rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
    · have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
      rw [cyclotomic_eq_minpoly_rat hprim hnpos]
      refine minpoly.dvd ℚ _ ?_
      rw [← eval_map_algebraMap, map_expand, expand_eval, ← IsRoot.def, ←
        cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, @isRoot_cyclotomic_iff]
      exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv
  · rw [natDegree_expand, natDegree_cyclotomic,
      natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ), natDegree_cyclotomic,
      natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv), Nat.totient_prime hp,
      mul_comm (p - 1), ← Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]

Goal state after: