awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
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:
⟨z, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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]
z : ℕ
hz₁ : z ≡ (↑x : ZMod n).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
refine_1 : (↑z : ZMod n) = (↑x : ZMod n)
refine_2 : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1

Tactic:
refine ⟨z, ?_, ?_⟩
-- 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]
z : ℕ
hz₁ : z ≡ (↑x : ZMod n).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ (↑z : ZMod n) = (↑x : ZMod n)

Tactic:
simpa [← ZMod.natCast_eq_natCast_iff] using hz₁

Premises used: ZMod.natCast_eq_natCast_iff
-- 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]
z : ℕ
hz₁ : z ≡ (↑x : ZMod n).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
refine_2 : ∀ (hz₂ : Eq (α := ZMod m) (↑z : ZMod m) (↑1 : ZMod m)), Eq (α := ZMod m) (↑z : ZMod m) 1
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1), Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ Eq (α := ZMod m) (↑z : ZMod m) 1

Tactic:
rwa [← ZMod.natCast_eq_natCast_iff, Nat.cast_one] at hz₂

Premises used: ZMod.natCast_eq_natCast_iff, Nat.cast_one
-- 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
suffices : (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1

Tactic:
suffices x.val.val ≡ 1 [MOD n.gcd m] by
      obtain ⟨z, hz₁, hz₂⟩ := Nat.chineseRemainder' this
      refine ⟨z, ?_, ?_⟩
      · simpa [← ZMod.natCast_eq_natCast_iff] using hz₁
      · rwa [← ZMod.natCast_eq_natCast_iff, Nat.cast_one] at hz₂
-- 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
rwa :
  ∀
    (hx :
      Eq (α := (ZMod (n.gcd m))ˣ) ((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod (n.gcd m))ˣ) x : (ZMod (n.gcd m))ˣ)
        (1 : (ZMod (n.gcd m))ˣ)),
    (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
rwa₁ :
  ∀
    (hx :
      Eq (α := ZMod (n.gcd m)) (↑((ZMod.unitsMap ⋯ : (a : (ZMod n)ˣ) → (ZMod (n.gcd m))ˣ) x) : ZMod (n.gcd m))
        (↑1 : ZMod (n.gcd m))),
    (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
rwa₂ : ∀ (hx : Eq (α := ZMod (n.gcd m)) (↑x : ZMod n).cast (↑1 : ZMod (n.gcd m))), (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
rwa₃ :
  ∀ (hx : Eq (α := ZMod (n.gcd m)) (↑(↑x : ZMod n).val : ZMod (n.gcd m)) (↑1 : ZMod (n.gcd m))),
    (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
rwa₄ : ∀ (hx : Eq (α := ZMod (n.gcd m)) (↑(↑x : ZMod n).val : ZMod (n.gcd m)) 1), (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
rwa₅ :
  ∀ (hx : Eq (α := ZMod (n.gcd m)) (↑(↑x : ZMod n).val : ZMod (n.gcd m)) (↑1 : ZMod (n.gcd m))),
    (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (hx : (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]), (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]

Tactic:
rwa [MonoidHom.mem_ker, Units.ext_iff, ZMod.unitsMap_val, ← ZMod.natCast_val,
      Units.val_one, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff] at hx

Premises used: Units.ext_iff, MonoidHom.mem_ker, ZMod.natCast_val, ZMod.unitsMap_val, Units.val_one, ZMod.natCast_eq_natCast_iff, Nat.cast_one
-- 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
obtain :
  ∀ (z : ℕ) (hz₁ : (↑z : ZMod n) = (↑x : ZMod n)) (hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1),
    Eq (α := R) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
⊢ Eq (α := R) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)

Tactic:
obtain ⟨z, hz₁, hz₂⟩ : ∃ z : ℕ, z = x.val ∧ (z : ZMod m) = 1 := by
    suffices x.val.val ≡ 1 [MOD n.gcd m] by
      obtain ⟨z, hz₁, hz₂⟩ := Nat.chineseRemainder' this
      refine ⟨z, ?_, ?_⟩
      · simpa [← ZMod.natCast_eq_natCast_iff] using hz₁
      · rwa [← ZMod.natCast_eq_natCast_iff, Nat.cast_one] at hz₂
    rwa [MonoidHom.mem_ker, Units.ext_iff, ZMod.unitsMap_val, ← ZMod.natCast_val,
      Units.val_one, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff] at hx

Premises used: Units.val
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.gcd (n * m) = 1

Tactic:
Nat.Coprime.mul_right ?_ ?_

Premises used: Nat.Coprime.mul_right
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
refine_1 : z.Coprime n
refine_2 : z.Coprime m
⊢ z.gcd (n * m) = 1

Tactic:
refine Nat.Coprime.mul_right ?_ ?_

Premises used: Nat.Coprime.mul_right
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.Coprime n

Tactic:
(ZMod.isUnit_iff_coprime _ _).mp <| hz₁ ▸ x.isUnit

Premises used: ZMod.isUnit_iff_coprime, Eq.rec, Iff.mp, Units.isUnit, Eq.symm
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.Coprime n

Tactic:
exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₁ ▸ x.isUnit

Premises used: ZMod.isUnit_iff_coprime, Iff.mp
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.Coprime m

Tactic:
(ZMod.isUnit_iff_coprime _ _).mp <| hz₂ ▸ isUnit_one

Premises used: ZMod.isUnit_iff_coprime, Eq.rec, isUnit_one, Iff.mp, Eq.symm
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.Coprime m

Tactic:
exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₂ ▸ isUnit_one

Premises used: ZMod.isUnit_iff_coprime, Iff.mp
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.gcd (n * m) = 1

Tactic:
have hz₀ : z.gcd (n * m) = 1 := by
    refine Nat.Coprime.mul_right ?_ ?_
    · exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₁ ▸ x.isUnit
    · exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₂ ▸ isUnit_one
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
hz₀ : z.gcd (n * m) = 1
⊢ Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)).cast : R)

Tactic:
have := changeLevel_eq_cast_of_dvd χ (n.dvd_mul_right m) (ZMod.unitOfCoprime z hz₀)
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
hz₀ : z.gcd (n * m) = 1
this :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)).cast : R)
⊢ Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑z : ZMod n) : R)

