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

Goal state before:
pp: s : ℂ
⊢ ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)

Tactic:
intro n

Goal state after:
s : ℂ
n : ℕ
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal,
    coe_algebraMap]

Goal state after:
case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-b * x ^ 2)) = ↑(√(π / b) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
intro n

Goal state after:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ
⊢ -↑n < s → Gamma s ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ 2) ^ (1 / 2 - 1) = x⁻¹

Tactic:
rw [← rpow_mul (le_of_lt hx)]

Goal state after:
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (2 * (1 / 2 - 1)) = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: ⊢ Gamma (1 / 2) = √π

Tactic:
by
  rw [Gamma_eq_integral one_half_pos, ← integral_comp_rpow_Ioi_of_pos zero_lt_two]
  convert! congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1) using 1
  · rw [← integral_const_mul]
    refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
    have : (x ^ (2 : ℝ)) ^ (1 / (2 : ℝ) - 1) = x⁻¹ := by
      rw [← rpow_mul (le_of_lt hx)]
      norm_num
      rw [rpow_neg (le_of_lt hx), rpow_one]
    rw [smul_eq_mul, this]
    simp [field, (ne_of_lt (show 0 < x from hx)).symm]
    norm_num
  · rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
⊢ (𝓕 fun x ↦ cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t ↦ 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (𝓕 fun x ↦ cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t ↦ 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / - -(↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
neg_neg

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_3
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Tactic:
have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]

Goal state after:
case e'_3
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
this : b ≠ 0
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this✝ :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
this : (fourier (Pi.single i 1 i)) (z i) * {i}ᶜ.prod ?m.57 = ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)

pp: d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ d → ℂ

pp: d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : j ∈ {i}ᶜ
⊢ (fourier (Pi.single i 1 j)) (z j) = ?m.57 j

Tactic:
· rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]

Goal state after:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : j ∈ {i}ᶜ
⊢ (fourier (Pi.single i 1 j)) (z j) = 1
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
n : d → ℤ
⊢ mFourierCoeff (↑↑g) n * (starRingEnd ℂ) (mFourierCoeff (↑↑f) n) =
    inner ℂ f (mFourierBasis n) * inner ℂ (mFourierBasis n) g

Tactic:
simp only [← mFourierBasis_repr, HilbertBasis.repr_apply_apply, inner_conj_symm,
    mul_comm (inner ℂ f _)]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ (starRingEnd ℂ) (mFourierCoeff (↑↑f) i) * mFourierCoeff (↑↑g) i)
    (∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑f t) * ↑↑g t)

Tactic:
by
  simp_rw [mul_comm (conj _)]
  refine HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)
  simp only [← mFourierBasis_repr, HilbertBasis.repr_apply_apply, inner_conj_symm,
    mul_comm (inner ℂ f _)]

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

Goal state before:
pp: case h.hg₁
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
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))

Tactic:
· fun_prop

Goal state after:
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‖
⊢ ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e

Tactic:
intro n

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‖
n : ℤ
⊢ e.comp (ContinuousMap.addRight ↑n) = e
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
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight ↑n)) x

Tactic:
by
      simp only [mul_comp] at eadd ⊢
      simp_rw [eadd]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ∀ (a : ℕ), a > 0 → ∑ i ∈ a.divisors, f i = g a ↔ (↑ζ • f') a = g' a

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n > 0 → ∑ i ∈ n.divisors, f i = g n ↔ (↑ζ • f') n = g' n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ∀ (a : ℕ), (μ • g') a = f' a ↔ a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (μ • g') n = f' n ↔ n > 0 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
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}
⊢ {v | ‖v‖ ≤ R + 1} = {y | dist y 0 ≤ R + 1}

Tactic:
dist_eq_norm,

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}
⊢ {v | ‖v‖ ≤ R + 1} = {y | ‖y - 0‖ ≤ R + 1}
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
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
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

pp: case refine_2
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, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
· rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

Goal state after:
case refine_2
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, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
⊢ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
intro n

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
⊢ n > 0 → n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
⊢ ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n

Tactic:
intro n

Goal state after:
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
⊢ n > 0 → n ∈ s → ∑ i ∈ n.divisors, f i = g n
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.toFun x‖ = ‖f.toFun (- -x)‖

Tactic:
neg_neg

Goal state after:
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.toFun x‖ = ‖f.toFun x‖
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
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
⊢ n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n ∈ s → (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

pp: case refine_2
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
⊢ (n ∈ s →
      ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
        if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
· rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

Goal state after:
case refine_2
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
⊢ (n ∈ s →
      ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
        if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ (j - i) = 1

Tactic:
← ((h.isUnit (Nat.ne_zero_of_lt hi)).pow i).mul_left_inj,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ (j - i) * ζ ^ i = 1 * ζ ^ i
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
⊢ ζ = 1

Tactic:
← pow_one ζ,

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
⊢ ζ ^ 1 = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ l = 1

Tactic:
← pow_one ζ,

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ (ζ ^ 1) ^ l = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R

Tactic:
← map_cyclotomic_int,

Goal state after:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (cyclotomic 1 ℤ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

Tactic:
rw [← map_cyclotomic_int]

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).Monic
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n R).degree = ↑n.totient

Tactic:
rw [← map_cyclotomic_int]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).degree = ↑n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)

Tactic:
intro n

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
n : ℕ
⊢ 0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∃ α, α ^ n = a
⊢ (nthRoots n a).Nodup

Tactic:
obtain ⟨α, hα⟩ := h
    by_cases hα' : α = 0
    · exact (ha (by rwa [hα', zero_pow hn.ne', eq_comm] at hα)).elim
    rw [nthRoots_eq h hα, Multiset.nodup_map_iff_inj_on (Multiset.nodup_range n)]
    exact h.injOn_pow_mul hα'

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0

Tactic:
intro n

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
⊢ 0 < n → ¬X ^ n - 1 = 0
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a : ℕ
⊢ ∀ (p : ℕ),
    a ≠ 0 →
      Prime p →
        (IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
          IsPrimitiveRoot μ n✝ → (p * a).Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))

Tactic:
p

Goal state after:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
⊢ a ≠ 0 →
    Prime p →
      (IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
        IsPrimitiveRoot μ n✝ → (p * a).Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
⊢ hμ.toRootsOfUnity ^ (↑h.choose).val = hμ.toRootsOfUnity ^ h.choose

Tactic:
rw [pow_eq_pow_iff_modEq, ZMod.val_natCast]

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
⊢ h.choose % n ≡ h.choose [MOD orderOf hμ.toRootsOfUnity]
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Function.Injective fun n ↦ cyclotomic n R

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n : ℕ
⊢ ∀ ⦃a₂ : ℕ⦄, (fun n ↦ cyclotomic n R) n = (fun n ↦ cyclotomic n R) a₂ → n = a₂
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℚ = minpoly ℚ μ

Tactic:
← map_cyclotomic_int,

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ map (Int.castRingHom ℚ) (cyclotomic n ℤ) = minpoly ℚ μ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℚ)

Tactic:
rw [← map_cyclotomic_int]

Goal state after:
n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case neg
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
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R ((B.basis.repr ((algebraMap R S) (Q.coeff ↑⟨j, hj⟩) • B.basis ⟨j, hj⟩)) i)

Tactic:
map_smul

Goal state after:
case neg
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
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R (((algebraMap R S) (Q.coeff ↑⟨j, hj⟩) • B.basis.repr (B.basis ⟨j, hj⟩)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (-1) (cyclotomic n R)

Tactic:
← map_cyclotomic_int,

Goal state after:
n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (-1) (map (Int.castRingHom R) (cyclotomic n ℤ))