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
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]
⊢ Eq (α := ZMod m) (↑z : ZMod m) 1
have refine_2 : ∀ (hz₂ : Eq (α := ZMod m) (↑z : ZMod m) (↑1 : ZMod m)), Eq (α := ZMod m) (↑z : ZMod m) 1
Tactic: rwa [← ZMod.natCast_eq_natCast_iff, Nat.cast_one] at hz₂
Cleared hypotheses: hz₂
-- 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_2 : ∀ (hz₂ : Eq (α := ZMod m) (↑z : ZMod m) (↑1 : ZMod m)), Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ Eq (α := ZMod m) (↑z : ZMod m) 1
have refine_2₁ : ∀ (hz₂ : 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₂
Cleared hypotheses: hz₂
-- 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
⊢ ∃ (z : ℕ), (↑z : ZMod n) = (↑x : ZMod n) ∧ Eq (α := ZMod m) (↑z : ZMod m) 1
have suffices : (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
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₂
-- 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
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have rwa : ∀
  (hx :
    Eq (α := (ZMod (n.gcd m))ˣ) ((ZMod.unitsMap sorry : (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]
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
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
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]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have rwa₁ : ∀
  (hx :
    Eq (α := ZMod (n.gcd m)) (↑((ZMod.unitsMap sorry : (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]
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
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
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]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have 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]
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
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
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]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have 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]
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
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
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]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have 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]
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
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
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]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have 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]
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
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
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]
⊢ (↑x : ZMod n).val ≡ 1 [MOD n.gcd m]
have rwa₆ : ∀ (hx : (↑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
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
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) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
have 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)
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
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
⊢ z.gcd (n * m) = 1
have refine_1 : z.Coprime n
Tactic: refine Nat.Coprime.mul_right ?_ ?_
-- 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
z : ℕ
hz₁ : (↑z : ZMod n) = (↑x : ZMod n)
hz₂ : Eq (α := ZMod m) (↑z : ZMod m) 1
refine_1 : z.Coprime n
⊢ z.gcd (n * m) = 1
have refine_2 : z.Coprime m
Tactic: refine Nat.Coprime.mul_right ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
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
⊢ Eq (α := R) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
have hz₀ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
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) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
have this : Eq (α := R)
  ((((changeLevel sorry : (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₀)
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
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) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
have this₁ : Eq (α := R)
  ((((changeLevel sorry : (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
Cleared hypotheses: 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
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) ((χ : (a : ZMod n) → R) (↑x : ZMod n) : R) (1 : R)
have rw : Eq (α := R)
  ((((changeLevel sorry : (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 [← hz₁, ← this, h]
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
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)
        (↑z : ZMod (n * m)) :
      R)
    (1 : R)
have this₁ : Eq (α := R)
  ((((changeLevel sorry : (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₀)
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (hypothesis)
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)
    (1 : R)
have this₁ : Eq (α := R)
  ((((changeLevel sorry : (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
Cleared hypotheses: this