mathlib-initiative/mathlib-tactics huggingface dataset:
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]
    simp [mul_pow]
    ring

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ (fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁) f = (fourierMultiplierCLM F (g₁ * g₂)) f

Tactic:
simp [fourierMultiplierCLM_fourierMultiplierCLM_apply hg₁ hg₂]

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

Goal state before:
pp: V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f : 𝓢(V, H)
⊢ ∫ (ξ : V), ‖(𝓕 f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

Tactic:
apply Complex.ofRealLI.injective

Goal state after:
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f : 𝓢(V, H)
⊢ Complex.ofRealLI (∫ (ξ : V), ‖(𝓕 f) ξ‖ ^ 2) = Complex.ofRealLI (∫ (x : V), ‖f x‖ ^ 2)
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_12
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
f : 𝓓'(Ω, F)
s : Set E
hf : IsVanishingOn (⇑f) s
m : E
⊢ IsVanishingOn (⇑(∂_{m} f)) s

Tactic:
intro u hu
  simp only [Distribution.lineDerivOp_apply_apply, map_neg, neg_eq_zero]
  exact hf (∂_{m} u) <| (tsupport_fderiv_apply_subset ℝ m).trans hu

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
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖x‖ ^ 2) ^ (s' / 2) = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2)

Tactic:
rw [← Real.rpow_add (by positivity)]

Goal state after:
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'
⊢ (fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) f = Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
TemperedDistribution.fourierMultiplierCLM_apply

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

Goal state before:
pp: 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
⊢ (𝓕⁻ (𝓕 (((convolution B) f) g))) x = 𝓕⁻ (fun y ↦ 𝓕 (⇑f ⋆[B, volume] ⇑g) y) x

Tactic:
by
    rw [fourierInv_coe]
    apply MeasureTheory.integral_congr_ae
    filter_upwards with x
    rw [fourier_convolution_apply]

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

Goal state before:
pp: case e'_3
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
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖x‖ ^ 2) ^ (-s / 2) = 1

Tactic:
rw [← Real.rpow_add (by positivity)]

Goal state after:
case e'_3
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
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (s / 2 + -s / 2) = 1
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x y : ℤ
h : zmod n ↑x = zmod n ↑y
⊢ ↑x = ↑y

Tactic:
have hn : (n : ℝ) ≠ 0 := NeZero.ne _

Goal state after:
n : ℕ
inst✝ : NeZero n
x y : ℤ
h : zmod n ↑x = zmod n ↑y
hn : ↑n ≠ 0
⊢ ↑x = ↑y
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: l : ℕ
hl : Squarefree l
⊢ ((-1) ^ cardFactors l) ^ 2 = 1

Tactic:
← pow_mul,

Goal state after:
l : ℕ
hl : Squarefree l
⊢ (-1) ^ (cardFactors l * 2) = 1
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2) • ((∫ (a : V), 𝐞 (-⟪a, w⟫) • f a) + - -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v)

pp: case hf
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f v) volume

pp: case hg
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume

Tactic:
neg_neg,

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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2) • ((∫ (a : V), 𝐞 (-⟪a, w⟫) • f a) + ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v)

case hf
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f v) volume

case hg
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume
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
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∀ᶠ (x : V) in cocompact V, ‖∫ (v : V), 𝐞 (-⟪v, x⟫) • f v‖ < ε

Tactic:
simp_rw [← comap_dist_left_atTop_eq_cocompact (0 : V), eventually_comap, eventually_atTop,
      dist_eq_norm', sub_zero]
    exact
      let ⟨T, hT⟩ := this
      ⟨T, fun b hb v hv => hT v (hv.symm ▸ hb)⟩

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

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

Tactic:
← intCoe_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
⊢ ↑(μ * ↑ζ) = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

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

Tactic:
← intCoe_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
⊢ ↑(↑ζ * μ) = 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case right
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[atTop] fun x ↦ |x| ^ (-b)

Tactic:
· refine (isBigO_of_le atTop ?_).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)
    simp_rw [norm_norm]; exact this

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 1 R = X - 1

Tactic:
by
  simp only [cyclotomic', Finset.prod_singleton, map_one, IsPrimitiveRoot.primitiveRoots_one]

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i

Tactic:
← exp_nat_mul

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i

Tactic:
← exp_nat_mul

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Tactic:
by
  by_cases hzero : n = 0
  · simp only [hzero, cyclotomic, dif_pos, Polynomial.map_one]
  simp [cyclotomic, hzero]

Goal state after:
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
m : ℕ
left✝ : m < n
⊢ (ζ ^ m) ^ n * a = a

Tactic:
← pow_mul,

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
m : ℕ
left✝ : m < n
⊢ ζ ^ (m * n) * a = a
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 R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
hr : 0 < n
⊢ b.Coprime n

Tactic:
by
      simpa [(b.gcd_dvd_left n).trans] using h.dvd_iff (Nat.gcd_dvd_right b n)

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : (cyclotomic m ℂ).IsRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
hmzero : NeZero m
⊢ n = m

Tactic:
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) m
hmzero : NeZero m
⊢ n = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ (X ^ p ^ k) ^ p - 1 = X ^ p ^ (k + 1) - 1

Tactic:
← pow_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ X ^ (p ^ k * p) - 1 = X ^ p ^ (k + 1) - 1
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ LinearIndependent K fun i ↦ ⟨x, ⋯⟩ ^ ↑i

Tactic:
have : LinearIndependent K _ := linearIndependent_pow
      (⟨x, self_mem_adjoin_singleton _ _⟩ : K[x])
    rwa [← minpoly.algebraMap_eq hST] at this

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

Goal state before:
pp: case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ (expand R p) (cyclotomic n R) = cyclotomic (n * p) R

Tactic:
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by
    rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]

Goal state after:
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))

Tactic:
by
    have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ']⟩
    rw [pow_succ', mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv,
      cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ← pow_mul]
    · simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
      rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]
    · assumption

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
by
  have hnegζ : IsPrimitiveRoot (-ζ) (2 * n) := by
    convert! IsPrimitiveRoot.orderOf (-ζ)
    rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
    · simp [hζ.eq_orderOf]
    · simp [← hζ.eq_orderOf, hno]
  obtain ⟨k, hkpos, hkn⟩ := isOfFinOrder_iff_pow_eq_one.1 hx
  obtain ⟨l, hl, hlroot⟩ := (isRoot_of_unity_iff hkpos _).1 hkn
  have hlzero : NeZero l := ⟨fun h ↦ by simp [h] at hl⟩
  have : NeZero (l : K) := ⟨NeZero.natCast_ne l K⟩
  rw [isRoot_cyclotomic_iff] at hlroot
  obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1
  replace hlroot : x ^ (2 * n) = 1 := by rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
  obtain ⟨s, -, hs⟩ := hnegζ.eq_pow_of_pow_eq_one hlroot
  exact ⟨s, hs.symm⟩

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) ζ
⊢ q - 1 < ‖↑q - ζ‖

Tactic:
by
      convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]

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

Goal state before:
pp: case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ (2 ^ 2) ^ 2 ^ k₁ = ↑2 ^ (2 * 2 ^ k₁)

Tactic:
← pow_mul,

Goal state after:
case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ 2 ^ (2 * 2 ^ k₁) = ↑2 ^ (2 * 2 ^ k₁)
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
this : IsCyclic ↥(rootsOfUnity n M)
⊢ Finite ↥(rootsOfUnity n M)

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := rootsOfUnity n M)

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
this : IsCyclic ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), x ∈ Subgroup.zpowers g
⊢ Finite ↥(rootsOfUnity n M)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝ : NeZero ↑n
k : K
this : IsLocalization (nonZeroDivisors A) K
⊢ ∃ x,
    (algebraMap K (CyclotomicField n K)) k * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1

Tactic:
replace := this.surj

Goal state after:
case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝ : NeZero ↑n
k : K
this : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
⊢ ∃ x,
    (algebraMap K (CyclotomicField n K)) k * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
k : K
⊢ ∃ x,
    (algebraMap K (CyclotomicField n K)) k * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1

Tactic:
have : IsLocalization (nonZeroDivisors A) K := inferInstance
      replace := this.surj
      obtain ⟨⟨z, w⟩, hw⟩ := this k
      refine ⟨⟨algebraMap A (CyclotomicRing n A K) z, algebraMap A (CyclotomicRing n A K) w,
        map_mem_nonZeroDivisors _ (algebraBase_injective n A K) w.2⟩, ?_⟩
      let : IsScalarTower A K (CyclotomicField n K) :=
        IsScalarTower.of_algebraMap_eq (congr_fun rfl)
      rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
        @IsScalarTower.algebraMap_apply A K _ _ _ _ _ (_root_.CyclotomicField.algebra n K) _ _ w,
        ← map_mul, hw, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : ¬IsUnit x
⊢ (if hx : IsUnit (x * y) then ↑(f hx.unit) else 0) =
    (if hx : IsUnit x then ↑(f hx.unit) else 0) * if hx : IsUnit y then ↑(f hx.unit) else 0

Tactic:
· simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst✝ : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hm).ker
⊢ x ∈ (ZMod.unitsMap ⋯).ker

Tactic:
MonoidHom.mem_ker

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst✝ : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : (ZMod.unitsMap hm) x = 1
⊢ (ZMod.unitsMap ⋯) x = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Odd n
⊢ χ ^ n = χ

Tactic:
obtain ⟨n, rfl⟩ := hn

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n + 1) = χ
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∈ χ.conductorSet
this✝¹ : NeZero d
this✝ : d.gcd χ.conductor ∈ χ.conductorSet
this : ¬χ.conductor ∣ d
⊢ d.gcd χ.conductor ≤ χ.conductor

Tactic:
exact Nat.gcd_le_right _ <| Nat.pos_of_ne_zero <| conductor_ne_zero χ

Goal state after: