awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.FactorsThrough 1
w : 1 ∣ n
χ₀ : DirichletCharacter R 1
hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R 1) → DirichletCharacter R n) χ₀
rwa : ∀ (hχ₀ : χ = (changeLevel w : (a : DirichletCharacter R 1) → DirichletCharacter R n) 1), χ = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hχ₀ : χ = 1), χ = 1
⊢ χ = 1

Tactic:
rwa [level_one χ₀, changeLevel_one] at hχ₀

Premises used: DirichletCharacter.changeLevel_one, DirichletCharacter.level_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x : ℕ
⊢ x ∈ χ.conductorSet ↔ χ.FactorsThrough x

Tactic:
Iff.refl _

Premises used: DirichletCharacter.FactorsThrough, Set.Mem, Iff.refl, setOf, DirichletCharacter.conductorSet
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n ∈ χ.conductorSet

Tactic:
FactorsThrough.same_level χ

Premises used: DirichletCharacter.FactorsThrough, DirichletCharacter.FactorsThrough.same_level, Set.Mem, setOf, DirichletCharacter.conductorSet
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x : ℕ
hx : x ∈ χ.conductorSet
⊢ x ∣ n

Tactic:
hx.dvd

Premises used: DirichletCharacter.FactorsThrough.dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
⊢ 0 ∉ χ.conductorSet

Tactic:
fun h ↦ NeZero.ne n <| Nat.eq_zero_of_zero_dvd <| FactorsThrough.dvd h

Premises used: DirichletCharacter.FactorsThrough.dvd, Not, NeZero.ne, Nat.eq_zero_of_zero_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor ∈ χ.conductorSet

Tactic:
Nat.sInf_mem (Set.nonempty_of_mem (level_mem_conductorSet χ))

Premises used: DirichletCharacter.conductor, Set.Mem, Nat.sInf_mem, DirichletCharacter.level_mem_conductorSet, Set.nonempty_of_mem
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor ∣ n

Tactic:
(conductor_mem_conductorSet χ).dvd

Premises used: DirichletCharacter.conductor_mem_conductorSet, DirichletCharacter.FactorsThrough.dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.FactorsThrough χ.conductor

Tactic:
conductor_mem_conductorSet χ

Premises used: DirichletCharacter.FactorsThrough, Set.Mem, setOf, DirichletCharacter.conductor_mem_conductorSet, DirichletCharacter.conductorSet
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
⊢ χ.conductor ≠ 0

Tactic:
fun h ↦ NeZero.ne n <| Nat.eq_zero_of_zero_dvd <| h ▸ conductor_dvd_level _

Premises used: DirichletCharacter.conductor_dvd_level, Eq.rec, Not, NeZero.ne, Nat.eq_zero_of_zero_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
this : FactorsThrough.{u_1} (R := R) (n := n) 1 1
⊢ conductor.{u_1} (R := R) (n := n) 1 ≤ 1

Tactic:
have h : conductor (1 : DirichletCharacter R n) ≤ 1 :=
      Nat.sInf_le <| (mem_conductorSet_iff _).mpr this
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
this : FactorsThrough.{u_1} (R := R) (n := n) 1 1
h : conductor.{u_1} (R := R) (n := n) 1 ≤ 1
⊢ conductor.{u_1} (R := R) (n := n) 1 = 1

Tactic:
Nat.le_antisymm h (Nat.pos_of_ne_zero <| conductor_ne_zero _)

Premises used: Nat.pos_of_ne_zero, Nat.le_antisymm, DirichletCharacter.conductor_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
this : FactorsThrough.{u_1} (R := R) (n := n) 1 1
h : conductor.{u_1} (R := R) (n := n) 1 ≤ 1
⊢ conductor.{u_1} (R := R) (n := n) 1 = 1

Tactic:
exact Nat.le_antisymm h (Nat.pos_of_ne_zero <| conductor_ne_zero _)

