mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑π ^ ↑(↑(finrank ℝ V) / 2) * ↑c ^ ↑(1 / 2 * ↑(finrank ℝ V)) = ↑π ^ (↑(finrank ℝ V) / 2) * ↑c ^ (↑(finrank ℝ V) / 2)

Tactic:
simp [div_eq_inv_mul]

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

Goal state before:
pp: case e_f.e_a
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
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ 2 * ↑π * Complex.I * (2 * ↑π * Complex.I) = ↑(algebraMap ℝ ℂ).toMonoidWithZeroHom (-(2 * π) ^ 2)

Tactic:
ring_nf

Goal state after:
case e_f.e_a
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
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ ↑π ^ 2 * Complex.I ^ 2 * 4 = { toFun := (↑↑(algebraMap ℝ ℂ)).toFun, map_zero' := ⋯ } (-(π ^ 2 * 4))
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f.e_a
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
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ 2 * ↑π * Complex.I * (2 * ↑π * Complex.I) = ↑(-(2 * π) ^ 2)

Tactic:
ring_nf

Goal state after:
case e_f.e_a
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
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ ↑π ^ 2 * Complex.I ^ 2 * 4 = ↑(-(π ^ 2 * 4))
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℂ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ ((toTemperedDistributionCLM E F μ) f) g = ∫ (x : E), g x • f x ∂μ

Tactic:
by
  simp [toTemperedDistributionCLM, comp_apply _]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
x y : W
⊢ char he hL (x + y) = char he hL x * char he hL y

Tactic:
ext
  simp [e.map_add_eq_mul]

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

Goal state before:
pp: case h
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : v ≠ v'
w : W
a : ℝ
ha : e a ≠ 1
hw : (L v) w - (L v') w ≠ 0
⊢ ¬e (-(a / ((L v) w - (L v') w) * (L v') w) + a / ((L v) w - (L v') w) * (L v) w) = 1

Tactic:
ring_nf

Goal state after:
case h
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : v ≠ v'
w : W
a : ℝ
ha : e a ≠ 1
hw : (L v) w - (L v') w ≠ 0
⊢ ¬e (a * (L v) w * ((L v) w - (L v') w)⁻¹ - a * (L v') w * ((L v) w - (L v') w)⁻¹) = 1
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ (↑(toTemperedDistributionCLM F μ p)).ker = ⊥

Tactic:
by
  rw [LinearMap.ker_eq_bot', ContinuousLinearMap.coe_coe]
  intro f hf
  rw [eq_zero_iff_ae_eq_zero]
  apply ae_eq_zero_of_integral_contDiff_smul_eq_zero
  · exact (Lp.memLp f).locallyIntegrable hp.elim
  · intro g g_smooth g_cpt
    have hg₁ : HasCompactSupport (Complex.ofRealCLM ∘ g) := g_cpt.comp_left rfl
    have hg₂ : ContDiff ℝ ∞ (Complex.ofRealCLM ∘ g) := by fun_prop
    calc
      _ = toTemperedDistributionCLM F μ p f (hg₁.toSchwartzMap hg₂) := by simp
      _ = _ := by simp [hf]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ¬↑(AddCircle.toCircle (x i)) = ↑(AddCircle.toCircle (y i))

Tactic:
Subtype.coe_inj

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹⁷ : RCLike 𝕜
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : InnerProductSpace ℝ E
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
inst✝¹¹ : NormedAddCommGroup F₁
inst✝¹⁰ : NormedSpace ℂ F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : SMulCommClass ℂ 𝕜 F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace ℂ F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : SMulCommClass ℂ 𝕜 F₂
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace ℂ F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
⊢ ∀ (x y : 𝓢(E, F₁)),
    fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 (x + y)) ∘SL fourierCLM 𝕜 𝓢(E, F₂) =
      fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 x) ∘SL fourierCLM 𝕜 𝓢(E, F₂) +
        fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 y) ∘SL fourierCLM 𝕜 𝓢(E, F₂)

Tactic:
simp [FourierTransform.fourier_add]

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

Goal state before:
pp: case right
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ eLpNorm (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume < ∞

Tactic:
· rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by norm_num) (by norm_num)]
      suffices h : ∫⁻ a : E, ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ⊤ from by
        norm_cast
        simp_rw [ofReal_norm] at h
        simp_rw [← enorm_pow]
        convert h
        rw [← Real.rpow_mul_natCast (by positivity)]
        simp
      apply ((integrable_rpow_neg_one_add_norm_sq hs).congr _).lintegral_lt_top
      filter_upwards with x
      rw [Real.norm_eq_abs, abs_eq_self.mpr (by positivity)]
      congr
      ring

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 + -s / 2) = 1

Tactic:
ring_nf

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) ^ 0 = 1
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ doubleDualEmb a = doubleDualEmb 0 ↔ a = 0

Tactic:
doubleDualEmb_inj

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ a = 0 ↔ a = 0
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case a
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
hiw : ⟪i w, w⟫ = 1 / 2
v : V
H : cexp (-(↑π * I)) = (-1)⁻¹
⊢ cexp (2 * ↑π * -↑⟪v, w⟫ * I) * 1 + cexp (-2 * ↑π * ↑⟪v, w⟫ * I) * (-1)⁻¹ -
      (-(cexp (2 * ↑π * -↑⟪v, w⟫ * I) * cexp (2 * ↑π * -(1 / 2) * I) * 1) +
        cexp (-2 * ↑π * ↑⟪v, w⟫ * I) * cexp (-(↑π * I))) =
    0

Tactic:
ring_nf

Goal state after:
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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
⊢ 1 / 2 / ‖w‖ / ‖w‖ * ‖w‖ = 1 / 2 / ‖w‖

Tactic:
div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)

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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
⊢ 1 / 2 / ‖w‖ = 1 / 2 / ‖w‖
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * (2 * ↑n / ↑q.den)) = cexp (2 * ↑π * I * (↑n / ↑q.den))

Tactic:
ring_nf

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

Goal state before:
pp: case e'_3
q : ℚ
h : Odd q.num
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * (↑q / 2))

Tactic:
ring_nf

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

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

Tactic:
zpow_natCast

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

Goal state before:
pp: k : ℕ
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
by
  by_cases h : k = 0
  · simp [h]
  exact (isPrimitiveRoot_exp k h).card_primitiveRoots

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

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

Tactic:
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
Q : ℤ[X]
hQ : (fun P ↦ map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ map (Int.castRingHom K) Q = map (Int.castRingHom K) P

Tactic:
hP.1,

Goal state after:
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
Q : ℤ[X]
hQ : (fun P ↦ map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ map (Int.castRingHom K) Q = cyclotomic' (↑n) K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

Tactic:
nontriviality R
  rw [natDegree_cyclotomic]

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

Goal state before:
pp: case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod : (mapRingHom (Int.castRingHom (ZMod p))) (P * Q) ∣ (mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)
⊢ False

Tactic:
rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one,
    Polynomial.map_pow, map_X] at prod

Goal state after:
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ X ^ n - 1
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ n.divisors.erase 1

Tactic:
simp [hd, hdn, hn.ne']

Goal state after:
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)
⊢ ↑((fun x ↦ ⟨↑x ^ a, ⋯⟩) ((fun x ↦ ⟨↑x ^ b, ⋯⟩) x)) = ↑x

Tactic:
simp [← pow_mul, mul_comm b,
    pow_eq_pow_of_modEq h (isPrimitiveRoot_of_mem_primitiveRoots x.2).pow_eq_one]

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

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∈ (orderOf μ).divisors
hiμ : (cyclotomic i K).IsRoot μ
⊢ False

Tactic:
replace hio := Nat.dvd_of_mem_divisors hio

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Nat.card G ∣ Nat.card G

Tactic:
Nat.card_eq_fintype_card

Goal state after:
G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Fintype.card G ∣ Fintype.card G
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R).coeff 0 = -(cyclotomic n R).coeff 0

Tactic:
mul_coeff_zero,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 * (∏ x ∈ n.properDivisors, cyclotomic x R).coeff 0 = -(cyclotomic n R).coeff 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : ¬i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

Tactic:
· rw [hc, degree_mul, degree_cyclotomic, Nat.totient_prime hp] at hP'
    have : c.degree ≤ 0 := (WithBot.add_le_add_iff_left (x := ↑(p - 1)) (by simp)).mp (by simpa)
    obtain ⟨c, rfl⟩ := natDegree_eq_zero.mp (natDegree_eq_zero_iff_degree_le_zero.mpr this)
    simp [hP, hc, cyclotomic_prime]

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : ¬i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

Tactic:
by
  rcases n with (_ | _ | _ | n)
  · simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self]
  · simp
  · simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]
    constructor <;> intro <;> linarith
  · constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by lia)

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
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
⊢ l ∣ 2 * n

Tactic:
have key := IsPrimitiveRoot.lcm_totient_le_finrank hζ hroot
    (cyclotomic.irreducible_rat <| Nat.lcm_pos (Nat.pos_of_ne_zero hl.1) (NeZero.pos n))

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
key : φ (l.lcm n) ≤ Module.finrank ℚ K
⊢ l ∣ 2 * n
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : g_poly.natDegree = p ^ n
this : g_poly.rootSet (GaloisField p n) = Set.univ
key : Fintype.card ↑Set.univ = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
← Fintype.ofEquiv_card (Equiv.Set.univ _)

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : g_poly.natDegree = p ^ n
this : g_poly.rootSet (GaloisField p n) = Set.univ
key : Fintype.card (GaloisField p n) = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n