awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NoZeroDivisors S
rw : Eq (α := S) ((ψ : (a : ZMod m) → S) (HPow.hPow (α := ZMod m) (β := ℕ) (-1) 2) : S) (1 : S)
rw₁ : Eq (α := S) ((ψ : (a : ZMod m) → S) 1 : S) (1 : S)
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 1 1
⊢ HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1

Tactic:
rw [← map_pow _, neg_one_sq, map_one]

Premises used: neg_one_sq, map_pow, map_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NeZero.{u_2} (R := S) 2
h : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (1 : S)
h' : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (-1 : S)
⊢ False

Tactic:
simp only [h', neg_eq_iff_add_eq_zero, one_add_one_eq_two, two_ne_zero] at h

Premises used: neg_eq_iff_add_eq_zero, one_add_one_eq_two, two_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NeZero.{u_2} (R := S) 2
hψ : ψ.Even
⊢ ¬ψ.Odd

Tactic:
not_and.mp ψ.not_even_and_odd hψ

Premises used: DirichletCharacter.not_even_and_odd, Iff.mp, not_and
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NeZero.{u_2} (R := S) 2
hψ : ψ.Odd
⊢ ¬ψ.Even

Tactic:
not_and'.mp ψ.not_even_and_odd hψ

Premises used: DirichletCharacter.not_even_and_odd, Iff.mp, not_and'
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
rw : Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑(-1) : S) : S)
⊢ Eq (α := Sˣ) ((toUnitHom ψ : (a : (ZMod m)ˣ) → Sˣ) (-1) : Sˣ) (-1 : Sˣ)

Tactic:
rw [← Units.val_inj, MulChar.coe_toUnitHom]

Premises used: Units.val_inj, MulChar.coe_toUnitHom
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑(-1) : S) : S)

Tactic:
hψ

Premises used: DirichletCharacter.Odd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑(-1) : S) : S)

Tactic:
exact hψ
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
rw : Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑1 : S) : S)
⊢ Eq (α := Sˣ) ((toUnitHom ψ : (a : (ZMod m)ˣ) → Sˣ) (-1) : Sˣ) (1 : Sˣ)

Tactic:
rw [← Units.val_inj, MulChar.coe_toUnitHom]

Premises used: Units.val_inj, MulChar.coe_toUnitHom
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑1 : S) : S)

Tactic:
hψ

Premises used: DirichletCharacter.Even
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑1 : S) : S)

Tactic:
exact hψ
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ.Odd
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (-1 : S)

Tactic:
rw [Odd] at hψ

Premises used: DirichletCharacter.Odd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (-1 : S)
rw :
  HMul.hMul (α := S) (β := S) ((ψ : (a : ZMod m) → S) (-1) : S) ((ψ : (a : ZMod m) → S) x : S) =
    -(ψ : (a : ZMod m) → S) x
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-x) : S) (-(ψ : (a : ZMod m) → S) x : S)

Tactic:
rw [← neg_one_mul, map_mul]

Premises used: neg_one_mul, map_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (-1 : S)
⊢ HMul.hMul (α := S) (β := S) ((ψ : (a : ZMod m) → S) (-1) : S) ((ψ : (a : ZMod m) → S) x : S) =
    -(ψ : (a : ZMod m) → S) x

Tactic:
simp [hψ]
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ.Even
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (1 : S)

Tactic:
rw [Even] at hψ

Premises used: DirichletCharacter.Even
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (1 : S)
rw :
  HMul.hMul (α := S) (β := S) ((ψ : (a : ZMod m) → S) (-1) : S) ((ψ : (a : ZMod m) → S) x : S) =
    (ψ : (a : ZMod m) → S) x
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-x) : S) ((ψ : (a : ZMod m) → S) x : S)

Tactic:
rw [← neg_one_mul, map_mul]

Premises used: neg_one_mul, map_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((ψ : (a : ZMod m) → S) (-1) : S) ((ψ : (a : ZMod m) → S) x : S) =
    (ψ : (a : ZMod m) → S) x

Tactic:
simp [hψ]
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Even
x : ZMod m
rw : Eq (α := S) ((χ : (a : ZMod m) → S) (-1 * x) : S) ((χ : (a : ZMod m) → S) x : S)
rw₁ :
  HMul.hMul (α := S) (β := S) ((χ : (a : ZMod m) → S) (-1) : S) ((χ : (a : ZMod m) → S) x : S) =
    (χ : (a : ZMod m) → S) x
rw₂ : HMul.hMul (α := S) (β := S) (1 : S) ((χ : (a : ZMod m) → S) x : S) = (χ : (a : ZMod m) → S) x
rw₃ rw₄ : Eq (α := S) ((χ : (a : ZMod m) → S) x : S) ((χ : (a : ZMod m) → S) x : S)
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) ((χ : (a : ZMod m) → S) x : S)

Tactic:
rw [← neg_one_mul, map_mul, hχ, one_mul]