Premises used: Nat.pos_of_ne_zero, Nat.le_antisymm, DirichletCharacter.conductor_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
suffices : FactorsThrough.{u_1} (R := R) (n := n) 1 1
⊢ conductor.{u_1} (R := R) (n := n) 1 = 1

Tactic:
suffices FactorsThrough (1 : DirichletCharacter R n) 1 by
    have h : conductor (1 : DirichletCharacter R n) ≤ 1 :=
      Nat.sInf_le <| (mem_conductorSet_iff _).mpr this
    exact Nat.le_antisymm h (Nat.pos_of_ne_zero <| conductor_ne_zero _)
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
⊢ FactorsThrough.{u_1} (R := R) (n := n) 1 1

Tactic:
(factorsThrough_one_iff _).mpr rfl

Premises used: Iff.mpr, DirichletCharacter.factorsThrough_one_iff, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
⊢ FactorsThrough.{u_1} (R := R) (n := n) 1 1

Tactic:
exact (factorsThrough_one_iff _).mpr rfl

Premises used: Iff.mpr, DirichletCharacter.factorsThrough_one_iff, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
⊢ χ = 1 ↔ χ.conductor = 1

Tactic:
⟨fun h ↦ h ▸ conductor_one, fun hχ ↦ ?_⟩

Premises used: DirichletCharacter.conductor_one, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
refine : ∀ (hχ : χ.conductor = 1), χ = 1
⊢ χ = 1 ↔ χ.conductor = 1

