mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
x : α
⊢ (∀ (s : Set α), x ∈ s → IsOpen[inst✝²] s → ¬IsVanishingOn f s) ↔
    ∀ (s : Set α), x ∈ s → IsOpen[inst✝²] s → ∃ u, tsupport ⇑u ⊆ s ∧ f u ≠ 0

Tactic:
not_isVanishingOn_iff

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
a : d → ℝ
⊢ MeasurePreserving (⇑(measurableEquivPiIoc a)) volume (Measure.comap Subtype.val volume)

Tactic:
refine (⟨(measurableEquivPiIoc a).symm.measurable, symm ?_⟩ :
    MeasurePreserving (measurableEquivPiIoc a).symm _ _).symm
  have := Measure.map_map (μ := volume.comap Subtype.val) (measurable_pi_lambda
    (fun (x : d → ℝ) => (fun i => x i : UnitAddTorus d))
    (fun i => AddCircle.measurable_mk'.comp (measurable_pi_apply i)))
    measurable_subtype_coe (α := {x : d → ℝ // ∀ i, x i ∈ Ioc (a i) (a i + 1)})
  simp only [Function.comp_def] at this
  simp_rw [coe_symm_measurableEquivPiIoc, ← this]
  convert! (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm
  · simp [volume, AddCircle.haarAddCircle]
  · convert!
    (map_comap_subtype_coe (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc (a := a i))) volume)
    convert! (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm
    grind

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (x : UnitAddTorus d), f x = ∫⁻ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}, f fun i ↦ ↑(x i)

Tactic:
by
  convert! lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm
  · exact (measurePreserving_equivPiIoc a).symm.map_eq.symm
  · rw [← lintegral_subtype_comap (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc))]
    rfl

Goal state after:
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
p q r : ℝ≥0∞
inst✝² : p.HolderTriple q r
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
⊢ (fun a ↦ u a • ↑↑(MemLp.toLp g hg₂ • f) a) =ᵐ[μ] fun a ↦ ((SchwartzMap.smulLeftCLM ℂ g) u) a • ↑↑f a

Tactic:
filter_upwards [Lp.coeFn_lpSMul (r := r) (hg₂.toLp _) f, hg₂.coeFn_toLp] with x hg hg'

Goal state after:
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
p q r : ℝ≥0∞
inst✝² : p.HolderTriple q r
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
x : E
hg : ↑↑(MemLp.toLp g hg₂ • f) x = (↑↑(MemLp.toLp g hg₂) • ↑↑f) x
hg' : ↑↑(MemLp.toLp g hg₂) x = g x
⊢ u x • ↑↑(MemLp.toLp g hg₂ • f) x = ((SchwartzMap.smulLeftCLM ℂ g) u) x • ↑↑f x
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case refine_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ ℤ ∙ p i ^ e i
i : ι
⊢ Nat.Prime ((fun i ↦ (p i).natAbs) i)

Tactic:
← Int.prime_iff_natAbs_prime,

Goal state after:
case refine_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ ℤ ∙ p i ^ e i
i : ι
⊢ Prime (p i)
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case refine_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ ℤ ∙ p i ^ e i
i : ι
⊢ Irreducible (p i)

Tactic:
exact hp i

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

Goal state before:
pp: G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
by
  cases nonempty_fintype G
  obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G
  rcases n with - | n
  · have : Unique (Fin Nat.zero →₀ ℤ) :=
      { uniq := by subsingleton }
    exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩
  · have := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
    exact
      (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
            ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim

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

Goal state before:
pp: case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0

Tactic:
· simp [h]

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

Goal state before:
pp: n : ℕ
⊢ μ n ≠ 0 ↔ Squarefree n

Tactic:
by
  constructor <;> intro h
  · contrapose h
    simp [h]
  · simp [h]

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
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → ∀ (a : V), dist 0 a = b → ‖∫ (v : V), 𝐞 (-⟪v, a⟫) • f v‖ < ε

Tactic:
dist_eq_norm',

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
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → ∀ (a : V), ‖a - 0‖ = b → ‖∫ (v : V), 𝐞 (-⟪v, a⟫) • f v‖ < ε
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
⊢ p ∈ n.primeFactors → 1 + f p = ↑(ζ p) + f p

Tactic:
hp

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = ↑(ζ p) + f 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∀ᶠ (x : V) in cocompact V, ‖∫ (v : V), 𝐞 (-⟪v, x⟫) • f v‖ < ε

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
⊢ p ∈ n.primeFactors → 1 - f p = 1 + ((↑μ).pmul f) p

Tactic:
hp

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ((↑μ).pmul f) p
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case prime_pow
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

Tactic:
rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']

Goal state after:
case prime_pow
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ ∑ k ∈ range n, μ (p ^ (k + 1)) + μ (p ^ 0) = 1 (p ^ n)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
let f' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else f x, if_pos rfl⟩

Goal state after:
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' := ⋯ }
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: 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
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

Tactic:
by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))

Goal state after:
case pos
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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

case neg
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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ orderOf ζ ≠ 0

Tactic:
simpa [← hζ.eq_orderOf]

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
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R + ‖-i w‖ ≤ ‖v‖

Tactic:
norm_neg

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
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
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R + ‖i w‖ ≤ ‖v‖
Module: Mathlib.RingTheory.RootsOfUnity.Complex

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

pp: case neg
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
· simp [h]

Goal state after:
case neg
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i

Tactic:
← mul_left_inj' (cyclotomic_ne_zero 1 ℤ),

Goal state after:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) * cyclotomic 1 ℤ = (∑ i ∈ range n, X ^ i) * cyclotomic 1 ℤ
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : Nat.card ↥(rootsOfUnity n R) = n
ζ : Rˣ
hζ' : ζ ∈ rootsOfUnity n R
hζ : IsPrimitiveRoot (↑↑⟨ζ, hζ'⟩) n
⊢ ∃ ζ, IsPrimitiveRoot ζ n

Tactic:
use ζ

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μ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 ∈ {i, n}, cyclotomic x K = X ^ n - 1
⊢ False

Tactic:
Finset.prod_pair key.ne,

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) * (cyclotomic i K * cyclotomic n K) = X ^ n - 1
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: 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
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * cyclotomic (p ^ (n_n + 1)) R) =
    X ^ p ^ (n_n + 1 + 1) - 1

Tactic:
n_ih

Goal state after:
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
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case e'_3
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y) = eval (x / y) (∏ ζ ∈ nthRootsFinset n 1, (X - C ζ)) * y ^ #(nthRootsFinset n 1)

Tactic:
· simp [eval_prod, prod_mul_pow_card, sub_mul, hy]

Goal state after:
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)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
this✝ : IsPrimitiveRoot z ↑k
this : IsCyclotomicExtension {↑k} K ↥K[z]
⊢ φ (p.lcm q) = Module.finrank K ↥(Subalgebra.toSubmodule K[z])

Tactic:
rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr

Goal state after:
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
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
hirr : Irreducible (cyclotomic (↑k) K)
this✝ : IsPrimitiveRoot z ↑k
this : IsCyclotomicExtension {↑k} K ↥K[z]
⊢ φ (p.lcm q) = Module.finrank K ↥(Subalgebra.toSubmodule K[z])
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 : ℕ
⊢ Nat.Prime p → ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs

Tactic:
hp

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
⊢ ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
h : l = 0
⊢ False

Tactic:
by simp [h] at hl

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

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : CommRing L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsDomain L
⊢ (Algebra.norm K) ζ = (-1) ^ Module.finrank K L

Tactic:
by
  rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic n ℤ)) = ↑n.minFac

Tactic:
← IsPrimePow.minFac_pow_factorization_eq hn

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic (n.minFac ^ n.factorization n.minFac) ℤ)) = ↑n.minFac
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ eval 0 (cyclotomic n ℤ) ≠ 0

Tactic:
← coeff_zero_eq_eval_zero,

Goal state after:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (cyclotomic n ℤ).coeff 0 ≠ 0
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i =
    x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i

Tactic:
Finset.prod_pow_eq_pow_sum

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i =
    x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case h
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
⊢ p ∣ x + ps.prod id * n → ¬p ∣ m

Tactic:
hp

Goal state after:
case h
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
⊢ ¬p ∣ m
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : (ψ.mulShift a) 1 = 1 1
⊢ False

Tactic:
rw [mulShift_apply, mul_one] at h

Goal state after:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : ψ a = 1 1
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: case inl
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : Nat.Prime (ringChar F')
⊢ ¬ringChar F' ∣ p

pp: case inr
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
⊢ ¬ringChar F' ∣ p

Tactic:
· exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm

Goal state after:
case inr
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
⊢ ¬ringChar F' ∣ p
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ χ ↑a = 0 ↔ ¬¬χ ↑a = 0

Tactic:
not_not

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ χ ↑a = 0 ↔ χ ↑a = 0
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ χ ↑x ^ p = χ ↑x

Tactic:
rcases hχ x with (hx | hx | hx)

Goal state after:
case inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 0
⊢ χ ↑x ^ p = χ ↑x

case inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ χ ↑x ^ p = χ ↑x

case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ χ ↑x ^ p = χ ↑x