awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this_1 : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
this :
  Eq (α := DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
      DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor))
obtain :
  ∀ (w : d.gcd χ.conductor ∣ d) (χ₁ : DirichletCharacter R (d.gcd χ.conductor))
    (hχ₁ : χ₀ = (changeLevel w : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R d) χ₁),
    d.gcd χ.conductor ∈ χ.conductorSet
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
obtain ⟨_, χ₁, hχ₁⟩ := factorsThrough_gcd χ₀ χ.primitiveCharacter this

Premises used: DirichletCharacter.primitiveCharacter, DirichletCharacter.factorsThrough_gcd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this_1 : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
this :
  Eq (α := DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
      DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor))
w : d.gcd χ.conductor ∣ d
χ₁ : DirichletCharacter R (d.gcd χ.conductor)
hχ₁ : χ₀ = (changeLevel w : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R d) χ₁
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
⟨Nat.dvd_trans (d.gcd_dvd_left χ.conductor) hd, χ₁, ?_⟩

Premises used: DirichletCharacter.conductor, Nat.gcd_dvd_left, DirichletCharacter.FactorsThrough, Set.Mem, setOf, Nat.dvd_trans, DirichletCharacter.conductorSet, Exists.intro
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this_1 : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
this :
  Eq (α := DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
      DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor))
w : d.gcd χ.conductor ∣ d
χ₁ : DirichletCharacter R (d.gcd χ.conductor)
hχ₁ : χ₀ = (changeLevel w : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R d) χ₁
refine : χ = (changeLevel ⋯ : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R n) χ₁
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
refine ⟨Nat.dvd_trans (d.gcd_dvd_left χ.conductor) hd, χ₁, ?_⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this_1 : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
this :
  Eq (α := DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
      DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor))
w : d.gcd χ.conductor ∣ d
χ₁ : DirichletCharacter R (d.gcd χ.conductor)
hχ₁ : χ₀ = (changeLevel w : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R d) χ₁
rw :
  χ =
    (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R d) χ₁)
rw₁ : d ∣ n
rw₂ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
rw₃ : d ∣ n
rw₄ :
  Eq (α := DirichletCharacter R n)
    ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀ : DirichletCharacter R n)
    ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀ : DirichletCharacter R n)
rw₅ : d ∣ n
rw₆ :
  Eq (α := DirichletCharacter R n)
    ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀ : DirichletCharacter R n)
    ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀ : DirichletCharacter R n)
rw₇ : d ∣ n
⊢ χ = (changeLevel ⋯ : (a : DirichletCharacter R (d.gcd χ.conductor)) → DirichletCharacter R n) χ₁

Tactic:
rw [changeLevel_trans _ (d.gcd_dvd_left χ.conductor), ← hχ₁, hχ₀]

Premises used: DirichletCharacter.conductor, Nat.gcd_dvd_left, DirichletCharacter.changeLevel_trans
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
suffices :
  Eq (α := DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
      DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor))
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
suffices (changeLevel (d.dvd_mul_right χ.conductor)) χ₀ =
      (changeLevel (χ.conductor.dvd_mul_left d)) χ.primitiveCharacter by
    obtain ⟨_, χ₁, hχ₁⟩ := factorsThrough_gcd χ₀ χ.primitiveCharacter this
    refine ⟨Nat.dvd_trans (d.gcd_dvd_left χ.conductor) hd, χ₁, ?_⟩
    rw [changeLevel_trans _ (d.gcd_dvd_left χ.conductor), ← hχ₁, hχ₀]
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
⊢ NeZero (d * χ.conductor * n)

Tactic:
have : NeZero (d * χ.conductor * n) :=
    ⟨Nat.mul_ne_zero (Nat.mul_ne_zero (NeZero.ne d) χ.conductor_ne_zero) (NeZero.ne n)⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this_1 : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
this : NeZero (d * χ.conductor * n)
a :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀) :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
          χ.primitiveCharacter) :
      DirichletCharacter R (d * χ.conductor * n))
⊢ Eq (α := DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
      DirichletCharacter R (d * χ.conductor))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor))

Tactic:
apply changeLevel_injective <| Nat.dvd_mul_right (d * χ.conductor) n

Premises used: DirichletCharacter.changeLevel_injective, DirichletCharacter.conductor, HMul.hMul, Nat.dvd_mul_right
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∣ n
⊢ d ∈ χ.conductorSet ↔ χ.conductor ∣ d

Tactic:
⟨conductor_dvd_of_mem_conductorSet χ, fun h ↦ χ.factorsThrough_conductor.mono χ h hd⟩

Premises used: DirichletCharacter.FactorsThrough.mono, Iff.intro, DirichletCharacter.conductor_dvd_of_mem_conductorSet, DirichletCharacter.factorsThrough_conductor
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
inl : ∀ (χ : DirichletCharacter R 0), (χ ^ m).conductor ∣ χ.conductor
inr : ∀ (hn : NeZero n), (χ ^ m).conductor ∣ χ.conductor
⊢ (χ ^ m).conductor ∣ χ.conductor

Tactic:
obtain rfl | hn := eq_zero_or_neZero n

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
m : ℤ
χ : DirichletCharacter R 0
⊢ (χ ^ m).conductor ∣ χ.conductor

Tactic:
simp [conductor_eq_zero_iff_level_eq_zero.mpr]

Premises used: Iff.mpr, DirichletCharacter.conductor_eq_zero_iff_level_eq_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
inr : (χ ^ m).FactorsThrough χ.conductor
⊢ (χ ^ m).conductor ∣ χ.conductor

Tactic:
rw [← mem_conductorSet_iff_conductor_dvd _ χ.conductor_dvd_level, mem_conductorSet_iff]

Premises used: DirichletCharacter.conductor_dvd_level, DirichletCharacter.mem_conductorSet_iff_conductor_dvd, DirichletCharacter.mem_conductorSet_iff
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ (χ ^ m).FactorsThrough χ.conductor

Tactic:
⟨χ.conductor_dvd_level, χ.primitiveCharacter ^ m, ?_⟩

Premises used: DirichletCharacter.FactorsThrough, DirichletCharacter.conductor_dvd_level, DirichletCharacter.primitiveCharacter, HPow.hPow, Exists.intro
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
inr :
  χ ^ m = (changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) (χ.primitiveCharacter ^ m)
⊢ (χ ^ m).FactorsThrough χ.conductor

Tactic:
refine ⟨χ.conductor_dvd_level, χ.primitiveCharacter ^ m, ?_⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
inr :
  χ ^ m =
    HPow.hPow (α := DirichletCharacter R n)
      ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
        DirichletCharacter R n)
      m
inr₁ inr₂ : χ ^ m = χ ^ m
⊢ χ ^ m = (changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) (χ.primitiveCharacter ^ m)

Tactic:
rw [MonoidHom.map_zpow, changeLevel_primitiveCharacter]

Premises used: DirichletCharacter.changeLevel_primitiveCharacter, MonoidHom.map_zpow
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
⊢ (χ ^ m).conductor ∣ χ.conductor

Tactic:
zpow_natCast χ m ▸ conductor_zpow_dvd ..

Premises used: zpow_natCast, Eq.rec, DirichletCharacter.conductor_zpow_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
rw : (HPow.hPow (β := ℤ) χ (-1)).conductor = χ.conductor
⊢ χ⁻¹.conductor = χ.conductor

Tactic:
rw [← zpow_neg_one]

Premises used: zpow_neg_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (HPow.hPow (β := ℤ) χ (-1)).conductor = χ.conductor

Tactic:
dvd_antisymm (conductor_zpow_dvd ..) ?_

Premises used: dvd_antisymm, DirichletCharacter.conductor_zpow_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
refine : χ.conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor
⊢ (HPow.hPow (β := ℤ) χ (-1)).conductor = χ.conductor

Tactic:
refine dvd_antisymm (conductor_zpow_dvd ..) ?_

Premises used: dvd_antisymm, DirichletCharacter.conductor_zpow_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
nth_rewrite : (HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) χ (-1)) (-1)).conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor
⊢ χ.conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor

Tactic:
nth_rewrite 1 [← inv_inv χ, ← zpow_neg_one, ← zpow_neg_one]

Premises used: zpow_neg_one, inv_inv
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) χ (-1)) (-1)).conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor

Tactic:
conductor_zpow_dvd ..

Premises used: DirichletCharacter.conductor_zpow_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) χ (-1)) (-1)).conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor

Tactic:
exact conductor_zpow_dvd ..

Premises used: DirichletCharacter.conductor_zpow_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
χ : DirichletCharacter R n
ψ : DirichletCharacter R m
⊢ χ.primitive_mul ψ = (χ.mul ψ).primitiveCharacter

Tactic:
rfl

Premises used: DirichletCharacter.primitive_mul, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
ψ : DirichletCharacter R m
⊢ (χ.primitive_mul ψ).IsPrimitive

Tactic:
primitiveCharacter_isPrimitive _

Premises used: DirichletCharacter.primitiveCharacter_isPrimitive, DirichletCharacter.primitive_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
inl : ∀ (χ ψ : DirichletCharacter R 0), (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
inr : ∀ (hn : NeZero n), (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor

Tactic:
obtain rfl | hn := eq_zero_or_neZero n

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ ψ : DirichletCharacter R 0
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor

Tactic:
simp [conductor_eq_zero_iff_level_eq_zero.mpr]

Premises used: Iff.mpr, DirichletCharacter.conductor_eq_zero_iff_level_eq_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
⊢ χ.conductor.lcm ψ.conductor ∣ n

Tactic:
have h := Nat.lcm_dvd χ.conductor_dvd_level ψ.conductor_dvd_level
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
inr : (χ * ψ).FactorsThrough (χ.conductor.lcm ψ.conductor)
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor

Tactic:
rw [← mem_conductorSet_iff_conductor_dvd _ h, mem_conductorSet_iff]

Premises used: DirichletCharacter.mem_conductorSet_iff_conductor_dvd, DirichletCharacter.mem_conductorSet_iff
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ (χ * ψ).FactorsThrough (χ.conductor.lcm ψ.conductor)

Tactic:
⟨h, χ.primitiveCharacter.mul ψ.primitiveCharacter, ?_⟩

Premises used: DirichletCharacter.FactorsThrough, DirichletCharacter.mul, DirichletCharacter.primitiveCharacter, Exists.intro
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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)
      (χ.primitiveCharacter.mul ψ.primitiveCharacter)
⊢ (χ * ψ).FactorsThrough (χ.conductor.lcm ψ.conductor)

Tactic:
refine ⟨h, χ.primitiveCharacter.mul ψ.primitiveCharacter, ?_⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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)
inr₅ inr₆ : χ * ψ = χ * ψ
⊢ χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (χ.primitiveCharacter.mul ψ.primitiveCharacter)

Tactic:
rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]

Premises used: DirichletCharacter.changeLevel_trans, DirichletCharacter.mul, DirichletCharacter.changeLevel_primitiveCharacter, MonoidHom.map_mul
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
apply : d.Coprime (a.conductor.lcm b.conductor)
⊢ Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} (a * b)

Tactic:
apply Nat.Coprime.of_dvd_right (conductor_mul_dvd_lcm_conductor _ _)

Premises used: DirichletCharacter.conductor_mul_dvd_lcm_conductor, Nat.Coprime.of_dvd_right
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
⊢ d.Coprime (a.conductor.lcm b.conductor)

Tactic:
(Nat.Coprime.mul_right hχ hψ).coprime_div_right <| Nat.gcd_dvd_mul _ _

Premises used: Nat.lcm, Nat.Coprime.coprime_div_right, Nat.gcd_dvd_mul, Nat.Coprime.mul_right
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
⊢ d.Coprime (a.conductor.lcm b.conductor)

Tactic:
exact (Nat.Coprime.mul_right hχ hψ).coprime_div_right <| Nat.gcd_dvd_mul _ _

Premises used: Nat.Coprime.coprime_div_right, Nat.gcd_dvd_mul, Nat.Coprime.mul_right
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
d : ℕ
⊢ Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} 1

Tactic:
simp [conductor_one]

Premises used: DirichletCharacter.conductor_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
rwa₁ rwa₂ rwa₃ rwa₄ : d.Coprime x.conductor
⊢ Membership.mem (γ := Set (DirichletCharacter R n)) {χ : DirichletCharacter R n | d.Coprime χ.conductor} x⁻¹

Tactic:
rwa [Set.mem_setOf, conductor_inv]

Premises used: Set.mem_setOf, DirichletCharacter.conductor_inv
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
d : ℕ
χ : DirichletCharacter R n
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n)) (subgroupOfCoprimeConductor d) χ ↔ d.Coprime χ.conductor

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NoZeroDivisors S
this : HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
⊢ Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (1 : S) ∨ Eq (α := S) ((ψ : (a : ZMod m) → S) (-1) : S) (-1 : S)

Tactic:
sq_eq_one_iff.mp this

Premises used: sq_eq_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NoZeroDivisors S
this : HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
⊢ ψ.Even ∨ ψ.Odd

Tactic:
convert! sq_eq_one_iff.mp this

Premises used: sq_eq_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
S : Type u_2
inst : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst_1 : NoZeroDivisors S
suffices : HPow.hPow (α := S) (β := ℕ) ((ψ : (a : ZMod m) → S) (-1) : S) 2 = 1
⊢ ψ.Even ∨ ψ.Odd

Tactic:
suffices ψ (-1) ^ 2 = 1 by convert! sq_eq_one_iff.mp this