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

Goal state before:
pp: case e'_12.e'_16
p : ℝ × ℝ
e_4✝¹ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝¹ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝¹ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_4✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = Prod.normedAddCommGroup.toAddCommMonoid
e_6✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_13✝ : Field.toSemifield.toDivisionSemiring.toAddCommMonoid = normedAddCommGroup.toAddCommMonoid
e_14✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ sin p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 * cos p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.1 • cos p.2 • ContinuousLinearMap.snd ℝ ℝ ℝ + (sin ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: p : ℝ × ℝ
| 1 * p.1

Tactic:
← cos_sq_add_sin_sq p.2

Goal state after:
p : ℝ × ℝ
| (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
← hasFiniteIntegral_norm_iff

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * ↑a ^ 2)‖) volume
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
E : Fin 0 → Type u_3
mE : (i : Fin 0) → MeasurableSpace (E i)
μ : (i : Fin 0) → Measure (E i)
inst✝ : ∀ (i : Fin 0), SigmaFinite (μ i)
f : (i : Fin 0) → E i → 𝕜
⊢ ∫ (x : (i : Fin 0) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
| zero =>

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

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

Tactic:
← hasFiniteIntegral_norm_iff

Goal state after:
case refine_2
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun a ↦ ‖a * rexp (-b.re * a ^ 2)‖) volume
⊢ HasFiniteIntegral (fun a ↦ ‖↑a * cexp (-b * ↑a ^ 2)‖) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)
⊢ ‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

Tactic:
rw [norm_cexp_neg_mul_sq_add_mul_I, this]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
h1 : -s.re < ↑0
⊢ GammaAux 0 s = GammaAux 0 (s + 1) / s

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
⊢ GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s

Tactic:
by
    induction k with
    | zero => simp [Gamma]
    | succ k hk =>
      rw [← hk, ← add_assoc]
      refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
      rw [Nat.cast_add]
      have i0 := Nat.sub_one_lt_floor (1 - s.re)
      simp only [sub_sub_cancel_left] at i0
      refine lt_add_of_lt_of_nonneg i0 ?_
      rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
⊢ Gamma (↑0 + 1) = ↑0!

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
⊢ Gamma (-↑0) = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
⊢ ∀ (s : ℂ), GammaAux 0 ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux 0 s)

Tactic:
| zero =>

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

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