Tactic:
refine ⟨fun h ↦ h ▸ conductor_one, fun hχ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
hχ : χ.conductor = 1
obtain :
  ∀ (h' : χ.conductor ∣ n) (χ₀ : DirichletCharacter R χ.conductor)
    (h : χ = (changeLevel h' : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ₀), χ = 1
⊢ χ = 1

Tactic:
obtain ⟨h', χ₀, h⟩ := factorsThrough_conductor χ

Premises used: DirichletCharacter.factorsThrough_conductor
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst_1 : NeZero n
hχ : χ.conductor = 1
h' : χ.conductor ∣ n
χ₀ : DirichletCharacter R χ.conductor
h : χ = (changeLevel h' : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ₀
⊢ χ = 1

Tactic:
exact (level_one' χ₀ hχ ▸ h).trans <| changeLevel_one h'

Premises used: DirichletCharacter.changeLevel_one
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor = 0 ↔ n = 0

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
refine_1 : χ.conductor = 0 → n = 0
refine_2 : n = 0 → χ.conductor = 0
⊢ χ.conductor = 0 ↔ n = 0

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
refine_1 : n ≠ 0 → χ.conductor ≠ 0
⊢ χ.conductor = 0 → n = 0

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n ≠ 0 → χ.conductor ≠ 0

Tactic:
fun h ↦ @conductor_ne_zero _ _ _ χ ⟨h⟩

Premises used: DirichletCharacter.conductor_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n ≠ 0 → χ.conductor ≠ 0

Tactic:
exact fun h ↦ @conductor_ne_zero _ _ _ χ ⟨h⟩

Premises used: DirichletCharacter.conductor_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 0
⊢ χ.conductor = 0

Tactic:
Nat.sInf_eq_zero.mpr <| Or.inl <| level_mem_conductorSet χ

Premises used: Iff.mpr, DirichletCharacter.conductor, Nat.sInf_eq_zero, DirichletCharacter.level_mem_conductorSet, Or.inl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 0
⊢ χ.conductor = 0

Tactic:
exact Nat.sInf_eq_zero.mpr <| Or.inl <| level_mem_conductorSet χ

Premises used: Iff.mpr, Nat.sInf_eq_zero, DirichletCharacter.level_mem_conductorSet, Or.inl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ.conductor ≤
    conductor.{u_1} (R := R) (n := d)
      (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
        χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯)

Tactic:
Nat.sInf_le <| (mem_conductorSet_iff χ).mpr <|
    ⟨dvd_trans (conductor_dvd_level _) hd.1,
     (factorsThrough_conductor (Classical.choose hd.2)).2.choose, ?_⟩

Premises used: Iff.mpr, DirichletCharacter.conductor, DirichletCharacter.conductor_dvd_level, dvd_trans, DirichletCharacter.mem_conductorSet_iff, Nat.sInf_le, Exists.intro, Classical.choose, Exists.choose, DirichletCharacter.factorsThrough_conductor
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
refine :
  χ =
    (changeLevel ⋯ : (a : DirichletCharacter R (Classical.choose ⋯).conductor) → DirichletCharacter R n)
      (Exists.choose (p :=
        fun
          (χ₀ :
            DirichletCharacter R
              (conductor.{u_1} (R := R) (n := d)
                (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
                  χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯))) ↦
        Eq (α := DirichletCharacter R d)
          (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
              χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯ :
            DirichletCharacter R d)
          ((changeLevel ⋯ : (a : DirichletCharacter R (Classical.choose ⋯).conductor) → DirichletCharacter R d) χ₀ :
            DirichletCharacter R d))
        ⋯)
⊢ χ.conductor ≤
    conductor.{u_1} (R := R) (n := d)
      (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
        χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯)

Tactic:
refine Nat.sInf_le <| (mem_conductorSet_iff χ).mpr <|
    ⟨dvd_trans (conductor_dvd_level _) hd.1,
     (factorsThrough_conductor (Classical.choose hd.2)).2.choose, ?_⟩

Premises used: Iff.mpr, DirichletCharacter.mem_conductorSet_iff, Nat.sInf_le
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
rw :
  χ =
    (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n)
      (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
        χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯)
⊢ χ =
    (changeLevel ⋯ : (a : DirichletCharacter R (Classical.choose ⋯).conductor) → DirichletCharacter R n)
      (Exists.choose (p :=
        fun
          (χ₀ :
            DirichletCharacter R
              (conductor.{u_1} (R := R) (n := d)
                (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
                  χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯))) ↦
        Eq (α := DirichletCharacter R d)
          (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
              χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯ :
            DirichletCharacter R d)
          ((changeLevel ⋯ : (a : DirichletCharacter R (Classical.choose ⋯).conductor) → DirichletCharacter R d) χ₀ :
            DirichletCharacter R d))
        ⋯)

Tactic:
rw [changeLevel_trans _ (conductor_dvd_level _) hd.dvd,
      ← (factorsThrough_conductor (Classical.choose hd.2)).2.choose_spec]

Premises used: Exists.choose_spec, DirichletCharacter.changeLevel_trans, DirichletCharacter.conductor_dvd_level, Classical.choose, DirichletCharacter.factorsThrough_conductor, DirichletCharacter.FactorsThrough.dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ =
    (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n)
      (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
        χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯)

Tactic:
hd.eq_changeLevel

Premises used: DirichletCharacter.FactorsThrough.χ₀, DirichletCharacter.FactorsThrough.eq_changeLevel
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ =
    (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n)
      (Classical.choose (p := fun (x : DirichletCharacter R d) ↦
        χ = (changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R n) x) ⋯)

Tactic:
exact hd.eq_changeLevel

Premises used: DirichletCharacter.FactorsThrough.eq_changeLevel
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.IsPrimitive ↔ χ.conductor = n

Tactic:
Iff.rfl

Premises used: Iff.rfl, DirichletCharacter.IsPrimitive
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
⊢ IsPrimitive.{u_1} (R := R) (n := 1) 1

Tactic:
Nat.dvd_one.mp (conductor_dvd_level _)

Premises used: DirichletCharacter.conductor_dvd_level, Nat.dvd_one, Iff.mp, DirichletCharacter.IsPrimitive
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
⊢ IsPrimitive.{u_1} (R := R) (n := 0) 1

Tactic:
conductor_eq_zero_iff_level_eq_zero.mpr rfl

Premises used: Iff.mpr, DirichletCharacter.conductor_eq_zero_iff_level_eq_zero, DirichletCharacter.IsPrimitive, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
rw : 1 ∣ n
⊢ conductor.{u_1} (R := R) (n := 1) 1 ∣ n

Tactic:
rw [(isPrimitive_def _).mp isPrimitive_one_level_one]

Premises used: DirichletCharacter.isPrimitive_def, DirichletCharacter.isPrimitive_one_level_one, Iff.mp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
⊢ 1 ∣ n

Tactic:
apply one_dvd _

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

Tactic:
(factorsThrough_conductor χ).choose_spec.choose_spec.symm

Premises used: Exists.choose_spec, DirichletCharacter.primitiveCharacter, DirichletCharacter.factorsThrough_conductor, Eq.symm
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
pos : ∀ (h : χ.conductor = 0), χ.primitiveCharacter.IsPrimitive
neg : ∀ (h : ¬χ.conductor = 0), χ.primitiveCharacter.IsPrimitive
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
by_cases h : χ.conductor = 0

Premises used: DirichletCharacter.conductor
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.conductor = 0

Tactic:
conductor_eq_zero_iff_level_eq_zero.mpr h

Premises used: Iff.mpr, DirichletCharacter.conductor_eq_zero_iff_level_eq_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.conductor = χ.conductor

Tactic:
convert! conductor_eq_zero_iff_level_eq_zero.mpr h

Premises used: Iff.mpr, DirichletCharacter.conductor_eq_zero_iff_level_eq_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : ¬χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
le_antisymm (Nat.le_of_dvd (Nat.pos_of_ne_zero h) (conductor_dvd_level _)) <|
      conductor_le_conductor_mem_conductorSet <| conductor_mem_conductorSet χ

Premises used: DirichletCharacter.conductor_le_conductor_mem_conductorSet, DirichletCharacter.conductor_dvd_level, DirichletCharacter.conductor_mem_conductorSet, le_antisymm, Nat.pos_of_ne_zero, DirichletCharacter.IsPrimitive, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : ¬χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
exact le_antisymm (Nat.le_of_dvd (Nat.pos_of_ne_zero h) (conductor_dvd_level _)) <|
      conductor_le_conductor_mem_conductorSet <| conductor_mem_conductorSet χ

Premises used: DirichletCharacter.conductor_le_conductor_mem_conductorSet, DirichletCharacter.conductor_dvd_level, DirichletCharacter.conductor_mem_conductorSet, le_antisymm, Nat.pos_of_ne_zero, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
⊢ NeZero (conductor.{u_1} (R := R) (n := n) 1)

Tactic:
have : NeZero (conductor (1 : DirichletCharacter R n)) :=
    ⟨@conductor_one R _ n _ ▸ Nat.one_ne_zero⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
inst_1 : NeZero n
this : NeZero (conductor.{u_1} (R := R) (n := n) 1)
rw : conductor.{u_1} (R := R) (n := conductor.{u_1} (R := R) (n := n) 1) (primitiveCharacter 1) = 1
rw₁ : conductor.{u_1} (R := R) (n := n) 1 = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ Eq.{u_1 + 1} (α := DirichletCharacter R (conductor.{u_1} (R := R) (n := n) 1)) (primitiveCharacter 1) 1

Tactic:
rw [eq_one_iff_conductor_eq_one,
    (isPrimitive_def _).1 (1 : DirichletCharacter R n).primitiveCharacter_isPrimitive,
    conductor_one]

Premises used: DirichletCharacter.isPrimitive_def, DirichletCharacter.conductor_one, DirichletCharacter.primitiveCharacter_isPrimitive, DirichletCharacter.eq_one_iff_conductor_eq_one, Iff.mp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
contrapose : ∀ (hd : d = 0), d ∉ χ.conductorSet
⊢ d ≠ 0

Tactic:
contrapose hd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d = 0
⊢ d ∉ χ.conductorSet

Tactic:
hd ▸ zero_ne_mem_conductorSet χ

Premises used: Eq.rec, Eq.symm, DirichletCharacter.zero_ne_mem_conductorSet
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d = 0
⊢ d ∉ χ.conductorSet

Tactic:
exact hd ▸ zero_ne_mem_conductorSet χ
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
⊢ NeZero d

Tactic:
have : NeZero d := ⟨by
    contrapose hd
    exact hd ▸ zero_ne_mem_conductorSet χ⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this_1 : NeZero d
this : d.gcd χ.conductor ∈ χ.conductorSet
⊢ χ.conductor ≤ d.gcd χ.conductor

Tactic:
have : χ.conductor ≤ d.gcd χ.conductor := Nat.sInf_le this
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this_1 : NeZero d
this_2 : d.gcd χ.conductor ∈ χ.conductorSet
this : χ.conductor ≤ d.gcd χ.conductor
contrapose! : ∀ (this : ¬χ.conductor ∣ d), d.gcd χ.conductor < χ.conductor
⊢ χ.conductor ∣ d

Tactic:
contrapose! this
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this_1 : NeZero d
this_2 : d.gcd χ.conductor ∈ χ.conductorSet
this : ¬χ.conductor ∣ d
⊢ d.gcd χ.conductor < χ.conductor

Tactic:
Nat.lt_of_le_of_ne ?_ (Nat.gcd_eq_right_iff_dvd.not.mpr this)

Premises used: Iff.mpr, Iff.not, Nat.lt_of_le_of_ne, Nat.gcd_eq_right_iff_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this_1 : NeZero d
this_2 : d.gcd χ.conductor ∈ χ.conductorSet
this : ¬χ.conductor ∣ d
refine : d.gcd χ.conductor ≤ χ.conductor
⊢ d.gcd χ.conductor < χ.conductor

Tactic:
refine Nat.lt_of_le_of_ne ?_ (Nat.gcd_eq_right_iff_dvd.not.mpr this)

Premises used: Iff.mpr, Iff.not, Nat.lt_of_le_of_ne, Nat.gcd_eq_right_iff_dvd
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this_1 : NeZero d
this_2 : d.gcd χ.conductor ∈ χ.conductorSet
this : ¬χ.conductor ∣ d
⊢ d.gcd χ.conductor ≤ χ.conductor

Tactic:
Nat.gcd_le_right _ <| Nat.pos_of_ne_zero <| conductor_ne_zero χ

Premises used: Nat.pos_of_ne_zero, Nat.gcd_le_right, DirichletCharacter.conductor_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this_1 : NeZero d
this_2 : d.gcd χ.conductor ∈ χ.conductorSet
this : ¬χ.conductor ∣ d
⊢ d.gcd χ.conductor ≤ χ.conductor

Tactic:
exact Nat.gcd_le_right _ <| Nat.pos_of_ne_zero <| conductor_ne_zero χ

Premises used: Nat.pos_of_ne_zero, Nat.gcd_le_right, DirichletCharacter.conductor_ne_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this : NeZero d
suffices : d.gcd χ.conductor ∈ χ.conductorSet
⊢ χ.conductor ∣ d

Tactic:
suffices d.gcd χ.conductor ∈ χ.conductorSet by
    have : χ.conductor ≤ d.gcd χ.conductor := Nat.sInf_le this
    contrapose! this
    refine Nat.lt_of_le_of_ne ?_ (Nat.gcd_eq_right_iff_dvd.not.mpr this)
    exact Nat.gcd_le_right _ <| Nat.pos_of_ne_zero <| conductor_ne_zero χ
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
hd : d ∈ χ.conductorSet
this : NeZero d
obtain :
  ∀ (hd : d ∣ n) (χ₀ : DirichletCharacter R d)
    (hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀),
    d.gcd χ.conductor ∈ χ.conductorSet
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
obtain ⟨hd, χ₀, hχ₀⟩ := hd