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
d : ℕ
inst_1 : NeZero n
this : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
⊢ d.gcd χ.conductor ∈ χ.conductorSet
have suffices : Eq (α := DirichletCharacter R (d * χ.conductor))
  ((changeLevel sorry : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀ :
    DirichletCharacter R (d * χ.conductor))
  ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
      χ.primitiveCharacter :
    DirichletCharacter R (d * χ.conductor))
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χ₀]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
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) χ₀
⊢ 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))
have this₁ : 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)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ 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))
have a : Eq (α := DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
      ((changeLevel sorry : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀) :
    DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
      ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter) :
    DirichletCharacter R (d * χ.conductor * n))
Tactic: apply changeLevel_injective <| Nat.dvd_mul_right (d * χ.conductor) n
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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)
⊢ 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))
have a : Eq (α := DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
    DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
      ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
        χ.primitiveCharacter) :
    DirichletCharacter R (d * χ.conductor * n))
Tactic: rw [← changeLevel_trans, ← changeLevel_trans,
    changeLevel_trans _ hd (n.dvd_mul_left (d * χ.conductor)), ← hχ₀,
    changeLevel_trans χ.primitiveCharacter χ.conductor_dvd_level, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      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 * 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))
have a₁ : Eq (α := DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
    DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
      χ.primitiveCharacter :
    DirichletCharacter R (d * χ.conductor * n))
Tactic: rw [← changeLevel_trans, ← changeLevel_trans,
    changeLevel_trans _ hd (n.dvd_mul_left (d * χ.conductor)), ← hχ₀,
    changeLevel_trans χ.primitiveCharacter χ.conductor_dvd_level, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      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))
a₁ :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor * n))
⊢ 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))
have a₂ : Eq (α := DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n))
      ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) :
    DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
      χ.primitiveCharacter :
    DirichletCharacter R (d * χ.conductor * n))
Tactic: rw [← changeLevel_trans, ← changeLevel_trans,
    changeLevel_trans _ hd (n.dvd_mul_left (d * χ.conductor)), ← hχ₀,
    changeLevel_trans χ.primitiveCharacter χ.conductor_dvd_level, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      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))
a₁ :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor * n))
a₂ :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor * n))
⊢ 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))
have a₃ : Eq (α := DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n)) χ :
    DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
      χ.primitiveCharacter :
    DirichletCharacter R (d * χ.conductor * n))
Tactic: rw [← changeLevel_trans, ← changeLevel_trans,
    changeLevel_trans _ hd (n.dvd_mul_left (d * χ.conductor)), ← hχ₀,
    changeLevel_trans χ.primitiveCharacter χ.conductor_dvd_level, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
⊢ (χ ^ m).conductor ∣ χ.conductor
have inl : ∀ (χ : DirichletCharacter R 0), (χ ^ m).conductor ∣ χ.conductor
Tactic: obtain rfl | hn := eq_zero_or_neZero n
Cleared hypotheses: n, χ
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
inl : ∀ (χ : DirichletCharacter R 0), (χ ^ m).conductor ∣ χ.conductor
⊢ (χ ^ m).conductor ∣ χ.conductor
have inr : ∀ (hn : NeZero n), (χ ^ m).conductor ∣ χ.conductor
Tactic: obtain rfl | hn := eq_zero_or_neZero n
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ (χ ^ m).conductor ∣ χ.conductor
have inr : (χ ^ m).FactorsThrough χ.conductor
Tactic: rw [← mem_conductorSet_iff_conductor_dvd _ χ.conductor_dvd_level, mem_conductorSet_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ (χ ^ m).FactorsThrough χ.conductor
have inr : χ ^ m = (changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) (χ.primitiveCharacter ^ m)
Tactic: refine ⟨χ.conductor_dvd_level, χ.primitiveCharacter ^ m, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ χ ^ m = (changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) (χ.primitiveCharacter ^ m)
have inr : χ ^ m =
  HPow.hPow (α := DirichletCharacter R n)
    ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter :
      DirichletCharacter R n)
    m
Tactic: rw [MonoidHom.map_zpow, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
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
⊢ χ ^ m = (changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) (χ.primitiveCharacter ^ m)
have inr₁ : χ ^ m = χ ^ m
Tactic: rw [MonoidHom.map_zpow, changeLevel_primitiveCharacter]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ⁻¹.conductor = χ.conductor
have rw : (HPow.hPow (β := ℤ) χ (-1)).conductor = χ.conductor
Tactic: rw [← zpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (HPow.hPow (β := ℤ) χ (-1)).conductor = χ.conductor
have refine : χ.conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor
Tactic: refine dvd_antisymm (conductor_zpow_dvd ..) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor
have nth_rewrite : (HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) χ (-1)) (-1)).conductor ∣ (HPow.hPow (β := ℤ) χ (-1)).conductor
Tactic: nth_rewrite 1 [← inv_inv χ, ← zpow_neg_one, ← zpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
have inl : ∀ (χ ψ : DirichletCharacter R 0), (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
Tactic: obtain rfl | hn := eq_zero_or_neZero n
Cleared hypotheses: n, χ, ψ
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
inl : ∀ (χ ψ : DirichletCharacter R 0), (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
have inr : ∀ (hn : NeZero n), (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
Tactic: obtain rfl | hn := eq_zero_or_neZero n
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
have h : χ.conductor.lcm ψ.conductor ∣ n
Tactic: have h := Nat.lcm_dvd χ.conductor_dvd_level ψ.conductor_dvd_level
-- 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
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
have inr : (χ * ψ).FactorsThrough (χ.conductor.lcm ψ.conductor)
Tactic: rw [← mem_conductorSet_iff_conductor_dvd _ h, mem_conductorSet_iff]
-- 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
⊢ (χ * ψ).FactorsThrough (χ.conductor.lcm ψ.conductor)
have inr : χ * ψ =
  (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
    (χ.primitiveCharacter.mul ψ.primitiveCharacter)
Tactic: refine ⟨h, χ.primitiveCharacter.mul ψ.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
⊢ χ * ψ =
    (changeLevel h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
      (χ.primitiveCharacter.mul ψ.primitiveCharacter)
have 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 sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
          χ.primitiveCharacter :
        DirichletCharacter R (χ.conductor.lcm ψ.conductor))
      ((changeLevel sorry : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
          ψ.primitiveCharacter :
        DirichletCharacter R (χ.conductor.lcm ψ.conductor)))
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)))
⊢ χ * ψ =
    (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 h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
        ((changeLevel sorry : (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 sorry : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
          ψ.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)
⊢ χ * ψ =
    (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 h : (a : DirichletCharacter R (χ.conductor.lcm ψ.conductor)) → DirichletCharacter R n)
        ((changeLevel sorry : (a : DirichletCharacter R ψ.conductor) → DirichletCharacter R (χ.conductor.lcm ψ.conductor))
          ψ.primitiveCharacter) :
      DirichletCharacter R n)
Tactic: rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]