Tactic:
← hasFiniteIntegral_norm_iff

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ Gamma (↑0 + 1 + 1 / 2) = ↑(2 * 0 + 1)‼ * √π / 2 ^ (0 + 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ Gamma (↑0 + 1 / 2) = ↑(2 * 0 - 1)‼ * √π / 2 ^ 0

Tactic:
| zero =>

Goal state after:
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
⊢ ↑((c ^ (1 / 2)) ^ finrank ℝ V) * ↑(π ^ (↑(finrank ℝ V) / 2)) = (↑π * ↑c) ^ (↑(finrank ℝ V) / 2)

Tactic:
rw [mul_cpow_ofReal_nonneg pi_nonneg hc.le, ← rpow_natCast, ← rpow_mul hc.le, mul_comm,
      ofReal_cpow pi_nonneg, ofReal_cpow hc.le]

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

Goal state before:
pp: case e'_3
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ ↑((π / b) ^ (↑(Module.finrank ℝ V) / 2)) = ↑(π / b) ^ (↑(Module.finrank ℝ V) / 2)

Tactic:
ofReal_cpow (by positivity)

Goal state after:
case e'_3
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ ↑(π / b) ^ ↑(↑(Module.finrank ℝ V) / 2) = ↑(π / b) ^ (↑(Module.finrank ℝ V) / 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
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
    ∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      (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:
gcongr with p

Goal state after:
case h
𝕜 : 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
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
    (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.Distribution.Support

Goal state before:
pp: case zero
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
m : Fin 0 → E
⊢ IsVanishingOn (⇑(∂^{m} f)) s

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 : Fin 0 → E
⊢ IsVanishingOn (⇑(∂^{m} f)) s

Tactic:
| zero =>

Goal state after:
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✝¹² : NormedAddCommGroup F₁
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedAddCommGroup F₃
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : BorelSpace E
inst✝⁵ : NormedSpace ℂ F₃
inst✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace F₃
inst✝¹ : NormedSpace ℂ F₁
inst✝ : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ Integrable (fun y ↦ 𝐞 (-inner ℝ y ξ) • f₂ y) volume

Tactic:
by simpa using hf₂

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case zero
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
⊢ (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) 0) =
    0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case zero
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
⊢ (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) 0) =
    0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R ↑n) A ≤ B
⊢ B.toAddSubgroup.IsFiniteRelIndex A.toAddSubgroup

Tactic:
have := fg_toAddSubgroup hfg
  have := isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg this hn
  refine isFiniteRelIndex_of_le_left (H := A.toAddSubgroup.map (nsmulAddMonoidHom n))
    A.toAddSubgroup ?_
  rw [SetLike.le_def] at h ⊢
  simpa using h

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ (if a = 0 then ↑(Fintype.card α) else 0) = 0 ↔ a ≠ 0

Tactic:
Ne.ite_eq_right_iff

Goal state after:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ ¬a = 0 ↔ a ≠ 0

case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ ↑(Fintype.card α) ≠ 0
Module: Mathlib.Data.PNat.Prime

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

Tactic:
rw [PNat.dvd_iff]
  rw [Nat.dvd_prime pp]
  simp

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

Goal state before:
pp: case zero
⊢ (μ * ↑ζ) 0 = 1 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ 0 > 0 → ∑ i ∈ divisors 0, f i = g 0 ↔ (↑ζ • f') 0 = g' 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ (μ • g') 0 = f' 0 ↔ 0 > 0 → ∑ x ∈ divisorsAntidiagonal 0, μ x.1 • g x.2 = f 0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ ∀ (a : ℕ),
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
⊢ a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case «1»
l : ℕ
hl0 : 0 < 1
hl4 : 1 < 4
⊢ I ^ 1 ≠ 1

Tactic:
norm_num [Complex.ext_iff]

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

Goal state before:
pp: case «2»
l : ℕ
hl0 : 0 < 2
hl4 : 2 < 4
⊢ I ^ 2 ≠ 1

Tactic:
norm_num [Complex.ext_iff]

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

Goal state before:
pp: case «3»
l : ℕ
hl0 : 0 < 3
hl4 : 3 < 4
⊢ I ^ 3 ≠ 1

Tactic:
norm_num [Complex.ext_iff]

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

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

Tactic:
· rw [← Int.cast_natCast, ← Rat.divInt_eq_div, ← Rat.mk_eq_divInt (nz := by simp)]
    apply Nat.Coprime.coprime_mul_left (k := 2)
    convert! q.reduced
    grind

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ Set.InjOn (fun x ↦ ζ ^ x) ↑(range n)

Tactic:
intro i hi j hj e
  rw [Finset.coe_range, Set.mem_Iio] at hi hj
  exact hζ.pow_inj hi hj e

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

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

Tactic:
lift l to ℕ using h0

Goal state after:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ ↑l = 1 ↔ ↑k ∣ ↑l
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n

Tactic:
convert! hin.add_mul_left_left (-1) using 1

Goal state after:
case e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + ↑n * -1
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg.inl
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
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1) ≤ 1
⊢ False

Tactic:
rw [Nat.cast_one] at habs

Goal state after:
case neg.inl
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
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : 1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1) ≤ 1
⊢ False
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:
intro a

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

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
hn : Squarefree ((∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)))
⊢ False

Tactic:
Squarefree

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
hn : ∀ (x : K[X]), x * x ∣ (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) → IsUnit x
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

Tactic:
| zero =>

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

Goal state before:
pp: 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)
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ ∀ (i j : Fin p), α i = α j

Tactic:
trans aeval ζ P = 0

Goal state after:
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] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ (aeval ζ) P = 0

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] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ (aeval ζ) P = 0 ↔ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
i : Fin (minpoly K x).natDegree
⊢ (powerBasisAux hx) i = ⟨x, ⋯⟩ ^ ↑i

Tactic:
rw [adjoin.powerBasisAux, Basis.mk_apply]

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

Goal state before:
pp: case inr.zero
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
hmn : m ≤ m + 0
h : Irreducible (cyclotomic (p ^ (m + 0)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
| zero =>

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

Goal state before:
pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (-1) ^ (IsPrimitiveRoot.powerBasis K hζ).dim = 1

Tactic:
hζ.powerBasis_dim K,

Goal state after:
case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (-1) ^ (minpoly K ζ).natDegree = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 0 ≤ eval q (cyclotomic 0 ℝ)

Tactic:
simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]

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

Goal state before:
pp: case neg.refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension ∅ A B

Tactic:
refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩

Goal state after:
case neg.refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
⊢ adjoin A {b | ∃ n ∈ ∅, n ≠ 0 ∧ b ^ n = 1} = ⊤
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ∈ (cyclotomic n A).rootSet B

Tactic:
rw [mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, map_cyclotomic, ← IsRoot]

Goal state after:
case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ cyclotomic n B ≠ 0 ∧ (cyclotomic n B).IsRoot ζ