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
h : χ.FactorsThrough d
⊢ ∃! χ' : DirichletCharacter R d, χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) χ'
have rcases : ∀ (hd : d ∣ n) (χ₂ : DirichletCharacter R d),
  ∃! χ' : DirichletCharacter R d,
    Eq (α := DirichletCharacter R n)
      ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₂ : DirichletCharacter R n)
      ((changeLevel sorry : (a : DirichletCharacter R d) → DirichletCharacter R n) χ' : DirichletCharacter R n)
Tactic: rcases h with ⟨hd, χ₂, rfl⟩
Cleared hypotheses: χ, h
-- 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
hd : d ∣ n
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
have refine_1 : χ.FactorsThrough d →
  ∀ (x : (ZMod n)ˣ) (hx : x ∈ (ZMod.unitsMap hd).ker) (w : d ∣ n) (χ₀ : DirichletCharacter R d)
    (hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀), x ∈ (toUnitHom χ).ker
Tactic: refine ⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩
-- 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
hd : d ∣ n
refine_1 :
  χ.FactorsThrough d →
    ∀ (x : (ZMod n)ˣ) (hx : x ∈ (ZMod.unitsMap hd).ker) (w : d ∣ n) (χ₀ : DirichletCharacter R d)
      (hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀), x ∈ (toUnitHom χ).ker
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
have refine_2 : ∀ (h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker), χ.FactorsThrough d
Tactic: refine ⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩
-- 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
hd : d ∣ n
h : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
⊢ x ∈ (toUnitHom χ).ker
have refine_1 : Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
Tactic: rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
-- 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
hd : d ∣ n
h : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
refine_1 : Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
⊢ x ∈ (toUnitHom χ).ker
have refine_1₁ : Eq.{u_1 + 1} (α := Rˣ)
  ((toUnitHom ((changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) : (a : (ZMod n)ˣ) → Rˣ) x :
    Rˣ)
  (1 : Rˣ)
Tactic: rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
-- 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
hd : d ∣ n
h : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
refine_1 : Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
refine_1₁ :
  Eq.{u_1 + 1} (α := Rˣ)
    ((toUnitHom ((changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) : (a : (ZMod n)ˣ) → Rˣ) x :
      Rˣ)
    (1 : Rˣ)
⊢ x ∈ (toUnitHom χ).ker
have refine_1₂ : Eq (α := Rˣ) (((toUnitHom χ₀).comp (ZMod.unitsMap w) : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
Tactic: rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
-- 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
hd : d ∣ n
h : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
refine_1 : Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
refine_1₁ :
  Eq.{u_1 + 1} (α := Rˣ)
    ((toUnitHom ((changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) : (a : (ZMod n)ˣ) → Rˣ) x :
      Rˣ)
    (1 : Rˣ)
refine_1₂ : Eq (α := Rˣ) (((toUnitHom χ₀).comp (ZMod.unitsMap w) : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
⊢ x ∈ (toUnitHom χ).ker
have refine_1₃ : Eq (α := Rˣ)
  ((toUnitHom χ₀ : (a : (ZMod d)ˣ) → Rˣ) ((ZMod.unitsMap w : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) : Rˣ) (1 : Rˣ)
Tactic: rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
-- 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
hd : d ∣ n
h : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
refine_1 : Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
refine_1₁ :
  Eq.{u_1 + 1} (α := Rˣ)
    ((toUnitHom ((changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) : (a : (ZMod n)ˣ) → Rˣ) x :
      Rˣ)
    (1 : Rˣ)
refine_1₂ : Eq (α := Rˣ) (((toUnitHom χ₀).comp (ZMod.unitsMap w) : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
refine_1₃ :
  Eq (α := Rˣ)
    ((toUnitHom χ₀ : (a : (ZMod d)ˣ) → Rˣ) ((ZMod.unitsMap w : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) : Rˣ)
    (1 : Rˣ)
⊢ x ∈ (toUnitHom χ).ker
have refine_1₄ : Eq (α := Rˣ) ((toUnitHom χ₀ : (a : (ZMod d)ˣ) → Rˣ) 1 : Rˣ) (1 : Rˣ)
Tactic: rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
-- 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
hd : d ∣ n
h : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
refine_1 : Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
refine_1₁ :
  Eq.{u_1 + 1} (α := Rˣ)
    ((toUnitHom ((changeLevel w : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) : (a : (ZMod n)ˣ) → Rˣ) x :
      Rˣ)
    (1 : Rˣ)
refine_1₂ : Eq (α := Rˣ) (((toUnitHom χ₀).comp (ZMod.unitsMap w) : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
refine_1₃ :
  Eq (α := Rˣ)
    ((toUnitHom χ₀ : (a : (ZMod d)ˣ) → Rˣ) ((ZMod.unitsMap w : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) : Rˣ)
    (1 : Rˣ)
refine_1₄ : Eq (α := Rˣ) ((toUnitHom χ₀ : (a : (ZMod d)ˣ) → Rˣ) 1 : Rˣ) (1 : Rˣ)
⊢ x ∈ (toUnitHom χ).ker
have refine_1₅ : Eq.{u_1 + 1} (α := Rˣ) 1 1
Tactic: rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
⊢ χ.FactorsThrough d
have hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
Tactic: have hE : E.comp (ZMod.unitsMap hd) = χ.toUnitHom := MonoidHom.liftOfRightInverse_comp ..
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
⊢ χ.FactorsThrough d
have refine_2 : toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
Tactic: refine ⟨hd, MulChar.ofUnitHom E, equivToUnitHom.injective (?_ : toUnitHom _ = toUnitHom _)⟩
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
⊢ toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
have refine_2 : toUnitHom χ = (ofUnitHom E).toUnitHom.comp (ZMod.unitsMap hd)
Tactic: simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
refine_2 : toUnitHom χ = (ofUnitHom E).toUnitHom.comp (ZMod.unitsMap hd)
⊢ toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
have refine_2₁ : Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
  (MonoidHom.comp ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ) (ofUnitHom E)) (ZMod.unitsMap hd) :
    (ZMod n)ˣ →* Rˣ)
Tactic: simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
refine_2 : toUnitHom χ = (ofUnitHom E).toUnitHom.comp (ZMod.unitsMap hd)
refine_2₁ :
  Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
    (MonoidHom.comp ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ) (ofUnitHom E)) (ZMod.unitsMap hd) :
      (ZMod n)ˣ →* Rˣ)
⊢ toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
have refine_2₂ : Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
  (MonoidHom.comp
      ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ)
        ((Equiv.symm equivToUnitHom : (a : (ZMod d)ˣ →* Rˣ) → MulChar (ZMod d) R) E))
      (ZMod.unitsMap hd) :
    (ZMod n)ˣ →* Rˣ)
Tactic: simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
refine_2 : toUnitHom χ = (ofUnitHom E).toUnitHom.comp (ZMod.unitsMap hd)
refine_2₁ :
  Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
    (MonoidHom.comp ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ) (ofUnitHom E)) (ZMod.unitsMap hd) :
      (ZMod n)ˣ →* Rˣ)
refine_2₂ :
  Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
    (MonoidHom.comp
        ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ)
          ((Equiv.symm equivToUnitHom : (a : (ZMod d)ˣ →* Rˣ) → MulChar (ZMod d) R) E))
        (ZMod.unitsMap hd) :
      (ZMod n)ˣ →* Rˣ)
⊢ toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
have refine_2₃ : (equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ = E.comp (ZMod.unitsMap hd)
Tactic: simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]
-- 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
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ :=
  ((ZMod.unitsMap hd).liftOfSurjective ⋯ :
      (a : { g : (ZMod n)ˣ →* Rˣ // (ZMod.unitsMap hd).ker ≤ g.ker }) → (ZMod d)ˣ →* Rˣ)
    (Subtype.mk (p := fun (g : (ZMod n)ˣ →* Rˣ) ↦ (ZMod.unitsMap hd).ker ≤ g.ker) (toUnitHom χ) h)
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
refine_2 : toUnitHom χ = (ofUnitHom E).toUnitHom.comp (ZMod.unitsMap hd)
refine_2₁ :
  Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
    (MonoidHom.comp ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ) (ofUnitHom E)) (ZMod.unitsMap hd) :
      (ZMod n)ˣ →* Rˣ)
refine_2₂ :
  Eq (α := (ZMod n)ˣ →* Rˣ) ((equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ : (ZMod n)ˣ →* Rˣ)
    (MonoidHom.comp
        ((equivToUnitHom : (a : MulChar (ZMod d) R) → (ZMod d)ˣ →* Rˣ)
          ((Equiv.symm equivToUnitHom : (a : (ZMod d)ˣ →* Rˣ) → MulChar (ZMod d) R) E))
        (ZMod.unitsMap hd) :
      (ZMod n)ˣ →* Rˣ)
refine_2₃ : (equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ = E.comp (ZMod.unitsMap hd)
⊢ toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
have refine_2₄ : (equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ = toUnitHom χ
Tactic: simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst_1 : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
⊢ χ.FactorsThrough m
have refine : ∀ (x : (ZMod n)ˣ) (hx : x ∈ (ZMod.unitsMap hm).ker), x ∈ (toUnitHom χ).ker
Tactic: refine (factorsThrough_iff_ker_unitsMap hm).mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst_1 : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hm).ker
⊢ x ∈ (ZMod.unitsMap ⋯).ker
have hx₁ : Eq (α := (ZMod m)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x : (ZMod m)ˣ) (1 : (ZMod m)ˣ)
Tactic: rw [MonoidHom.mem_ker] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst_1 : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : Eq (α := (ZMod m)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x : (ZMod m)ˣ) (1 : (ZMod m)ˣ)
⊢ Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
have a : Eq (α := (ZMod d)ˣ) (((ZMod.unitsMap hd).comp (ZMod.unitsMap hm) : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ)
  (1 : (ZMod d)ˣ)
Tactic: rw [← ZMod.unitsMap_comp hd hm, MonoidHom.comp_apply, hx, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst_1 : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : Eq (α := (ZMod m)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x : (ZMod m)ˣ) (1 : (ZMod m)ˣ)
a :
  Eq (α := (ZMod d)ˣ) (((ZMod.unitsMap hd).comp (ZMod.unitsMap hm) : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ)
    (1 : (ZMod d)ˣ)
⊢ Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
have a₁ : Eq (α := (ZMod d)ˣ)
  ((ZMod.unitsMap hd : (a : (ZMod m)ˣ) → (ZMod d)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x) : (ZMod d)ˣ)
  (1 : (ZMod d)ˣ)
Tactic: rw [← ZMod.unitsMap_comp hd hm, MonoidHom.comp_apply, hx, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst_1 : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : Eq (α := (ZMod m)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x : (ZMod m)ˣ) (1 : (ZMod m)ˣ)
a :
  Eq (α := (ZMod d)ˣ) (((ZMod.unitsMap hd).comp (ZMod.unitsMap hm) : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ)
    (1 : (ZMod d)ˣ)
a₁ :
  Eq (α := (ZMod d)ˣ)
    ((ZMod.unitsMap hd : (a : (ZMod m)ˣ) → (ZMod d)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x) : (ZMod d)ˣ)
    (1 : (ZMod d)ˣ)
⊢ Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
have a₂ : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod m)ˣ) → (ZMod d)ˣ) 1) 1
Tactic: rw [← ZMod.unitsMap_comp hd hm, MonoidHom.comp_apply, hx, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst_1 : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
x : (ZMod n)ˣ
hx : Eq (α := (ZMod m)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x : (ZMod m)ˣ) (1 : (ZMod m)ˣ)
a :
  Eq (α := (ZMod d)ˣ) (((ZMod.unitsMap hd).comp (ZMod.unitsMap hm) : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ)
    (1 : (ZMod d)ˣ)
a₁ :
  Eq (α := (ZMod d)ˣ)
    ((ZMod.unitsMap hd : (a : (ZMod m)ˣ) → (ZMod d)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x) : (ZMod d)ˣ)
    (1 : (ZMod d)ˣ)
a₂ : Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap hd : (a : (ZMod m)ˣ) → (ZMod d)ˣ) 1) 1
⊢ Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) (1 : (ZMod d)ˣ)
have a₃ : Eq (α := (ZMod d)ˣ) 1 1
Tactic: rw [← ZMod.unitsMap_comp hd hm, MonoidHom.comp_apply, hx, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst_1 : NeZero n
ψ : DirichletCharacter R m
h :
  Eq (α := DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m))
⊢ χ.FactorsThrough (n.gcd m)
have refine : ∀ (x : (ZMod n)ˣ) (hx : x ∈ (ZMod.unitsMap sorry).ker), Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
Tactic: refine (factorsThrough_iff_ker_unitsMap (n.gcd_dvd_left m)).mpr fun x hx ↦
    MonoidHom.mem_ker.mpr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst_1 : NeZero n
ψ : DirichletCharacter R m
h :
  Eq (α := DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m))
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
⊢ Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
have rw : Eq (α := R) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
Tactic: rw [Units.ext_iff, MulChar.coe_toUnitHom, Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst_1 : NeZero n
ψ : DirichletCharacter R m
h :
  Eq (α := DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m))
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1
have obtain : ∀ (z : ℕ) (hz₁ : z ≡ (↑x : ZMod n).val [MOD n]) (hz₂ : z ≡ 1 [MOD m]),
  ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1
Tactic: obtain ⟨z, hz₁, hz₂⟩ := Nat.chineseRemainder' this
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst_1 : NeZero n
ψ : DirichletCharacter R m
h :
  Eq (α := DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m))
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x : ZMod n).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1
have refine_1 : (↑z : ZMod n) = (↑x : ZMod n)
Tactic: refine ⟨z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst_1 : NeZero n
ψ : DirichletCharacter R m
h :
  Eq (α := DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m))
    ((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m))
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x : ZMod n).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
refine_1 : (↑z : ZMod n) = (↑x : ZMod n)
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1
have refine_2 : Eq (α := ZMod m) (↑z : ZMod m) 1
Tactic: refine ⟨z, ?_, ?_⟩