awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
inr :
  χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (HMul.hMul (α := DirichletCharacter R (χ.conductor.lcm ψ.conductor)) (β :=
        DirichletCharacter R (χ.conductor.lcm ψ.conductor))
        ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            χ.primitiveCharacter :
          DirichletCharacter R (χ.conductor.lcm ψ.conductor))
        ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter :
          DirichletCharacter R (χ.conductor.lcm ψ.conductor)))
inr₁ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            χ.primitiveCharacter) :
        DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter) :
        DirichletCharacter R n)
inr₂ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
        DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter) :
        DirichletCharacter R n)
⊢ χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (χ.primitiveCharacter.mul ψ.primitiveCharacter)
have inr₃ : χ * ψ =
  HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
    ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
      DirichletCharacter R n)
    ((changeLevel sorry : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R n) ψ.primitiveCharacter :
      DirichletCharacter R n)
Tactic: rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
inr :
  χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (HMul.hMul (α := DirichletCharacter R (χ.conductor.lcm ψ.conductor)) (β :=
        DirichletCharacter R (χ.conductor.lcm ψ.conductor))
        ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            χ.primitiveCharacter :
          DirichletCharacter R (χ.conductor.lcm ψ.conductor))
        ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter :
          DirichletCharacter R (χ.conductor.lcm ψ.conductor)))
inr₁ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            χ.primitiveCharacter) :
        DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter) :
        DirichletCharacter R n)
inr₂ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
        DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter) :
        DirichletCharacter R n)
inr₃ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
        DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R n) ψ.primitiveCharacter :
        DirichletCharacter R n)
⊢ χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (χ.primitiveCharacter.mul ψ.primitiveCharacter)
have inr₄ : χ * ψ =
  HMul.hMul (β := DirichletCharacter R n) χ
    ((changeLevel sorry : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R n) ψ.primitiveCharacter :
      DirichletCharacter R n)
Tactic: rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
inr :
  χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (HMul.hMul (α := DirichletCharacter R (χ.conductor.lcm ψ.conductor)) (β :=
        DirichletCharacter R (χ.conductor.lcm ψ.conductor))
        ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            χ.primitiveCharacter :
          DirichletCharacter R (χ.conductor.lcm ψ.conductor))
        ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter :
          DirichletCharacter R (χ.conductor.lcm ψ.conductor)))
inr₁ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            χ.primitiveCharacter) :
        DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter) :
        DirichletCharacter R n)
inr₂ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
        DirichletCharacter R n)
      ((changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
          ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
            ψ.primitiveCharacter) :
        DirichletCharacter R n)
inr₃ :
  χ * ψ =
    HMul.hMul (α := DirichletCharacter R n) (β := DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
        DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R n) ψ.primitiveCharacter :
        DirichletCharacter R n)
inr₄ :
  χ * ψ =
    HMul.hMul (β := DirichletCharacter R n) χ
      ((changeLevel ⋯ : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R n) ψ.primitiveCharacter :
        DirichletCharacter R n)