Premises used: neg_one_mul, map_mul, one_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Odd
x : ZMod m
rw : Eq (α := S) ((χ : (a : ZMod m) → S) (-1 * x) : S) (-(χ : (a : ZMod m) → S) x : S)
rw₁ :
  HMul.hMul (α := S) (β := S) ((χ : (a : ZMod m) → S) (-1) : S) ((χ : (a : ZMod m) → S) x : S) =
    -(χ : (a : ZMod m) → S) x
rw₂ : HMul.hMul (α := S) (β := S) (-1 : S) ((χ : (a : ZMod m) → S) x : S) = -(χ : (a : ZMod m) → S) x
rw₃ rw₄ : Eq (α := S) (-(χ : (a : ZMod m) → S) x : S) (-(χ : (a : ZMod m) → S) x : S)
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) (-(χ : (a : ZMod m) → S) x : S)

Tactic:
rw [← neg_one_mul, map_mul, hχ, neg_one_mul]

Premises used: neg_one_mul, map_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) = 1

Tactic:
(pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_

Premises used: Nat.card_pos, LT.lt.ne', Iff.mp, pow_eq_one_iff_of_nonneg, norm_nonneg
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
refine : norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) = 1

Tactic:
refine (pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_

Premises used: Nat.card_pos, LT.lt.ne', Iff.mp, pow_eq_one_iff_of_nonneg, norm_nonneg
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
rw : ‖HPow.hPow (α := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) (Nat.card (ZMod n)ˣ)‖ = 1
rw₁ : norm (E := F) ((χ : (a : ZMod n) → F) ((↑a : ZMod n) ^ Nat.card (ZMod n)ˣ) : F) = 1
rw₂ : norm (E := F) ((χ : (a : ZMod n) → F) (↑(a ^ Nat.card (ZMod n)ˣ) : ZMod n) : F) = 1
rw₃ : norm (E := F) ((χ : (a : ZMod n) → F) (↑1 : ZMod n) : F) = 1
rw₄ : norm (E := F) ((χ : (a : ZMod n) → F) 1 : F) = 1
rw₅ : norm.{u_1} (E := F) 1 = 1
rw₆ rw₇ : Eq (α := ℝ) 1 1
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1

Tactic:
rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]

Premises used: norm_pow, NormOneClass.norm_one, map_pow, pow_card_eq_one', map_one, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
pos : ∀ (h : IsUnit a), norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1
neg : ∀ (h : ¬IsUnit a), norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1
⊢ norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1

Tactic:
by_cases h : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : IsUnit a
⊢ norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1

Tactic:
(χ.unit_norm_eq_one h.unit).le

Premises used: DirichletCharacter.unit_norm_eq_one, Eq.le, IsUnit.unit
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : IsUnit a
⊢ norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1

Tactic:
exact (χ.unit_norm_eq_one h.unit).le

Premises used: DirichletCharacter.unit_norm_eq_one, Eq.le, IsUnit.unit
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
neg : LE.le (α := ℝ) 0 1
⊢ norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1

Tactic:
rw [χ.map_nonunit h, norm_zero]

Premises used: norm_zero, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Bounds
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
this : e.mulShift (↑u : ZMod N) = e
rw : gaussSum χ e
| HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e)

Tactic:
rw [← this, gaussSum_mulShift]

Premises used: gaussSum_mulShift
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
this : e.mulShift (↑u : ZMod N) = e
conv_lhs : HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e
conv_lhs₁ : gaussSum χ e = gaussSum χ e
⊢ HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e

Tactic:
conv_lhs => rw [← this, gaussSum_mulShift]

Premises used: gaussSum_mulShift
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
suffices : e.mulShift (↑u : ZMod N) = e
⊢ HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e

Tactic:
suffices e.mulShift u = e by conv_lhs => rw [← this, gaussSum_mulShift]
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
⊢ (↑u : ZMod N) = (↑u : ZMod N) - 1 + 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
rw : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
⊢ e.mulShift (↑u : ZMod N) = e

Tactic:
rw [(by ring : u.val = (u - 1) + 1), ← mulShift_mul, mulShift_one, mul_eq_right]

Premises used: AddChar.mulShift_one, mul_eq_right, AddChar.mulShift_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
rsuffices :
  ∀ (a : ℤ) (ha : HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1 = (↑d : ℤ) * a),
    Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