Tactic:
simp only [ZMod.coe_unitOfCoprime, dvd_mul_right, ZMod.cast_natCast] at this

Premises used: ZMod.cast_natCast, dvd_mul_right, ZMod.coe_unitOfCoprime
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
hz₀ : z.gcd (n * m) = 1
this :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑z : ZMod n) : R)
rw :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    (1 : R)
⊢ Eq (α := R) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)

Tactic:
rw [← hz₁, ← this, h]
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
hz₀ : z.gcd (n * m) = 1
this :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑z : ZMod n) : R)
⊢ Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)) :
      R)
    ((ψ : (a : ZMod m) → R) (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)).cast : R)

Tactic:
have := changeLevel_eq_cast_of_dvd ψ (m.dvd_mul_left n) (ZMod.unitOfCoprime z hz₀)
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
hz₀ : z.gcd (n * m) = 1
this_1 :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑z : ZMod n) : R)
this :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)) :
      R)
    ((ψ : (a : ZMod m) → R) (↑(ZMod.unitOfCoprime z hz₀) : ZMod (n * m)).cast : R)
⊢ Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((ψ : (a : ZMod m) → R) (↑z : ZMod m) : R)

Tactic:
simp only [ZMod.coe_unitOfCoprime, dvd_mul_left, ZMod.cast_natCast] at this

Premises used: ZMod.cast_natCast, dvd_mul_left, ZMod.coe_unitOfCoprime
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
hz₀ : z.gcd (n * m) = 1
this_1 :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (n * m)) χ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((χ : (a : ZMod n) → R) (↑z : ZMod n) : R)
this :
  Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    ((ψ : (a : ZMod m) → R) (↑z : ZMod m) : R)