⊢ χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (χ.primitiveCharacter.mul ψ.primitiveCharacter)
have inr₅ : χ * ψ = χ * ψ
Tactic: rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
d : ℕ
a b : DirichletCharacter R n
hχ : Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} a
hψ : Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} b
⊢ Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} (a * b)
have apply : d.Coprime (a.conductor.lcm b.conductor)
Tactic: apply Nat.Coprime.of_dvd_right (conductor_mul_dvd_lcm_conductor _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
d : ℕ
x : DirichletCharacter R n
hχ : Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} x
⊢ Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} x⁻¹
have rwa : d.Coprime x⁻¹.conductor
Tactic: rwa [Set.mem_setOf, conductor_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
d : ℕ
x : DirichletCharacter R n
hχ : Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} x
rwa : d.Coprime x⁻¹.conductor
⊢ Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} x⁻¹
have rwa₁ : d.Coprime x.conductor
Tactic: rwa [Set.mem_setOf, conductor_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NoZeroDivisors S
⊢ ψ.Even ∨ ψ.Odd
have suffices : HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
Tactic: suffices ψ (-1) ^ 2 = 1 by convert! sq_eq_one_iff.mp this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NoZeroDivisors S
⊢ HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
have rw : Eq (α := S) ((ψ : (a : ZMod m) → S) (HPow.hPow (α := ZMod m) (β := ℕ) (-1) 2) : S) (1 : S)
Tactic: rw [← map_pow _, neg_one_sq, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
have rw₁ : Eq (α := S) ((ψ : (a : ZMod m) → S) 1 : S) (1 : S)
Tactic: rw [← map_pow _, neg_one_sq, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
have rw₂ : Eq.{u_2 + 1} (α := S) 1 1
Tactic: rw [← map_pow _, neg_one_sq, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ Eq (α := Sˣ) ((toUnitHom ψ : (a : (ZMod m)ˣ) → Sˣ) (-1) : Sˣ) (-1 : Sˣ)
have rw : Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑(-1) : S) : S)
Tactic: rw [← Units.val_inj, MulChar.coe_toUnitHom]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ Eq (α := Sˣ) ((toUnitHom ψ : (a : (ZMod m)ˣ) → Sˣ) (-1) : Sˣ) (1 : Sˣ)
have rw : Eq (α := S) ((ψ : (a : ZMod m) → S) (↑(-1) : ZMod m) : S) ((↑1 : S) : S)
Tactic: rw [← Units.val_inj, MulChar.coe_toUnitHom]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ.Odd
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-x) : S) (-(ψ : (a : ZMod m) → S) x : S)
have hψ₁ : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (-1 : S)
Tactic: rw [Odd] at hψ
Cleared hypotheses: hψ
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-x) : S) (-(ψ : (a : ZMod m) → S) x : S)
have rw : HMul.hMul (α := S) (β := S) ((ψ : (a : ZMod m) → S) (-1) : S) ((ψ : (a : ZMod m) → S) x : S) = -(ψ : (a : ZMod m) → S) x
Tactic: rw [← neg_one_mul, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ.Even
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-x) : S) ((ψ : (a : ZMod m) → S) x : S)
have hψ₁ : Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (1 : S)
Tactic: rw [Even] at hψ
Cleared hypotheses: hψ
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-x) : S) ((ψ : (a : ZMod m) → S) x : S)
have rw : HMul.hMul (α := S) (β := S) ((ψ : (a : ZMod m) → S) (-1) : S) ((ψ : (a : ZMod m) → S) x : S) = (ψ : (a : ZMod m) → S) x
Tactic: rw [← neg_one_mul, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Even
x : ZMod m
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) ((χ : (a : ZMod m) → S) x : S)
have rw : Eq (α := S) ((χ : (a : ZMod m) → S) (-1 * x) : S) ((χ : (a : ZMod m) → S) x : S)
Tactic: rw [← neg_one_mul, map_mul, hχ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) ((χ : (a : ZMod m) → S) x : S)
have rw₁ : HMul.hMul (α := S) (β := S) ((χ : (a : ZMod m) → S) (-1) : S) ((χ : (a : ZMod m) → S) x : S) = (χ : (a : ZMod m) → S) x
Tactic: rw [← neg_one_mul, map_mul, hχ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) ((χ : (a : ZMod m) → S) x : S)
have rw₂ : HMul.hMul (α := S) (β := S) (1 : S) ((χ : (a : ZMod m) → S) x : S) = (χ : (a : ZMod m) → S) x
Tactic: rw [← neg_one_mul, map_mul, hχ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) ((χ : (a : ZMod m) → S) x : S)
have rw₃ : Eq (α := S) ((χ : (a : ZMod m) → S) x : S) ((χ : (a : ZMod m) → S) x : S)
Tactic: rw [← neg_one_mul, map_mul, hχ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Odd
x : ZMod m
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) (-(χ : (a : ZMod m) → S) x : S)
have rw : Eq (α := S) ((χ : (a : ZMod m) → S) (-1 * x) : S) (-(χ : (a : ZMod m) → S) x : S)
Tactic: rw [← neg_one_mul, map_mul, hχ, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) (-(χ : (a : ZMod m) → S) x : S)
have rw₁ : HMul.hMul (α := S) (β := S) ((χ : (a : ZMod m) → S) (-1) : S) ((χ : (a : ZMod m) → S) x : S) = -(χ : (a : ZMod m) → S) x
Tactic: rw [← neg_one_mul, map_mul, hχ, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) (-(χ : (a : ZMod m) → S) x : S)
have rw₂ : HMul.hMul (α := S) (β := S) (-1 : S) ((χ : (a : ZMod m) → S) x : S) = -(χ : (a : ZMod m) → S) x
Tactic: rw [← neg_one_mul, map_mul, hχ, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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
⊢ Eq (α := S) ((χ : (a : ZMod m) → S) (-x) : S) (-(χ : (a : ZMod m) → S) x : S)
have rw₃ : 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]
-- 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 : ZMod n) : F) = 1
have refine : norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
Tactic: refine (pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_
-- 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 : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
have rw : ‖HPow.hPow (α := 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]
-- 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)ˣ
rw : ‖HPow.hPow (α := 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) ^ Nat.card (ZMod n)ˣ = 1
have rw₁ : norm (E := F) ((χ : (a : ZMod n) → F) ((↑a : ZMod n) ^ Nat.card (ZMod n)ˣ) : F) = 1
Tactic: rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]
-- 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)ˣ
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
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
have rw₂ : norm (E := F) ((χ : (a : ZMod n) → F) (↑(a ^ Nat.card (ZMod n)ˣ) : ZMod n) : F) = 1
Tactic: rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]
-- 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)ˣ
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
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
have rw₃ : norm (E := F) ((χ : (a : ZMod n) → F) (↑1 : ZMod n) : F) = 1
Tactic: rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]
-- 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)ˣ
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
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
have rw₄ : norm (E := F) ((χ : (a : ZMod n) → F) 1 : F) = 1
Tactic: rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]
-- 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)ˣ
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
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
have rw₅ : norm.{u_1} (E := F) 1 = 1
Tactic: rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]
-- 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)ˣ
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
⊢ norm (E := F) ((χ : (a : ZMod n) → F) (↑a : ZMod n) : F) ^ Nat.card (ZMod n)ˣ = 1
have rw₆ : Eq (α := ℝ) 1 1
Tactic: rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]