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

Goal state before:
pp: case convert_1
c : ℝ
hc : 1 < c
t : ℝ
⊢ t ∈ Ici c → HasDerivAt (fun t ↦ -(log t)⁻¹) (t⁻¹ / log t ^ 2) t

Tactic:
_

Goal state after:
case convert_1
c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ HasDerivAt (fun t ↦ -(log t)⁻¹) (t⁻¹ / log t ^ 2) t
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0} → (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg) ∈ Ioi 0 ×ˢ Ioo (-π) π

Tactic:
rintro ⟨x, y⟩ hxy

Goal state after:
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ (√((x, y).1 ^ 2 + (x, y).2 ^ 2), (Complex.equivRealProd.symm (x, y)).arg) ∈ Ioi 0 ×ˢ Ioo (-π) π
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane

Tactic:
rintro ⟨x, y⟩ hxy

Goal state after:
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ Complex.equivRealProd.symm (x, y) ∈ Complex.slitPlane
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ Integrable (fun x ↦ cexp (-b * ↑x ^ 2)) volume

Tactic:
refine ⟨by fun_prop, ?_⟩

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun x ↦ cexp (-b * ↑x ^ 2)) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ), cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2)) =
    ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2))

Tactic:
by
      rw [← integral_comp_polarCoord_symm]
      simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x ↦ cexp (-b * (↑x + ↑c * I) ^ 2)) volume

Tactic:
refine ⟨by fun_prop, ?_⟩

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun x ↦ cexp (-b * (↑x + ↑c * I) ^ 2)) volume
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 : s * Gamma s ≠ 0
⊢ Gamma s ≠ 0

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:
mul_ne_zero_iff

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

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
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
| ∫ (x : ℝ), cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
1,

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
| ∫ (x : ℝ), cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2)
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)
x m : V
⊢ ((𝓕 ((fderivCLM 𝕜 V E) f)) x) m = (((2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (𝓕 f)) x) m

Tactic:
change 𝓕 (fderiv ℝ ⇑f) x m = _

Goal state after:
𝕜 : 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)
x m : V
⊢ (𝓕 (fderiv ℝ ⇑f) x) m = (((2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (𝓕 f)) x) m
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s

Tactic:
intro u hu
  apply hf ((SchwartzMap.smulLeftCLM ℂ g) u)
  rw [SchwartzMap.smulLeftCLM_apply hg]
  exact (tsupport_smul_subset_right g u).trans hu

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ = 1

Tactic:
by
  apply le_antisymm
  · refine (ContinuousMap.norm_le _ zero_le_one).mpr fun i ↦ ?_
    simp only [mFourier, fourier_apply, ContinuousMap.coe_mk, norm_prod, Circle.norm_coe,
      Finset.prod_const_one, le_rfl]
  · refine (le_of_eq ?_).trans ((mFourier n).norm_coe_le_norm fun _ ↦ 0)
    simp only [mFourier, ContinuousMap.coe_mk, fourier_eval_zero, Finset.prod_const_one,
      CStarRing.norm_one]

Goal state after:
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
⊢ { toFun := fun x ↦ ∏ i_1, (fourier (Pi.single i 1 i_1)) (x i_1), continuous_toFun := ⋯ } z = (fourier 1) (z i)

Tactic:
ContinuousMap.coe_mk

Goal state after:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
⊢ ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)
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
m : E
f : 𝓢'(E, F)
⊢ (besselPotential E F (-1)) (∂_{m} f) =
    (2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f

Tactic:
rw [lineDeriv_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
  congr
  ext x
  simp

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ Orthonormal ℂ (mFourierLp 2)

Tactic:
orthonormal_iff_ite

Goal state after:
d : Type u_1
inst✝ : Fintype d
⊢ ∀ (i j : d → ℤ), inner ℂ (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0
⊢ LinearIndependent 𝕜 f

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0
h✝ : IsEmpty ι
⊢ LinearIndependent 𝕜 f

case inr
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0
h✝ : Nonempty ι
⊢ LinearIndependent 𝕜 f
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: 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 : ℕ
hn : n > 0
hnP : n ∈ s
n✝ : ℕ
⊢ n✝ > 0 → ∑ i ∈ n✝.divisors, f i = G n✝

Tactic:
_

Goal state after:
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 : ℕ
hn : n > 0
hnP : n ∈ s
n✝ : ℕ
a✝ : n✝ > 0
⊢ ∑ i ∈ n✝.divisors, f i = G n✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: 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 : ℕ
hn : n > 0
hnP : n ∈ s
n✝ : ℕ
⊢ n✝ > 0 → ∑ x ∈ n✝.divisorsAntidiagonal, μ x.1 • g x.2 = F n✝

Tactic:
_

Goal state after:
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 : ℕ
hn : n > 0
hnP : n ∈ s
n✝ : ℕ
a✝ : n✝ > 0
⊢ ∑ x ∈ n✝.divisorsAntidiagonal, μ x.1 • g x.2 = F n✝
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
⊢ IsPrimitiveRoot (↑ζ ^ i) k

Tactic:
← Units.val_pow_eq_pow_val

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
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
this : Summable fun c ↦ f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (c : ℤ), f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))) x

Tactic:
simp_rw [← tsum_apply h, ← tsum_apply this]

Goal state after:
case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
this : Summable fun c ↦ f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))
⊢ ∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p))) (x + p) =
    ∑' (i : ℤ), (f.comp (ContinuousMap.addRight ((Equiv.addRight 1) i • p))) x
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)

Tactic:
← orderOf_pow_of_dvd hp hdiv

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
⊢ z ∈ primitiveRoots n R → X - C z ≠ 0

Tactic:
_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
a✝ : z ∈ primitiveRoots n R
⊢ X - C z ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
n : ℕ
z : K
⊢ z ∈ primitiveRoots n K → (X - C z).Splits

Tactic:
_

Goal state after:
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
a✝ : z ∈ primitiveRoots n K
⊢ (X - C z).Splits
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (∏ i ∈ n.divisors, cyclotomic' i K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
← Nat.cons_self_properDivisors hpos.ne',

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic' i K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
· have : 0 ≤ -l := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
    lift -l to ℕ using this with l' hl'
    rw [← dvd_neg, ← hl']
    norm_cast
    rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]

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

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
⊢ i ∈ n.properDivisors → (cyclotomic' i K).Monic

Tactic:
_

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
a✝ : i ∈ n.properDivisors
⊢ (cyclotomic' i K).Monic
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
i : ℕ
⊢ i ∈ k.properDivisors → (cyclotomic' i K).Monic

Tactic:
_

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
i : ℕ
a✝ : i ∈ k.properDivisors
⊢ (cyclotomic' i K).Monic
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

Tactic:
← Nat.cons_self_properDivisors hpos.ne',

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
⊢ IsPrimitiveRoot μ n✝ → u.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ u)

Tactic:
_

Goal state after:
case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
⊢ u.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ u)
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
⊢ u.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ u)

Tactic:
_

Goal state after:
case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : u.Coprime n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ u)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
i : ℕ
⊢ i ∈ n.properDivisors → (cyclotomic i R).Monic

Tactic:
_

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝¹ : Nontrivial R
i : ℕ
a✝ : i ∈ n.properDivisors
⊢ (cyclotomic i R).Monic
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:
_

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
⊢ Prime p →
    (IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
      IsPrimitiveRoot μ n✝ → (p * a).Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K

Tactic:
obtain hzero | hpos := k.eq_zero_or_pos

Goal state after:
case h.inl
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ cyclotomic k K = cyclotomic' k K

case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic k K = cyclotomic' k K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R = ∏ i ∈ n.divisors, cyclotomic i R

Tactic:
← Nat.cons_self_properDivisors hpos.ne',

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

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

Tactic:
_

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

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval ((Nat.castRingHom (ZMod p)) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) = 0

Tactic:
← Nat.cons_self_properDivisors hpos.ne',

Goal state after:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval ((Nat.castRingHom (ZMod p)) a) (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic i (ZMod p)) = 0
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
⊢ IsIntegral R ((B.basis.repr ((aeval B.gen) Q)) i)

Tactic:
aeval_eq_sum_range' hlt

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
⊢ IsIntegral R ((B.basis.repr (∑ i ∈ Finset.range B.dim, Q.coeff i • B.gen ^ i)) i)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
by
  rcases Nat.eq_zero_or_pos p with (rfl | hppos)
  · simp
  rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
  · simp
  let z := x ^ (p / factorizationLCMLeft p q) * y ^ (q / factorizationLCMRight p q)
  let k := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
  have : IsPrimitiveRoot z k := hx.pow_mul_pow_lcm hy hppos.ne' hqpos.ne'
  have := IsPrimitiveRoot.adjoin_isCyclotomicExtension K this
  convert! Submodule.finrank_le (Subalgebra.toSubmodule (adjoin K { z }))
  rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr
  simpa using! (IsCyclotomicExtension.finrank (Algebra.adjoin K {z}) hirr).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
⊢ False

Tactic:
apply_fun eval 1 at this

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = eval 1 (∑ i ∈ range n, X ^ i)
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case insert
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
⊢ Module.Finite A B

Tactic:
| @insert n S _ _ H =>

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_4
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x✝ : GaloisField (n✝ + 1) n
hx :
  x✝ ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
x y : GaloisField (n✝ + 1) n
⊢ x ∈
      Subring.closure
        (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
          (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
    y ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      x ^ (n✝ + 1) ^ n = x → y ^ (n✝ + 1) ^ n = y → x ^ (n✝ + 1) ^ n + y ^ (n✝ + 1) ^ n = x + y

Tactic:
_

Goal state after:
case succ.refine_4
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x✝ : GaloisField (n✝ + 1) n
hx :
  x✝ ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
x y : GaloisField (n✝ + 1) n
hx✝ :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ y ∈
      Subring.closure
        (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
          (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
    x ^ (n✝ + 1) ^ n = x → y ^ (n✝ + 1) ^ n = y → x ^ (n✝ + 1) ^ n + y ^ (n✝ + 1) ^ n = x + y