rw : Eq (α := R) ((ψ : (a : ZMod m) → R) (↑z : ZMod m) : R) (1 : R)
rw₁ : Eq (α := R) ((ψ : (a : ZMod m) → R) 1 : R) (1 : R)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq (α := R)
    ((((changeLevel ⋯ : (a : DirichletCharacter R m) → DirichletCharacter R (n * m)) ψ : DirichletCharacter R (n * m)) :
          (a : ZMod (n * m)) → R)
        (↑z : ZMod (n * m)) :
      R)
    (1 : R)

Tactic:
rw [this, hz₂, map_one]

Premises used: map_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
h : ∀ (a : (ZMod 1)ˣ), Eq (α := R) ((χ : (a : ZMod 1) → R) (↑a : ZMod 1) : R) ((1 : (a : ZMod 1) → R) (↑a : ZMod 1) : R)
⊢ χ = 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
a : (ZMod 1)ˣ
⊢ Eq (α := R) ((χ : (a : ZMod 1) → R) (↑a : ZMod 1) : R) ((1 : (a : ZMod 1) → R) (↑a : ZMod 1) : R)

Tactic:
simp [Units.eq_one]

Premises used: Units.eq_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n = 1
subst : ∀ (χ : DirichletCharacter R 1), χ = 1
⊢ χ = 1

Tactic:
subst hn
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ χ = 1

Tactic:
level_one _

Premises used: DirichletCharacter.level_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ χ = 1

Tactic:
exact level_one _

Premises used: DirichletCharacter.level_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ Subsingleton.{u_1 + 1} (DirichletCharacter R 1)

Tactic:
subsingleton_iff.mpr (fun χ χ' ↦ ?_)

Premises used: Iff.mpr, subsingleton_iff
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
refine : ∀ (χ χ' : DirichletCharacter R 1), χ = χ'
⊢ Subsingleton.{u_1 + 1} (DirichletCharacter R 1)

Tactic:
refine subsingleton_iff.mpr (fun χ χ' ↦ ?_)

Premises used: Iff.mpr, subsingleton_iff
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ_1 : DirichletCharacter R n
χ χ' : DirichletCharacter R 1
⊢ χ = χ'

Tactic:
simp [level_one]

Premises used: DirichletCharacter.level_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n ≠ 1
⊢ Eq (α := R) ((χ : (a : ZMod n) → R) 0 : R) (0 : R)

Tactic:
have := ZMod.nontrivial_iff.mpr hn; χ.map_zero

Premises used: Iff.mpr, ZMod.nontrivial_iff, MulChar.map_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n d : ℕ
h : d ∣ n
⊢ Eq.{u_1 + 1} (α := DirichletCharacter R n) ((changeLevel h : (a : DirichletCharacter R d) → DirichletCharacter R n) 1)
    1

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ = 1
rw :
  Eq.{u_1 + 1} (α := DirichletCharacter R n) 1
    ((changeLevel ⋯ : (a : DirichletCharacter R 1) → DirichletCharacter R n) 1)
rw₁ rw₂ : Eq.{u_1 + 1} (α := DirichletCharacter R n) 1 1
⊢ χ = (changeLevel ⋯ : (a : DirichletCharacter R 1) → DirichletCharacter R n) 1

Tactic:
rw [h, changeLevel_one]

Premises used: DirichletCharacter.changeLevel_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
refine :
  χ.FactorsThrough 1 →
    ∀ (w : 1 ∣ n) (χ₀ : DirichletCharacter R 1)
      (hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R 1) → DirichletCharacter R n) χ₀), χ = 1
⊢ χ.FactorsThrough 1 ↔ χ = 1

Tactic:
refine ⟨fun ⟨_, χ₀, hχ₀⟩ ↦ ?_,
          fun h ↦ ⟨one_dvd n, 1, by rw [h, changeLevel_one]⟩⟩