awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Bounds (goal)
Goal:
F : Type u_1
inst : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
⊢ norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1
have pos : ∀ (h : IsUnit a), norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1
Tactic: by_cases h : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Bounds (goal)
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
⊢ norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1
have neg : ∀ (h : ¬IsUnit a), norm (E := F) ((χ : (a : ZMod n) → F) a : F) ≤ 1
Tactic: by_cases h : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Bounds (goal)
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
have neg : LE.le (α := ℝ) 0 1
Tactic: rw [χ.map_nonunit h, norm_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
| HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e)
have rw : gaussSum χ e
Tactic: rw [← this, gaussSum_mulShift]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e
have conv_lhs : HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e
Tactic: conv_lhs => rw [← this, gaussSum_mulShift]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e
have conv_lhs₁ : gaussSum χ e = gaussSum χ e
Tactic: conv_lhs => rw [← this, gaussSum_mulShift]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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)ˣ)
⊢ HMul.hMul (α := R) ((χ : (a : ZMod N) → R) (↑u : ZMod N) : R) (gaussSum χ e) = gaussSum χ e
have suffices : e.mulShift (↑u : ZMod N) = e
Tactic: suffices e.mulShift u = e by conv_lhs => rw [← this, gaussSum_mulShift]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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)ˣ)
⊢ e.mulShift (↑u : ZMod N) = e
have rw : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
Tactic: rw [(by ring : u.val = (u - 1) + 1), ← mulShift_mul, mulShift_one, mul_eq_right]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
have 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
Tactic: rsuffices ⟨a, ha⟩ : (d : ℤ) ∣ (u.val.val - 1 : ℤ)
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
have rsuffices₁ : (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
Tactic: rsuffices ⟨a, ha⟩ : (d : ℤ) ∣ (u.val.val - 1 : ℤ)
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
have this : (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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)
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift ((↑u : ZMod N) - 1)) 1
have rw : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑((↑d : ℤ) * a) : ZMod N)) 1
Tactic: rw [this, ha]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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)
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑((↑d : ℤ) * a) : ZMod N)) 1
have 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)
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (hypothesis)
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)ˣ)
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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)
Tactic: rw [← Units.val_inj, Units.val_one, ZMod.unitsMap_def, Units.coe_map] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (hypothesis)
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)
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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)
Tactic: have : ZMod.castHom hd (ZMod d) u.val = ((u.val.val : ℤ) : ZMod d) := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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)
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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
Tactic: rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
Cleared hypotheses: hu, this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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
Tactic: rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
Cleared hypotheses: hu, this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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
Tactic: rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
Cleared hypotheses: hu, this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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
Tactic: rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
Cleared hypotheses: hu, this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ (↑d : ℤ) ∣ HSub.hSub (α := ℤ) (↑(↑u : ZMod N).val : ℤ) 1
have 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
Tactic: rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
Cleared hypotheses: hu, this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ χ.FactorsThrough d
have rw : (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
Tactic: rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
⊢ gaussSum χ e = 0
have contrapose! : ∀ (hχ : gaussSum χ e ≠ 0), ¬χ.IsPrimitive
Tactic: contrapose! hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
hχ : gaussSum χ e ≠ 0
⊢ ¬χ.IsPrimitive
have rcases : ∀ (d : ℕ) (hd₁ : d ∣ N) (hd₂ : d < N) (hed : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1),
  ¬χ.IsPrimitive
Tactic: rcases e.exists_divisor_of_not_isPrimitive he with ⟨d, hd₁, hd₂, hed⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (hypothesis)
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
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
⊢ ¬χ.IsPrimitive
have this : χ.conductor ≤ d
Tactic: have : χ.conductor ≤ d := Nat.sInf_le <| factorsThrough_of_gaussSum_ne_zero e hd₁ hed hχ
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
a : ZMod N
⊢ gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
have pos : ∀ (ha : IsUnit a), gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
a : ZMod N
pos : ∀ (ha : IsUnit a), gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
⊢ gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
have neg : ∀ (ha : ¬IsUnit a), gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.GaussSum (goal)
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
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
have neg : gaussSum χ (e.mulShift a) = 0
Tactic: rw [MulChar.map_nonunit _ ha, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Orthogonality (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card.{u_1} (DirichletCharacter R n) = n.totient
have rw : Nat.card.{u_1} (DirichletCharacter R n) = Nat.card (ZMod n)ˣ
Tactic: rw [← ZMod.card_units_eq_totient n, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Orthogonality (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0
have obtain : ∀ (χ : DirichletCharacter R n) (hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)),
  Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0
Tactic: obtain ⟨χ, hχ⟩ := exists_apply_ne_one_of_hasEnoughRootsOfUnity R ha
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Orthogonality (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0
have refine : HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n) → R) a : R)
    (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a : R) =
  ∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a
Tactic: refine eq_zero_of_mul_eq_self_left hχ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Orthogonality (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n) → R) a : R)
      (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a : R) =
    ∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a
have simp : Eq.{u_1 + 1} (α := R) (∑ x : DirichletCharacter R n, (χ * x : (a : ZMod n) → R) a)
  (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a)
Tactic: simp only [Finset.mul_sum, ← MulChar.mul_apply]