mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
val✝ : Fintype K
this : (Polynomial.map (algebraMap K K) (X ^ Fintype.card K - X)).Splits
⊢ (X ^ Nat.card K - X).Splits

Tactic:
simpa using

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
val✝ : Fintype K
this : (Polynomial.map (algebraMap K K) (X ^ Fintype.card K - X)).Splits
⊢ (X ^ Fintype.card K - X).Splits
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
val✝ : Infinite K
⊢ (-(X ^ Nat.card K - X)).Splits

Tactic:
simpa using

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
val✝ : Infinite K
⊢ (X - 1).Splits
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
by
  by_cases htwo : p ^ (k - s + 1) = 2
  · obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo
    simp only [add_eq_right] at hks
    replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)
    simp only [hp, hs] at hζ hirr hcycl ⊢
    obtain ⟨k₁, hk₁⟩ := Nat.exists_eq_succ_of_ne_zero hk
    rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,
      mul_pow, neg_one_sq, one_mul, ← pow_mul, ← _root_.pow_succ']
    simp
  · exact hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
this : IsCyclic ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), x ∈ Subgroup.zpowers g
hg' : g ^ n = 1
f : ZMod n → ↥(rootsOfUnity n M) := fun j ↦ g ^ ↑j.val
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
⊢ f ↑k = x

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
this : IsCyclic ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), x ∈ Subgroup.zpowers g
hg' : g ^ n = 1
f : ZMod n → ↥(rootsOfUnity n M) := fun j ↦ g ^ ↑j.val
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
⊢ g ^ (k % ↑n) = g ^ k
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
hGalK : K ≃ₐ[ZMod p] GaloisField p ↑n
⊢ K ≃ₐ[ZMod p] K'

Tactic:
have hK'Gal := (GaloisField.algEquivGaloisFieldOfFintype p n' hK').symm

Goal state after:
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
hGalK : K ≃ₐ[ZMod p] GaloisField p ↑n
hK'Gal : GaloisField p ↑n' ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
⊢ False

Tactic:
simpa using

Goal state after:
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
⊢ False
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K

Tactic:
algebraize [f.toRingHom]

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
algInst✝ : Algebra K L := f.toAlgebra
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
x✝ : Nonempty (K →ₐ[F] L)
f : K →ₐ[F] L
⊢ Module.finrank F K ∣ Module.finrank F L

Tactic:
algebraize [f.toRingHom]

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
x✝ : Nonempty (K →ₐ[F] L)
f : K →ₐ[F] L
algInst✝ : Algebra K L := f.toAlgebra
⊢ Module.finrank F K ∣ Module.finrank F L
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℕ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ℕ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℕ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
simpa using toCircle_intCast (N := N) j

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

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8),

Goal state after:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑n = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Tactic:
← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8),

Goal state after:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ χ₈' ↑n = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
⊢ (if hx : IsUnit (x * y) then ↑(f hx.unit) else 0) =
    (if hx : IsUnit x then ↑(f hx.unit) else 0) * if hx : IsUnit y then ↑(f hx.unit) else 0

Tactic:
simp only [hx, IsUnit.mul_iff, true_and, dif_pos]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
⊢ (if h : IsUnit y then ↑(f ⋯.unit) else 0) = ↑(f ⋯.unit) * if hx : IsUnit y then ↑(f hx.unit) else 0
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : ∀ (a : (ZMod m)ˣ), ((changeLevel hm) a₁✝) ↑a = ((changeLevel hm) a₂✝) ↑a
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : ∀ (a : (ZMod m)ˣ), ((changeLevel hm) a₁✝) ↑a = ((changeLevel hm) a₂✝) ↑a
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ χ a ≠ 0 → IsUnit a

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ ¬χ a = 0 → IsUnit a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ χ a = 0 ↔ ¬IsUnit a

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ χ a = 0 ↔ ¬IsUnit a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ ↑z = ↑x

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ ↑z = ↑x
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case hS
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ ∀ n_1 ∈ {n}, n_1 ≠ 0 → ∃ r, IsPrimitiveRoot r n_1

Tactic:
simpa using

Goal state after:
case hS
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ ∃ r, IsPrimitiveRoot r n
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : χ ↑b ≠ 1
⊢ χ ↑b * ∑ a, χ a = ∑ a, χ a

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : χ ↑b ≠ 1
⊢ ∑ x, χ (↑b * x) = ∑ a, χ a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
⊢ ((changeLevel hm) χ).conductor = χ.conductor

Tactic:
have h : (changeLevel hm χ).conductor ∣ χ.conductor := by
    refine conductor_dvd_of_mem_conductorSet _
      ⟨χ.conductor_dvd_level.trans hm, χ.primitiveCharacter, ?_⟩
    rw [changeLevel_trans _ χ.conductor_dvd_level, changeLevel_primitiveCharacter]

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
h : ((changeLevel hm) χ).conductor ∣ χ.conductor
⊢ ((changeLevel hm) χ).conductor = χ.conductor
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂ ^ d) n₁
⊢ C₁ ≤ C₂

