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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
⊢ ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s

Tactic:
have int_eval := integral_eq_sub_of_hasDerivAt_of_le hX cont.continuousOn F_der_I der_ible

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  ∫ (y : ℝ) in 0..X, -(↑(rexp (-y)) * ↑y ^ s) + ↑(rexp (-y)) * (s * ↑y ^ (s - 1)) =
    ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0
⊢ ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p)

Tactic:
by
      apply setIntegral_congr_fun polarCoord.open_target.measurableSet fun x hx => ?_
      rw [abs_of_pos hx.1]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun y ↦ -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))

Tactic:
refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)

Goal state after:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x ↦ ‖cexp (-b * ↑x ^ 2)‖) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero.hb
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0

Tactic:
contrapose! h1

Goal state after:
case zero.hb
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
let n := ⌊1 - s.re⌋₊
  have t1 : -s.re < n := by simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)
  have t2 : -(s + 1).re < n := by rw [add_re, one_re]; linarith
  rw [Gamma_eq_GammaAux s n t1, Gamma_eq_GammaAux (s + 1) n t2, GammaAux_recurrence1 s n t1]
  field

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)
⊢ (↑k + ↑1 + 1 / 2) * Gamma (↑k + ↑1 + 1 / 2) = ↑(2 * (k + 1) + 1)‼ * √π / 2 ^ (k + 1 + 1)

Tactic:
Nat.cast_one,

Goal state after:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ (↑k + 1 + 1 / 2) * Gamma (↑k + 1 + 1 / 2) = ↑(2 * (k + 1) + 1)‼ * √π / 2 ^ (k + 1 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -(↑n✝ + ↑1) < s
⊢ -↑n✝ < s + 1

Tactic:
Nat.cast_one,

Goal state after:
case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -(↑n✝ + 1) < s
⊢ -↑n✝ < s + 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0

Tactic:
simpa using hs 0

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

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

Tactic:
rw [integral_add_right_eq_self fun a : ℝ ↦ cexp (- -b * (↑a + ↑(c / (2 * b)).im * I) ^ 2),
    integral_cexp_neg_mul_sq_add_real_mul_I ((neg_re b).symm ▸ (neg_pos.mpr hb))]

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

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Integrable (fun v ↦ cexp (-∑ i, b i * ↑(v i) ^ 2 + ∑ i, c i * ↑(v i))) volume

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Integrable (fun v ↦ ∏ x, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x))) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (-∑ i, b i * ↑(v i) ^ 2 + ∑ i, c i * ↑(v i)) =
    ∏ i, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), ∏ x, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x)) = ∏ i, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case refine_4
𝕜 : 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
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ (2 * π) ^ (k, n).2 * (2 * ↑(k, n).2 + 2) ^ (k, n).1 *
      ∑ p ∈ Finset.range ((k, n).2 + 1) ×ˢ Finset.range ((k, n).1 + 1),
        ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
    ((2 * π) ^ n * (2 * ↑n + 2) ^ k * ↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
            2 ^ volume.integrablePower *
          ∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) *
        2 *
      ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f

Tactic:
simp only [mul_assoc]

Goal state after:
case refine_4
𝕜 : 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
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ (2 * π) ^ n *
      ((2 * ↑n + 2) ^ k *
        ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖) ≤
    (2 * π) ^ n *
      ((2 * ↑n + 2) ^ k *
        (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
          (2 ^ volume.integrablePower *
            ((∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) *
              (2 *
                ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup
                    (schwartzSeminormFamily 𝕜 V E))
                  f)))))
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ (fun a ↦ (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a) * ↑↑f a) =ᵐ[volume] fun a ↦ (mFourier (-i)) a • ↑↑f a

Tactic:
filter_upwards [coeFn_mFourierLp 2 i] with _ ht

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a✝) * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝
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')
⊢ 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)) = Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
rw [hf', Lp.fourierInv_toTemperedDistribution_eq f']

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p m : ℕ+
pp : p.Prime
⊢ m ∣ p ↔ m = 1 ∨ m = p

Tactic:
PNat.dvd_iff

Goal state after:
p m : ℕ+
pp : p.Prime
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
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) • ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v - 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)

Tactic:
integral_sub,

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) - ∫ (a : V), 𝐞 (-⟪a, w⟫) • f (a + (1 / (2 * ‖w‖ ^ 2)) • w))

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.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ μ (p ^ k) = if k = 1 then -1 else 0

Tactic:
by
  split_ifs with h
  · rw [h, pow_one, moebius_apply_prime hp]
  rw [moebius_eq_zero_of_not_squarefree]
  rw [squarefree_pow_iff hp.ne_one hk, not_and_or]
  exact Or.inr h

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l

Tactic:
intro l

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
⊢ ζ ^ (a * l) = 1 → b ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l

Tactic:
intro l

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
⊢ f ζ ^ l = 1 → orderOf ζ ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot (f ζ) k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), ζ ^ l = 1 → orderOf (f ζ) ∣ l

Tactic:
intro l

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot (f ζ) k
hf : Injective ⇑f
l : ℕ
⊢ ζ ^ l = 1 → orderOf (f ζ) ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ∀ (l : ℕ), ζ⁻¹ ^ l = 1 → k ∣ l

Tactic:
intro l

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ⁻¹ ^ l = 1 → k ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case left
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✝ h : IsPrimitiveRoot ζ k
i : ZMod k
hi :
  ↑((((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i) =
    ↑0
this : ↑k ∣ i.cast
⊢ ↑i.cast = i

Tactic:
exact ZMod.intCast_rightInverse i

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

Goal state before:
pp: case e'_3
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
hfi : ¬Integrable f volume
w : V
⊢ ¬Integrable (fun a ↦ 𝐞 (-⟪a, w⟫) • f a) volume

Tactic:
rwa [Real.fourierIntegral_convergent_iff]

Goal state after:
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✝ : a ≠ 0
hprime : Prime p
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))

Tactic:
replace hprime := hprime.nat_prime

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✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
⊢ minpoly ℤ (μ ^ a) = 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:
← rootsOfUnity.coe_pow,

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μ.toRootsOfUnity ^ (↑h.choose).val) = ↑↑hμ.toRootsOfUnity ^ h.choose
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ (cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
← isRoot_map_iff hf,

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ (map (algebraMap R (FractionRing R)) (cyclotomic n R)).IsRoot ((algebraMap R (FractionRing R)) μ) ↔
    IsPrimitiveRoot μ n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

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

Tactic:
Nat.totient_eq_zero,

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : m = 0
⊢ 0 = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ 0 < eval x (cyclotomic n R)

Tactic:
by
  induction n using Nat.strong_induction_on with | _ n ih
  have hn' : 0 < n := pos_of_gt hn
  have hn'' : 1 < n := one_lt_two.trans hn
  have := prod_cyclotomic_eq_geom_sum hn' R
  apply_fun eval x at this
  rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons,
    eval_mul, eval_geom_sum] at this
  rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)
  · apply pos_of_mul_pos_left
    · rwa [this]
    rw [eval_prod]
    refine Finset.prod_nonneg fun i hi => ?_
    simp only [Finset.mem_erase, mem_properDivisors] at hi
    rw [geom_sum_pos_iff hn'.ne'] at h
    rcases h with hk | hx
    · refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le <;> rintro rfl
      · exact hn'.ne' (zero_dvd_iff.mp hi.2.1)
      · exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk
    · rcases eq_or_ne i 2 with (rfl | hk)
      · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le
      refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le
      rintro rfl
      exact hn'.ne' <| zero_dvd_iff.mp hi.2.1
  · rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h
    exact h.1.symm ▸ cyclotomic_neg_one_pos hn
  · apply pos_of_mul_neg_left
    · rwa [this]
    rw [geom_sum_neg_iff hn'.ne'] at h
    have h2 : 2 ∈ n.properDivisors.erase 1 := by
      rw [Finset.mem_erase, mem_properDivisors]
      exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
    rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]
    apply mul_nonpos_of_nonneg_of_nonpos
    · refine Finset.prod_nonneg fun i hi => le_of_lt ?_
      simp only [Finset.mem_erase, mem_properDivisors] at hi
      refine ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)
      rintro rfl
      rw [zero_dvd_iff] at hi
      exact hn'.ne' hi.2.2.1
    · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le

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

Goal state before:
pp: case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ p ^ k - p ^ (k - 1) ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt <| pow_right_strictMono₀ hp.out.one_lt <| Nat.pred_lt hk.ne'

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

Goal state before:
pp: case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (0 - 1) ^ φ n < (eval (↑0) (cyclotomic n ℤ)).natAbs

Tactic:
zero_tsub,

Goal state after:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ 0 ^ φ n < (eval (↑0) (cyclotomic n ℤ)).natAbs
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (↑q - ↑1) ^ φ n < ↑(eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
Nat.cast_one,

Goal state after:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (↑q - 1) ^ φ n < ↑(eval (↑q) (cyclotomic n ℤ)).natAbs
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_3
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ + b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

pp: case refine_4
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ * b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
· exact Subalgebra.add_mem _ hb₁ hb₂

Goal state after:
case refine_4
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ * b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
algInst✝ : Algebra K L := f.toAlgebra
this : Finite K
⊢ Nat.card Gal(K/F) = Module.finrank F K

Tactic:
IsGalois.card_aut_eq_finrank

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
algInst✝ : Algebra K L := f.toAlgebra
this : Finite K
⊢ Module.finrank F K = Module.finrank F K
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
A : Type u
K : Type w
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ n
⊢ CyclotomicRing n A K = ↥A[μ]

Tactic:
rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
    IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]
  simp [CyclotomicRing, NeZero.ne n]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a

Tactic:
refine ⟨hu.unit, ?_, hu.unit_spec⟩

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ hu.unit ∈ rootsOfUnity (orderOf χ) R
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
h₁ : IsCyclotomicExtension {0} A ↥C₁
h : 0 ∣ n₂
⊢ False

Tactic:
exact NeZero.ne n₂ <| eq_zero_of_zero_dvd h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
h : ((changeLevel hm) χ).conductor ∣ χ.conductor
⊢ χ = (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter

Tactic:
apply changeLevel_injective hm

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
h : ((changeLevel hm) χ).conductor ∣ χ.conductor
⊢ (changeLevel hm) χ = (changeLevel hm) ((changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : ¬IsCoprime a ↑χ.conductor
⊢ ¬IsCoprime a ↑((changeLevel hm) χ).conductor

Tactic:
rwa [conductor_changeLevel]

Goal state after: