mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ (((convolution B) f) g) x = (𝓕⁻ (𝓕 (((convolution B) f) g))) x

Tactic:
by simp

Goal state after:
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:
rw [← Int.prime_iff_natAbs_prime, ← irreducible_iff_prime]; exact hp i

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝ : NeZero n
⊢ zmod n 0 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝ : NeZero n
⊢ ∀ (a b : ZMod n), zmod n (a + b) = zmod n a * zmod n b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ ∑ ψ, ψ a = if a = 0 then ↑(Fintype.card α) else 0

Tactic:
simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

Goal state after:
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ 1 ≤ 1 + ‖x‖ ^ 2

Tactic:
by simp

Goal state after:
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ ((1 + ‖x‖ ^ 2) ^ (1 / 2)) ^ 2 = ((1 + ‖x‖ ^ 2) ^ (1 / 2)) ^ 2

Tactic:
by simp

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

Goal state before:
pp: n : ℕ+
⊢ gcd 1 n = 1

Tactic:
apply one_gcd

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

Goal state before:
pp: f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
⊢ ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x

Tactic:
let F : C(UnitAddCircle, ℂ) :=
    ⟨(f.periodic_tsum_comp_add_zsmul 1).lift, continuous_coinduced_dom.mpr (map_continuous _)⟩
  have : Summable (fourierCoeff F) := by
    convert! h_sum
    exact Real.fourierCoeff_tsum_comp_add h_norm _
  convert! (has_pointwise_sum_fourier_series_of_summable this x).tsum_eq.symm using 1
  · simpa only [F, coe_mk, ← QuotientAddGroup.mk_zero, Periodic.lift_coe, zsmul_one, comp_apply,
      coe_addRight, zero_add]
       using (hasSum_apply (summable_of_locally_summable_norm h_norm).hasSum x).tsum_eq
  · simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]

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

Goal state before:
pp: R : Type u_1
⊢ (if Squarefree 0 then (-1) ^ cardFactors 0 else 0) = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ μ 1 = 1

Tactic:
by simp

Goal state after:
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
hs₀ : 0 ∉ s
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
have : ∀ P : ℕ → Prop, ((∀ n ∈ s, P n) ↔ (∀ n > 0, n ∈ s → P n)) := fun P ↦ by
    refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
    contrapose! hs₀
    simpa [nonpos_iff_eq_zero.mp hs₀] using hn

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
this : ∀ (P : ℕ → Prop), (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : k ≠ 0
⊢ ζ * ζ ^ (k - 1) = 1

Tactic:
← pow_succ',

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : k ≠ 0
⊢ ζ ^ (k - 1 + 1) = 1
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ q.den ≠ 0

Tactic:
by simp

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

Goal state before:
pp: q : ℚ
h : Odd q.num
⊢ q.den * 2 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ n = (X ^ n - C 1).natDegree

Tactic:
natDegree_X_pow_sub_C

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ n = n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
⊢ NeZero ↑n

Tactic:
let p := ringChar R

Goal state after:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
⊢ NeZero ↑n
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
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / ↑B
⊢ ∀ v ∈ A, ‖f v - f (v + (1 / (2 * ‖w‖ ^ 2)) • w)‖ ≤ ε / ↑B

Tactic:
refine fun x _ => (hδ2 ?_).le

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
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / ↑B
x : V
x✝ : x ∈ A
⊢ ‖x - (x + (1 / (2 * ‖w‖ ^ 2)) • w)‖ < δ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: 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
h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K
⊢ (X ^ k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' k K

Tactic:
cyclotomic'_eq_X_pow_sub_one_div hpos hz,

Goal state after:
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
h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K
⊢ (X ^ k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic i K = (X ^ k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic' i K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: 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
h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K
⊢ cyclotomic k K = cyclotomic' k K

Tactic:
rw [@cyclotomic_eq_X_pow_sub_one_div _ _ _ hpos, cyclotomic'_eq_X_pow_sub_one_div hpos hz,
    Finset.prod_congr (refl k.properDivisors) h]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
| n

Tactic:
hμ.eq_orderOf

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
| orderOf μ
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
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : ↑(p - 1) + c.degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
⊢ ↑(p - 1) ≠ ⊥

Tactic:
by simp

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

Tactic:
by
  have : Fact p.Prime := ⟨hp⟩
  let P : ℚ[X] := ∑ i, C (α i) * X ^ i.1
  have hP (i : Fin p) : α i = P.coeff i := by simp [P, ← Fin.ext_iff]
  have hP' : P.degree ≤ ↑(p - 1) :=
    (degree_sum_le ..).trans (Finset.sup_le fun _ _ ↦ by grw [degree_C_mul_X_pow_le]; simp; grind)
  trans aeval ζ P = 0; · simp [P]
  rw [← minpoly.dvd_iff, ← cyclotomic_eq_minpoly_rat hζ hp.pos]
  refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩
  · 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]
  · lift i to Fin p using h; simp [cyclotomic_prime, ← hP, H i 0]
  · simp [cyclotomic_prime, P, h, Fin.forall_iff, @forall_comm _ (_ = _), Finset.sum_eq_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Semiring S
f : R →+* S
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic p R) = ↑p

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Semiring S
f : R →+* S
p k : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = ↑p

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)

Tactic:
← pow_succ',

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1 + 1)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ (aeval (ζ - 1)) (X + 1) = ζ

Tactic:
by simp

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
hirr : Irreducible (cyclotomic n K)
hn : ¬n = 2
⊢ (Algebra.norm K) ζ = 1

Tactic:
exact hζ.norm_eq_one hn hirr

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
⊢ IsMulCommutative (B ≃ₐ[A] B)

Tactic:
refine ⟨⟨fun f g ↦ algEquiv_eq_of_apply_eq S A B fun n hn h1 ↦ ?_⟩⟩
  obtain ⟨r, hr⟩ := ‹IsCyclotomicExtension S A B›.exists_isPrimitiveRoot hn h1
  use r, hr
  simp only [AlgEquiv.mul_apply]
  have := NeZero.mk h1
  obtain ⟨mf, -, hf⟩ := hr.eq_pow_of_pow_eq_one (show f r ^ n = 1 by rw [← map_pow, hr.1, map_one])
  obtain ⟨mg, -, hg⟩ := hr.eq_pow_of_pow_eq_one (show g r ^ n = 1 by rw [← map_pow, hr.1, map_one])
  simp [← hf, ← hg, ← pow_mul, mul_comm mf mg]

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
by_cases hn : n = 0
  · simp only [hn, Nat.cast_zero, isCoprime_zero_right] at h
    rcases Int.isUnit_eq_one_or h with h | h <;> simp [h]
  have : NeZero n := ⟨hn⟩
  rw [← natCast_zmod_val x]
  apply coe_mul_inv_eq_one
  rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℤ
m : ℕ
h : IsCoprime (↑m) n
⊢ ↑(unitOfIsCoprime n ⋯) = ↑n

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
⊢ IsPrimitiveRoot 1 1

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (G →* ↥S)
f : G →* Mˣ
H : ∀ (a : G), f a ∈ S
x✝ : G
⊢ (S.subtype.comp (f.codRestrict S H)) x✝ = f x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
⊢ ⟨toUnits (toCircle 0), ⋯⟩ = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
by
  rw [χ₄_int_mod_four, hn]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
by
  rw [χ₄_int_mod_four, hn]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8), χ₈' a = χ₄ a.cast * χ₈ a

Tactic:
by
  decide

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
a : ZMod n
ha : IsUnit a
⊢ χ a = ↑((toUnitHom χ) ha.unit)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ toUnitHom χ = toUnitHom ψ ↔ χ = ψ

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x : ZMod n
⊢ χ (↑n - x) = χ (-x)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ χ = χ'

Tactic:
apply ext'

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ ∀ (a : R), χ a = χ' a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ χ a * (χ a)⁻¹ʳ = χ a * χ a⁻¹ʳ

Tactic:
Ring.mul_inverse_cancel _ h,

Goal state after:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ 1 = χ a * χ a⁻¹ʳ
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n ≠ 0 → χ.conductor ≠ 0

Tactic:
exact fun h ↦ @conductor_ne_zero _ _ _ χ ⟨h⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
h : ∀ a ∈ H, χ ↑a = 1
x : (ZMod n)ˣ
hx : x ∈ Submonoid.closure H
⊢ χ ↑1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ i, χ ↑a * (χ i * ψ (↑a * i)) = ∑ a, χ a * ψ a

Tactic:
simp_rw [← mul_assoc, ← map_mul]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ x, χ (↑a * x) * ψ (↑a * x) = ∑ a, χ a * ψ a
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, ∑ i, χ i * ψ i * (χ x⁻¹ * ψ (-x)) = ↑(Fintype.card R)

Tactic:
conv =>
    enter [1, 2, x, 2, y]
    rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, ∑ y, χ (y * x⁻¹) * ψ (y - x) = ↑(Fintype.card R)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ * χ ^ (orderOf χ - 1) = 1

Tactic:
← pow_succ',

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ ^ (orderOf χ - 1 + 1) = 1
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ 1 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)

Tactic:
rw [← frobenius_def, gaussSum, gaussSum, map_sum]
  simp_rw [pow_apply' χ fp.1.ne_zero, map_mul, frobenius_def]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑p) = χ ↑p * χ ↑hp.unit * gaussSum χ (ψ.mulShift ↑hp.unit)

Tactic:
hp.unit_spec,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑p) = χ ↑p * χ ↑p * gaussSum χ (ψ.mulShift ↑p)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2) * ‖f x‖ * ‖fderiv ℝ f x‖ = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
← Real.rpow_add_one' (by positivity) (by linarith)

Goal state after:
case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2 + 1) * ‖fderiv ℝ f x‖ = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)

Tactic:
← Real.rpow_add_one' (by positivity) (by linarith)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
⊢ stdAddChar (-(k * j)) * χ j = χ j * stdAddChar (-k * j)

Tactic:
neg_mul,

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
⊢ stdAddChar (-(k * j)) * χ j = χ j * stdAddChar (-(k * j))