Tactic:
simpa using

Goal state after:
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂ ^ d) n₁
⊢ A[↑ζ₂ ^ d] ≤ A[↑ζ₂]
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χ : ∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1
x : (ZMod n)ˣ
hx : x ∈ Submonoid.closure H
⊢ x⁻¹ ∈ ↑(Submonoid.closure H)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
hχ : ∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1
x : (ZMod n)ˣ
hx : x ∈ Submonoid.closure H
⊢ x ∈ Subgroup.closure H
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
this : ↑u - 1 = ↑(↑(↑u).val - 1)
y : ZMod N
⊢ (e.mulShift ↑(↑d * a)) y = 1 y

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
this : ↑u - 1 = ↑(↑(↑u).val - 1)
y : ZMod N
⊢ e (↑d * (↑a * y)) = 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : CommRing R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
⊢ gaussSum χ 1 = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
R' : Type u_2
inst✝³ : CommRing R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
⊢ ∑ a, χ a = 0
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
x✝ : (ZMod N)ˣ
hu : x✝ ∈ (ZMod.unitsMap hd).ker
⊢ x✝ ∈ (MulChar.toUnitHom χ).ker

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
x✝ : (ZMod N)ˣ
hu : x✝ ∈ (ZMod.unitsMap hd).ker
⊢ χ ↑x✝ = 1
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: case pos
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Tactic:
simpa using

Goal state after:
case pos
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e
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:
by
  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.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: x p : ℝ
hp : 1 < p
⊢ HasDerivAt (fun x ↦ |x| ^ p) (p * |x| ^ (p - 2) * x) x

Tactic:
simpa using

Goal state after:
x p : ℝ
hp : 1 < p
⊢ HasDerivAt (fun x ↦ |x| ^ p) (p * |x| ^ (p - 2) * x) x
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 χ ψ ^ p = χ ↑p * gaussSum χ ψ

Tactic:
rw [_root_.gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit,
    ← mul_assoc, hp.unit_spec, ← pow_two, ← pow_apply' _ two_ne_zero, hχ.sq_eq_one, ← hp.unit_spec,
    one_apply_coe, one_mul]

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ auxDFT (fun j ↦ Φ (-j)) k = auxDFT Φ (-k)

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ ∑ x, stdAddChar (-(x * k)) • Φ (-x) = ∑ j, stdAddChar (-(j * -k)) • Φ j
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: 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 : ℝ≥0
hp : 1 < p
⊢ ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ ↑p) x‖ₑ ≤ ↑p * ‖f x‖ₑ ^ (↑p - 1) * ‖fderiv ℝ f x‖ₑ

Tactic:
simpa using

Goal state after:
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 : ℝ≥0
hp : 1 < p
⊢ ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ ↑p) x‖₊ ≤ p * ‖f x‖₊ ^ (↑p - 1) * ‖fderiv ℝ f x‖₊
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
t : Multiset α
hst : s < t
hts : t < a ::ₘ s
⊢ t.card < succ s.card

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Multiset α
a : α
t : Multiset α
hst : s < t
hts : t < a ::ₘ s
⊢ t.card ≤ s.card
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∉ s, insert a s = t
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
this : ContinuousAt (fun x ↦ p * ‖x‖ ^ (p - 1)) 0
⊢ Filter.Tendsto (fun x ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
this : ContinuousAt (fun x ↦ p * ‖x‖ ^ (p - 1)) 0
⊢ Filter.Tendsto (fun x ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
hΦ : Function.Even (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = Φ x

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
hΦ : Function.Even (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = Φ x
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
hΦ : Function.Odd (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = -Φ x

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
hΦ : Function.Odd (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = -Φ x
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:
stdAddChar_apply,

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
⊢ ↑(toCircle (-(k * j))) * χ j = χ j * ↑(toCircle (-(k * j)))
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
u₁ u₂ : ↥(t \ s).powerset
h : (fun u ↦ (↑u).disjUnion s ⋯) u₁ = (fun u ↦ (↑u).disjUnion s ⋯) u₂
⊢ u₁ = u₂

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
u₁ u₂ : ↥(t \ s).powerset
h : (fun u ↦ (↑u).disjUnion s ⋯) u₁ = (fun u ↦ (↑u).disjUnion s ⋯) u₂
⊢ ↑u₁ = ↑u₂
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
⊢ (ψ₈.char 1 ^ 4) ^ 2 = 1

pp: case refine_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
⊢ ¬ψ₈.char 1 ^ 4 = 1

Tactic:
· rw [← pow_mul, ← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide

Goal state after:
case refine_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
⊢ ¬ψ₈.char 1 ^ 4 = 1
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
⊢ dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2

Tactic:
simpa using

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
⊢ dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2