rsuffices₁ : (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1

Tactic:
rsuffices ⟨a, ha⟩ : (d : ℤ) ∣ (u.val.val - 1 : ℤ)

Premises used: Units.val, HSub.hSub, Nat.cast, OfNat.ofNat, ZMod.val
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
a : ℤ
ha : HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1 = (↑d : ℤ) * a
⊢ (↑u : ZMod N) - 1 = (↑(HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1) : ZMod N)

Tactic:
simp only [ZMod.natCast_val, Int.cast_sub,
      ZMod.intCast_cast, ZMod.cast_id', id_eq, Int.cast_one]

Premises used: Int.cast_sub, ZMod.natCast_val, ZMod.cast_id', ZMod.intCast_cast, Int.cast_one, id_eq
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
a : ℤ
ha : HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1 = (↑d : ℤ) * a
⊢ (↑u : ZMod N) - 1 = (↑(HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1) : ZMod N)

Tactic:
have : u.val - 1 = ↑(u.val.val - 1 : ℤ) := by simp only [ZMod.natCast_val, Int.cast_sub,
      ZMod.intCast_cast, ZMod.cast_id', id_eq, Int.cast_one]
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
a : ℤ
ha : HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1 = (↑d : ℤ) * a
this : (↑u : ZMod N) - 1 = (↑(HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1) : ZMod N)
rw : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑((↑d : ℤ) * a) : ZMod N)) 1
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1

Tactic:
rw [this, ha]
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
a : ℤ
ha : HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1 = (↑d : ℤ) * a
this : (↑u : ZMod N) - 1 = (↑(HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1) : ZMod N)
h :
  ∀ (y : ZMod N),
    Eq.{u_1 + 1} (α := R) ((e.mulShift (↑((↑d : ℤ) * a) : ZMod N) : (a : ZMod N) → R) y : R)
      ((1 : (a : ZMod N) → R) y : R)
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑((↑d : ℤ) * a) : ZMod N)) 1

Tactic:
ext1 y
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
a : ℤ
ha : HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1 = (↑d : ℤ) * a
this : (↑u : ZMod N) - 1 = (↑(HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1) : ZMod N)
y : ZMod N
⊢ Eq.{u_1 + 1} (α := R) ((e.mulShift (↑((↑d : ℤ) * a) : ZMod N) : (a : ZMod N) → R) y : R)
    ((1 : (a : ZMod N) → R) y : R)

Tactic:
simpa only [Int.cast_mul, Int.cast_natCast, mulShift_apply, mul_assoc, one_apply]
      using DFunLike.ext_iff.mp he (a * y)

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, mul_assoc, AddChar.mulShift_apply, DFunLike.ext_iff, AddChar.one_apply, Int.cast_mul, Iff.mp
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod N)ˣ) → (ZMod d)ˣ) u : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
⊢ Eq (α := ZMod d) (((↑(ZMod.castHom hd (ZMod d)) : ZMod N →* ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    (1 : ZMod d)

Tactic:
rw [← Units.val_inj, Units.val_one, ZMod.unitsMap_def, Units.coe_map] at hu

Premises used: Units.coe_map, Units.val_inj, Units.val_one, ZMod.unitsMap_def
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod d) (((↑(ZMod.castHom hd (ZMod d)) : ZMod N →* ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    (1 : ZMod d)
⊢ Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod d) (((↑(ZMod.castHom hd (ZMod d)) : ZMod N →* ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    (1 : ZMod d)
⊢ Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)

Tactic:
have : ZMod.castHom hd (ZMod d) u.val = ((u.val.val : ℤ) : ZMod d) := by simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod d) (((↑(ZMod.castHom hd (ZMod d)) : ZMod N →* ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    (1 : ZMod d)
this :
  Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
    ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)
rwa :
  ∀ (hu : Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d) (1 : ZMod d))
    (this :
      Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
        ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)),
    (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
rwa₁ :
  ∀ (hu : Eq (α := ZMod d) (↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) 1)
    (this :
      Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
        ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)),
    (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
rwa₂ :
  ∀ (hu : Eq (α := ZMod d) (↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) (↑1 : ZMod d))
    (this :
      Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
        ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)),
    (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
rwa₃ :
  ∀ (hu : Eq (α := ZMod d) (↑1 : ZMod d) (↑(↑(↑u : ZMod N).val : ℤ) : ZMod d))
    (this :
      Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
        ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)),
    (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (hu : (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1)
    (this :
      Eq (α := ZMod d) ((ZMod.castHom hd (ZMod d) : (a : ZMod N) → ZMod d) (↑u : ZMod N) : ZMod d)
        ((↑(↑(↑u : ZMod N).val : ℤ) : ZMod d) : ZMod d)),
    (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1

Tactic:
rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub, MonoidHom.coe_coe, eq_comm, Int.cast_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
h_ne : gaussSum χ e ≠ 0
rw : (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
⊢ χ.FactorsThrough d

Tactic:
rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]

Premises used: DirichletCharacter.factorsThrough_iff_ker_unitsMap
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
h_ne : gaussSum χ e ≠ 0
x : (ZMod N)ˣ
hu : x ∈ (ZMod.unitsMap hd).ker
⊢ x ∈ (MulChar.toUnitHom χ).ker

Tactic:
simpa [← Units.val_inj, h_ne] using gaussSum_aux_of_mulShift e χ hd he hu

Premises used: gaussSum_aux_of_mulShift, Units.val_inj
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
contrapose! : ∀ (hχ : gaussSum χ e ≠ 0), ¬χ.IsPrimitive
⊢ gaussSum χ e = 0

Tactic:
contrapose! hχ