mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
⊢ (cyclotomic n K).degree ≠ 0

Tactic:
]

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
⊢ (cyclotomic n K).degree ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = ((↑(starRingEnd ℂ)).compAddChar φ) a

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = ((↑(starRingEnd ℂ)).compAddChar φ) a
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
k : Type u_3
inst✝² : AddCommGroup k
inst✝¹ : Finite k
inst✝ : Module (ZMod p) k
⊢ p ^ Module.finrank (ZMod p) k = p ^ Module.finrank (ZMod p) k

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
k : Type u_3
inst✝² : AddCommGroup k
inst✝¹ : Fintype k
inst✝ : Module (ZMod p) k
⊢ Nat.card k = Nat.card k

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case refine_2
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
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card F ^ Module.finrank F K - X) ∣
    Polynomial.map (algebraMap F L) (X ^ Fintype.card F ^ Module.finrank F L - X)

Tactic:
]

Goal state after:
case refine_2
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
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card F ^ Module.finrank F K - X) ∣
    Polynomial.map (algebraMap F L) (X ^ Fintype.card F ^ Module.finrank F L - X)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
]

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n 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
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
algInst✝ : Algebra K L := f.toAlgebra
this : Finite K
⊢ Module.finrank F K = Module.finrank F K

Tactic:
]

Goal state after:
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
inst✝ : Finite K
h : Module.finrank F K ∣ Module.finrank F L
⊢ Module.finrank F K = Module.finrank F K

Tactic:
]

Goal state after:
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
algInst✝ : Algebra K L := f.toAlgebra
⊢ Module.finrank F K ∣ Module.finrank F K * Module.finrank K L

Tactic:
]

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 K * Module.finrank K L
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ adjoin K ((cyclotomic n K).rootSet (cyclotomic n K).SplittingField) =
    adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
]

Goal state after:
case refine_2
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ adjoin K ((cyclotomic n K).rootSet (cyclotomic n K).SplittingField) =
    adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁹ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsDomain A
inst✝ : IsFractionRing A K
⊢ Function.Injective ⇑((algebraMap K (CyclotomicField n K)).comp (algebraMap A K))

Tactic:
]

Goal state after:
n : ℕ
inst✝⁹ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsDomain A
inst✝ : IsFractionRing A K
⊢ Function.Injective ⇑((algebraMap K (CyclotomicField n K)).comp (algebraMap A K))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
a : ℕ
han : a = n
x✝ : a ≠ 0
⊢ ∃ r, IsPrimitiveRoot r a

Tactic:
]

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
a : ℕ
han : a = n
x✝ : a ≠ 0
⊢ ∃ r, IsPrimitiveRoot r a
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : (cyclotomic n (CyclotomicField n K)).IsRoot μ
⊢ (cyclotomic n (CyclotomicField n K)).IsRoot μ

Tactic:
]

Goal state after:
case refine_1
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : (cyclotomic n (CyclotomicField n K)).IsRoot μ
⊢ (cyclotomic n (CyclotomicField n K)).IsRoot μ
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ IsPrimitiveRoot μ n

Tactic:
]

Goal state after:
case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ IsPrimitiveRoot μ n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ y ^ n = 1

Tactic:
]

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ y ^ n = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ ↑(toCircle j) = ↑(toCircle j)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
t : ZMod N
ht : t = 0
⊢ t = 0

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
t : ZMod N
ht : t = 0
⊢ t = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ (rootsOfUnitytoCircle n) (z ^ n) = (rootsOfUnitytoCircle n) 1

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ (rootsOfUnitytoCircle n) (z ^ n) = (rootsOfUnitytoCircle n) 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x✝ : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑⟨x, hx⟩ ≠ 0

Tactic:
]

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x✝ : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑⟨x, hx⟩ ≠ 0
Module: Mathlib.Data.Int.Range

Goal state before:
pp: m n r : ℤ
h : m ≤ r ∧ r < n
⊢ m + ↑(r - m).toNat < n ∧ m + ↑(r - m).toNat = r

Tactic:
simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]

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

Goal state before:
pp: case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap A (CyclotomicField n K)) (z, w).1 = (algebraMap A (CyclotomicField n K)) z

Tactic:
]

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

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑(n % 4) = χ₄ ↑(n % 4)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Tactic:
]

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)

Tactic:
]

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

Tactic:
]

Goal state after:
n : ℕ
hn : n % 4 = 1
⊢ χ₄ ↑1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

Tactic:
]

Goal state after:
n : ℕ
hn : n % 4 = 3
⊢ χ₄ ↑3 = -1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

Tactic:
]

Goal state after:
n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

Tactic:
]

Goal state after:
n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑3 = -1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
⊢ χ₈ ↑(n % 8) = χ₈ ↑(n % 8)

Tactic:
]

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

Goal state before:
pp: n : ℤ
⊢ χ₈ ↑(n % 8) = χ₈ ↑(n % 8)

Tactic:
]

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 % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
]

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 % ↑8) = 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 % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Tactic:
]

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 % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: a : ℤ
⊢ χ₈' ↑a = χ₄ (↑a).cast * χ₈ ↑a

Tactic:
]

Goal state after:
a : ℤ
⊢ χ₈' ↑a = χ₄ (↑a).cast * χ₈ ↑a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

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

Tactic:
]

Goal state after:
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:
]

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

Goal state before:
pp: case refine_3
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 +
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
]

Goal state after:
case refine_3
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 +
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1
Module: Mathlib.NumberTheory.MulChar.Basic

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

Tactic:
]

Goal state after:
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:
]

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.DirichletCharacter.Basic

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

Tactic:
]

Goal state after:
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
hy : IsUnit y
hm : ⋯.unit = hx.unit * hy.unit
⊢ ↑(f ⋯.unit) = ↑(f ⋯.unit) * ↑(f ⋯.unit)

Tactic:
hm,

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
hy : IsUnit y
hm : ⋯.unit = hx.unit * hy.unit
⊢ ↑(f (hx.unit * hy.unit)) = ↑(f ⋯.unit) * ↑(f ⋯.unit)
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
hy : IsUnit y
hm : ⋯.unit = hx.unit * hy.unit
⊢ ↑(f hx.unit * f hy.unit) = ↑(f ⋯.unit) * ↑(f ⋯.unit)

Tactic:
]

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
hy : IsUnit y
hm : ⋯.unit = hx.unit * hy.unit
⊢ ↑(f hx.unit * f hy.unit) = ↑(f ⋯.unit) * ↑(f ⋯.unit)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ χ ↑a = χ ↑a

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_3
inst✝ : CommMonoidWithZero R'
g : Rˣ
hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g
χ₁ χ₂ : MulChar R R'
⊢ ↑((equivToUnitHom χ₁) g) = ↑((equivToUnitHom χ₂) g) ↔ ↑((equivToUnitHom χ₁) g) = ↑((equivToUnitHom χ₂) g)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_3
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
S : Submonoid R
x : (↥S)ˣ
⊢ ↑(f ↑(S.unitsEquivUnitsType.symm x)) = ↑(f ↑(S.unitsEquivUnitsType.symm x))

Tactic:
]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Fintype Rˣ
a : Rˣ
χ : MulChar R R'
⊢ (equivToUnitHom χ) 1 = (equivToUnitHom χ) 1

Tactic:
]

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'
x : Rˣ
⊢ χ ↑x = χ ↑x

Tactic:
]

Goal state after: