awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n_1 : ℕ
χ : DirichletCharacter R n_1
n m : ℕ
hm : n ∣ m
a : (ZMod m)ˣ
⊢ Eq.{u_1 + 1} (α := R)
    ((ofUnitHom (MonoidHom.comp (toUnitHom 1) (ZMod.unitsMap hm)) : (a : ZMod m) → R) (↑a : ZMod m) : R)
    ((1 : (a : ZMod m) → R) (↑a : ZMod m) : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n_1 : ℕ
χ : DirichletCharacter R n_1
n m : ℕ
hm : n ∣ m
ψ₁ ψ₂ : DirichletCharacter R n
h :
  ∀ (a : (ZMod m)ˣ),
    Eq (α := R) ((ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm)) : (a : ZMod m) → R) (↑a : ZMod m) : R)
      ((ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm)) :
            (a : ZMod m) → R)
          (↑a : ZMod m) :
        R)
⊢ ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm)) =
    ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm))

Tactic:
ext
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n_1 : ℕ
χ : DirichletCharacter R n_1
n m : ℕ
hm : n ∣ m
ψ₁ ψ₂ : DirichletCharacter R n
a : (ZMod m)ˣ
⊢ Eq (α := R) ((ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm)) : (a : ZMod m) → R) (↑a : ZMod m) : R)
    ((ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm)) :
          (a : ZMod m) → R)
        (↑a : ZMod m) :
      R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
⊢ (changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) χ =
    ofUnitHom ((toUnitHom χ).comp (ZMod.unitsMap hm))

Tactic:
rfl

Premises used: MulChar.ofUnitHom, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
⊢ toUnitHom ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) χ) =
    (toUnitHom χ).comp (ZMod.unitsMap hm)

Tactic:
simp [changeLevel]

Premises used: DirichletCharacter.changeLevel
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ : DirichletCharacter R n
_ :
  ∀ ⦃a₂ : DirichletCharacter R n⦄,
    Eq (α := DirichletCharacter R m)
        ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
        ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : DirichletCharacter R n⦄,
    Eq (α := DirichletCharacter R m)
        ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
        ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  Eq (α := DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m)
h₁ :
  ∀ (y : (ZMod n)ˣ), Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑y : ZMod n) : R) ((a₂ : (a : ZMod n) → R) (↑y : ZMod n) : R)
⊢ a₁ = a₂

Tactic:
ext1 y
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  Eq (α := DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m)
y : (ZMod n)ˣ
h₁ :
  ∀ (z : (ZMod m)ˣ),
    Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
      ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
⊢ Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑y : ZMod n) : R) ((a₂ : (a : ZMod n) → R) (↑y : ZMod n) : R)

Tactic:
obtain ⟨z, rfl⟩ := ZMod.unitsMap_surjective hm y

Premises used: ZMod.unitsMap_surjective, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  Eq (α := DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m)
z : (ZMod m)ˣ
h₁ :
  ∀
    (h :
      ∀ (a : (ZMod m)ˣ),
        Eq (α := R)
          ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m) :
                (a : ZMod m) → R)
              (↑a : ZMod m) :
            R)
          ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m) :
                (a : ZMod m) → R)
              (↑a : ZMod m) :
            R))
    (z : (ZMod m)ˣ),
    Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
      ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
⊢ Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
    ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)

Tactic:
rw [MulChar.ext_iff] at h

Premises used: MulChar.ext_iff
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  ∀ (a : (ZMod m)ˣ),
    Eq (α := R)
      ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m) :
            (a : ZMod m) → R)
          (↑a : ZMod m) :
        R)
      ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m) :
            (a : ZMod m) → R)
          (↑a : ZMod m) :
        R)
z : (ZMod m)ˣ
⊢ Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
    ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)

Tactic:
simpa [changeLevel_def] using h z

Premises used: DirichletCharacter.changeLevel_def
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
χ : DirichletCharacter R n
hm : n ∣ m
⊢ Eq (α := DirichletCharacter R m)
      ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) χ : DirichletCharacter R m)
      (1 : DirichletCharacter R m) ↔
    χ = 1

Tactic:
map_eq_one_iff _ (changeLevel_injective hm)

Premises used: DirichletCharacter.changeLevel_injective, map_eq_one_iff
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R n) χ = χ

Tactic:
simp [changeLevel, ZMod.unitsMap]

Premises used: ZMod.unitsMap, DirichletCharacter.changeLevel
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
rw rw₁ : toUnitHom χ = toUnitHom χ
⊢ toUnitHom ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R n) χ) = toUnitHom χ

Tactic:
rw [changeLevel_self]

Premises used: DirichletCharacter.changeLevel_self
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ Eq (α := DirichletCharacter R d)
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R d) χ : DirichletCharacter R d)
    ((changeLevel hd : (a : DirichletCharacter R m) → DirichletCharacter R d)
        ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) χ) :
      DirichletCharacter R d)

Tactic:
simp [changeLevel_def, MonoidHom.comp_assoc, ZMod.unitsMap_comp]

Premises used: DirichletCharacter.changeLevel_def, ZMod.unitsMap_comp, MonoidHom.comp_assoc
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : (ZMod m)ˣ
⊢ Eq (α := R)
    ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) χ : DirichletCharacter R m) :
          (a : ZMod m) → R)
        (↑a : ZMod m) :
      R)
    ((χ : (a : ZMod n) → R) (↑a : ZMod m).cast : R)

Tactic:
simp [changeLevel_def, ZMod.unitsMap_val]

Premises used: DirichletCharacter.changeLevel_def, ZMod.unitsMap_val
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
⊢ FactorsThrough.{u_1} (R := R) (n := m) ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) χ) n

Tactic:
⟨hm, χ, rfl⟩

Premises used: DirichletCharacter.FactorsThrough, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
h : χ.FactorsThrough d
⊢ d ∣ n

Tactic:
h.1
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
h : χ.FactorsThrough d
⊢ χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) h.χ₀

Tactic:
Classical.choose_spec h.2

Premises used: DirichletCharacter.FactorsThrough.χ₀, Classical.choose_spec
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
h : χ.FactorsThrough d
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 ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) χ' : DirichletCharacter R n)
⊢ ∃! χ' : DirichletCharacter R d, χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) χ'

Tactic:
rcases h with ⟨hd, χ₂, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n d : ℕ
inst_1 : NeZero n
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 ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) χ' : DirichletCharacter R n)

Tactic:
⟨χ₂, rfl, fun χ₃ hχ₃ ↦ (changeLevel_injective hd hχ₃).symm⟩

Premises used: DirichletCharacter.changeLevel_injective, ExistsUnique, And.intro, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n d : ℕ
inst_1 : NeZero n
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 ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) χ' : DirichletCharacter R n)

Tactic:
exact ⟨χ₂, rfl, fun χ₃ hχ₃ ↦ (changeLevel_injective hd hχ₃).symm⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.FactorsThrough n

Tactic:
⟨dvd_refl n, χ, (changeLevel_self χ).symm⟩

Premises used: DirichletCharacter.FactorsThrough, Exists.intro, Eq.symm, dvd_refl, DirichletCharacter.changeLevel_self
-- 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
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker

Tactic:
⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩

Premises used: Membership.mem, MonoidHom.ker, MulChar.toUnitHom, Iff.intro, _private.0.DirichletCharacter.factorsThrough_iff_ker_unitsMap.match_1
-- 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
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
refine_2 : ∀ (h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker), χ.FactorsThrough d
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker

Tactic:
refine ⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩
-- 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
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ˣ)
refine_1₅ refine_1₆ : Eq.{u_1 + 1} (α := Rˣ) 1 1
⊢ x ∈ (toUnitHom χ).ker

Tactic:
rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]

Premises used: DirichletCharacter.changeLevel_toUnitHom, MonoidHom.mem_ker, map_one, MonoidHom.comp_apply
-- 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
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)
⊢ E.comp (ZMod.unitsMap hd) = toUnitHom χ

Tactic:
have hE : E.comp (ZMod.unitsMap hd) = χ.toUnitHom := MonoidHom.liftOfRightInverse_comp ..
-- 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
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

Tactic:
⟨hd, MulChar.ofUnitHom E, equivToUnitHom.injective (?_ : toUnitHom _ = toUnitHom _)⟩

Premises used: DirichletCharacter.FactorsThrough, MulChar.equivToUnitHom, Exists.intro, Equiv.injective, MulChar.ofUnitHom
-- 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
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 χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))
⊢ χ.FactorsThrough d

Tactic:
refine ⟨hd, MulChar.ofUnitHom E, equivToUnitHom.injective (?_ : toUnitHom _ = toUnitHom _)⟩
-- 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
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)
refine_2₄ : (equivToUnitHom : (a : MulChar (ZMod n) R) → (ZMod n)ˣ →* Rˣ) χ = toUnitHom χ
⊢ toUnitHom χ = toUnitHom ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) (ofUnitHom E))

Tactic:
simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]

Premises used: MulChar.toUnitHom_eq, Equiv.apply_symm_apply, DirichletCharacter.changeLevel_toUnitHom, MulChar.ofUnitHom_eq
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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

Tactic:
(factorsThrough_iff_ker_unitsMap hm).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, DirichletCharacter.factorsThrough_iff_ker_unitsMap
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
refine : ∀ (x : (ZMod n)ˣ) (hx : x ∈ (ZMod.unitsMap hm).ker), x ∈ (toUnitHom χ).ker
⊢ χ.FactorsThrough m

Tactic:
refine (factorsThrough_iff_ker_unitsMap hm).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, DirichletCharacter.factorsThrough_iff_ker_unitsMap
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
⊢ Eq (α := (ZMod m)ˣ) ((ZMod.unitsMap hm : (a : (ZMod n)ˣ) → (ZMod m)ˣ) x : (ZMod m)ˣ) (1 : (ZMod m)ˣ)

Tactic:
rw [MonoidHom.mem_ker] at hx ⊢

Premises used: MonoidHom.mem_ker
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
a₃ a₄ : Eq (α := (ZMod d)ˣ) 1 1
⊢ Eq (α := (ZMod d)ˣ) ((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod d)ˣ) x : (ZMod d)ˣ) (1 : (ZMod d)ˣ)

Tactic:
rw [← ZMod.unitsMap_comp hd hm, MonoidHom.comp_apply, hx, map_one]

Premises used: ZMod.unitsMap_comp, map_one, MonoidHom.comp_apply
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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)

Tactic:
(factorsThrough_iff_ker_unitsMap (n.gcd_dvd_left m)).mpr fun x hx ↦
    MonoidHom.mem_ker.mpr ?_

Premises used: Iff.mpr, Nat.gcd_dvd_left, MonoidHom.mem_ker, DirichletCharacter.factorsThrough_iff_ker_unitsMap
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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))
refine :
  ∀ (x : (ZMod n)ˣ) (hx : x ∈ (ZMod.unitsMap ⋯).ker),
    Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)
⊢ χ.FactorsThrough (n.gcd m)

Tactic:
refine (factorsThrough_iff_ker_unitsMap (n.gcd_dvd_left m)).mpr fun x hx ↦
    MonoidHom.mem_ker.mpr ?_

Premises used: Iff.mpr, Nat.gcd_dvd_left, MonoidHom.mem_ker, DirichletCharacter.factorsThrough_iff_ker_unitsMap
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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
rw : Eq (α := R) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
⊢ Eq (α := Rˣ) ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) x : Rˣ) (1 : Rˣ)

Tactic:
rw [Units.ext_iff, MulChar.coe_toUnitHom, Units.val_one]

Premises used: Units.ext_iff, Units.val_one, MulChar.coe_toUnitHom
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
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]
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
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := Nat.chineseRemainder' this

Premises used: Nat.chineseRemainder'