awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
        n =
      1 ∧
    ∀ m < n,
      0 < m →
        Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
              ⋯ ^
            m ≠
          1

Tactic:
⟨?_, fun m hm hm₀ h ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
h₁ :
  Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
      n =
    1
h₂ :
  ∀ (m : ℕ) (hm : m < n) (hm₀ : 0 < m)
    (h :
      Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
            ⋯ ^
          m =
        1),
    False
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
        n =
      1 ∧
    ∀ m < n,
      0 < m →
        Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
              ⋯ ^
            m ≠
          1

Tactic:
refine ⟨?_, fun m hm hm₀ h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
h₁ :
  (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
                ⋯ ^
              n) :
          Rˣ) :
      R) =
    (↑(↑1 : Rˣ) : R)
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
      n =
    1

Tactic:
ext
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
h₁ : (↑ζ' : R) ^ n = 1
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
                ⋯ ^
              n) :
          Rˣ) :
      R) =
    (↑(↑1 : Rˣ) : R)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
⊢ (↑ζ' : R) ^ n = 1

Tactic:
hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
⊢ (↑ζ' : R) ^ n = 1

Tactic:
exact hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h_1 : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
m : ℕ
hm : m < n
hm₀ : 0 < m
h :
  Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
      m =
    1
⊢ (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
                ⋯ ^
              m) :
          Rˣ) :
      R) =
    (↑(↑1 : Rˣ) : R)

Tactic:
rw [Subtype.ext_iff, Units.ext_iff] at h

Premises used: Units.ext_iff, Subtype.ext_iff
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h_1 : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
m : ℕ
hm : m < n
hm₀ : 0 < m
h : (↑ζ' : R) ^ m = 1
⊢ False

Tactic:
((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false

Premises used: LT.lt.false, IsPrimitiveRoot.dvd_of_pow_eq_one, LE.le.trans_lt, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h_1 : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
m : ℕ
hm : m < n
hm₀ : 0 < m
h : (↑ζ' : R) ^ m = 1
⊢ False

Tactic:
exact ((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false

Premises used: LT.lt.false, IsPrimitiveRoot.dvd_of_pow_eq_one, LE.le.trans_lt, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
have : 0 < n
have₁ : ∀ (hn₀ : 0 < n), ∃ (χ : MulChar F R), orderOf χ = n
have₂ : 0 < n
have₃ have₄ have₅ have₆ : ∀ (hn₀ : 0 < n), ∃ (χ : MulChar F R), orderOf χ = n
have₇ :
  ∀ (hn₀ : 0 < n),
    let ζ' := ⋯.unit;
    ∀ (h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1), ∃ (χ : MulChar F R), orderOf χ = n
h₁ :
  ∀ (hn₀ : 0 < n),
    let e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R;
    let ζ' := ⋯.unit;
    ∀ (h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1),
      orderOf (G := MulChar F R)
          ((e.symm : (a : ↥(rootsOfUnity (Fintype.card Fˣ) R)) → MulChar F R)
              (Subtype.mk (p := fun (x : Rˣ) ↦
                Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯) :
            MulChar F R) =
        n
h₂ :
  ∀ (hn₀ : 0 < n),
    let ζ' := ⋯.unit;
    ∀ (h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1),
      Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
              ⋯ ^
            n =
          1 ∧
        ∀ m < n,
          0 < m →
            Subtype.mk (p := fun (x : Rˣ) ↦
                  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
                m ≠
              1
h₃ :
  ∀ (hn₀ : 0 < n),
    let ζ' := ⋯.unit;
    ∀ (h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1),
      Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
            ⋯ ^
          n =
        1
h₄ h₅ :
  ∀ (hn₀ : 0 < n),
    let ζ' := ⋯.unit;
    ∀ (h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1) (m : ℕ) (hm : m < n) (hm₀ : 0 < m)
      (h :
        Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
              ⋯ ^
            m =
          1),
      False
⊢ ∃ (χ : MulChar F R), orderOf χ = n

Tactic:
classical
  have hn₀ : 0 < n := by
    refine Nat.pos_of_ne_zero fun hn ↦ ?_
    simp only [hn, zero_dvd_iff, Nat.sub_eq_zero_iff_le] at h
    exact (Fintype.one_lt_card.trans_le h).false
  let e := MulChar.equiv_rootsOfUnity F R
  let ζ' : Rˣ := (hζ.isUnit hn₀.ne').unit
  have h' : ζ' ^ (Fintype.card Fˣ : ℕ) = 1 :=
    Units.ext_iff.mpr <| (hζ.pow_eq_one_iff_dvd _).mpr <| Fintype.card_units (α := F) ▸ h
  use e.symm ⟨ζ', (mem_rootsOfUnity (Fintype.card Fˣ) ζ').mpr h'⟩
  rw [e.symm.orderOf_eq, orderOf_eq_iff hn₀]
  refine ⟨?_, fun m hm hm₀ h ↦ ?_⟩
  · ext
    push_cast
    exact hζ.pow_eq_one
  · rw [Subtype.ext_iff, Units.ext_iff] at h
    push_cast at h
    exact ((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false

Premises used: Units.ext_iff, Subtype.ext_iff, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
rw : orderOf χ ∣ Fintype.card.{u_1} Fˣ
⊢ orderOf χ ∣ Fintype.card F - 1

Tactic:
rw [← Fintype.card_units]

Premises used: Fintype.card_units
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card.{u_1} Fˣ

Tactic:
orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Premises used: orderOf_dvd_of_pow_eq_one, MulChar.pow_card_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card.{u_1} Fˣ

Tactic:
exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Premises used: orderOf_dvd_of_pow_eq_one, MulChar.pow_card_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
rw rw₁ rw₂ : orderOf χ ∣ Fintype.card.{u_1} Fˣ
⊢ orderOf χ ∣ Fintype.card F - 1

Tactic:
classical
  rw [← Fintype.card_units]
  exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Premises used: Fintype.card_units
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
inst_3 : DecidableEq F
ζ : R
hζ : IsPrimitiveRoot ζ (Fintype.card.{u_1} Fˣ)
rw rw₁ : Fintype.card F - 1 ∣ Fintype.card F - 1
⊢ Fintype.card.{u_1} Fˣ ∣ Fintype.card F - 1

Tactic:
rw [Fintype.card_units]

Premises used: Fintype.card_units
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
⊢ IsUnit.{u_2} (M := R) ((χ : (a : F) → R) a : R)

Tactic:
have hu : IsUnit (χ a) := ha.isUnit.map χ
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit.{u_2} (M := R) ((χ : (a : F) → R) a : R)
⊢ ∃ (ζ : Rˣ), Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) ζ ∧ (↑ζ : R) = (χ : (a : F) → R) a

Tactic:
⟨hu.unit, ?_, hu.unit_spec⟩

Premises used: And.intro, Exists.intro, IsUnit.unit, IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit.{u_2} (M := R) ((χ : (a : F) → R) a : R)
refine : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) hu.unit
⊢ ∃ (ζ : Rˣ), Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) ζ ∧ (↑ζ : R) = (χ : (a : F) → R) a

Tactic:
refine ⟨hu.unit, ?_, hu.unit_spec⟩
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit.{u_2} (M := R) ((χ : (a : F) → R) a : R)
⊢ a = (↑(IsUnit.unit (a := a) ⋯) : F)

Tactic:
simp only [IsUnit.unit_spec]

Premises used: IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit.{u_2} (M := R) ((χ : (a : F) → R) a : R)
rw : hu.unit ^ orderOf χ = 1
rw₁ : (↑(hu.unit ^ orderOf χ) : R) = (↑1 : R)
rw₂ : (↑hu.unit : R) ^ orderOf χ = (↑1 : R)
rw₃ : (↑hu.unit : R) ^ orderOf χ = 1
rw₄ : HPow.hPow (α := R) ((χ : (a : F) → R) a : R) (orderOf χ) = 1
rw₅ : Eq.{u_2 + 1} (α := R) ((χ ^ orderOf χ : (a : F) → R) a : R) (1 : R)
rw₆ : Eq.{u_2 + 1} (α := R) ((1 : (a : F) → R) a : R) (1 : R)
rw₇ : Eq.{u_2 + 1} (α := R) ((1 : (a : F) → R) (↑(IsUnit.unit (a := a) ⋯) : F) : R) (1 : R)
rw₈ rw₉ : Eq.{u_2 + 1} (α := R) 1 1
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) hu.unit

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one,
    IsUnit.unit_spec, ← χ.pow_apply' χ.orderOf_pos.ne', pow_orderOf_eq_one,
    show a = (isUnit_iff_ne_zero.mpr ha).unit by simp only [IsUnit.unit_spec],
    MulChar.one_apply_coe]

Premises used: mem_rootsOfUnity, Units.ext_iff, MulChar.one_apply_coe, MulChar.pow_apply', LT.lt.ne', pow_orderOf_eq_one, MulChar.orderOf_pos, Units.val_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
obtain :
  ∀ (μ : Rˣ) (hμ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) μ)
    (hμ₂ : (↑μ : R) = (χ : (a : F) → R) a),
    ∃ (ζ : Rˣ), Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ ∧ (↑ζ : R) = (χ : (a : F) → R) a
⊢ ∃ (ζ : Rˣ), Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ ∧ (↑ζ : R) = (χ : (a : F) → R) a

Tactic:
obtain ⟨μ, hμ₁, hμ₂⟩ := χ.apply_mem_rootsOfUnity_orderOf ha

Premises used: MulChar.apply_mem_rootsOfUnity_orderOf
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
μ : Rˣ
hμ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) μ
hμ₂ : (↑μ : R) = (χ : (a : F) → R) a
⊢ ∃ (ζ : Rˣ), Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ ∧ (↑ζ : R) = (χ : (a : F) → R) a

Tactic:
⟨μ, rootsOfUnity_le_of_dvd (orderOf_dvd_of_pow_eq_one hχ) hμ₁, hμ₂⟩

Premises used: orderOf_dvd_of_pow_eq_one, And.intro, Exists.intro, rootsOfUnity_le_of_dvd
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
μ : Rˣ
hμ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (orderOf χ) R) μ
hμ₂ : (↑μ : R) = (χ : (a : F) → R) a
⊢ ∃ (ζ : Rˣ), Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ ∧ (↑ζ : R) = (χ : (a : F) → R) a

Tactic:
exact ⟨μ, rootsOfUnity_le_of_dvd (orderOf_dvd_of_pow_eq_one hχ) hμ₁, hμ₂⟩
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
obtain :
  ∀ (ζ : Rˣ) (hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ) (hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a),
    ∃ k < n, (χ : (a : F) → R) a = μ ^ k
⊢ ∃ k < n, (χ : (a : F) → R) a = μ ^ k

Tactic:
obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ ha

Premises used: MulChar.apply_mem_rootsOfUnity_of_pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
⊢ (↑ζ : R) ^ n = 1

Tactic:
have hζ' : ζ.val ^ n = 1 := (mem_rootsOfUnity' n ↑ζ).mp hζ₁
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
hζ' : (↑ζ : R) ^ n = 1
obtain : ∀ (k : ℕ) (hk₁ : k < n) (hk₂ : μ ^ k = (↑ζ : R)), ∃ k < n, (χ : (a : F) → R) a = μ ^ k
⊢ ∃ k < n, (χ : (a : F) → R) a = μ ^ k

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := hμ.eq_pow_of_pow_eq_one hζ'

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
hζ' : (↑ζ : R) ^ n = 1
k : ℕ
hk₁ : k < n
hk₂ : μ ^ k = (↑ζ : R)
⊢ ∃ k < n, (χ : (a : F) → R) a = μ ^ k

Tactic:
⟨k, hk₁, (hζ₂ ▸ hk₂).symm⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
hζ' : (↑ζ : R) ^ n = 1
k : ℕ
hk₁ : k < n
hk₂ : μ ^ k = (↑ζ : R)
⊢ ∃ k < n, (χ : (a : F) → R) a = μ ^ k

Tactic:
exact ⟨k, hk₁, (hζ₂ ▸ hk₂).symm⟩
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
inl : Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) 0 : R)
inr : ∀ (h : a ≠ 0), Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)

Tactic:
rcases eq_or_ne a 0 with rfl | h

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) 0 : R)

Tactic:
χ.map_zero ▸ Subalgebra.zero_mem _

Premises used: Set.Mem, Subalgebra.zero_mem, Eq.rec, Eq.symm, MulChar.map_zero
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) 0 : R)

Tactic:
exact χ.map_zero ▸ Subalgebra.zero_mem _
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
inr :
  ∀ (ζ : Rˣ) (hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ) (hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a),
    Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)

Tactic:
obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ h

Premises used: MulChar.apply_mem_rootsOfUnity_of_pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
⊢ (↑ζ : R) ^ n = (↑1 : R)

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁

Premises used: mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
hζ₃ : (↑ζ : R) ^ n = (↑1 : R)
⊢ (↑ζ : R) = (χ : (a : F) → R) a

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁

Premises used: mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : (↑ζ : R) ^ n = (↑1 : R)
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
inr : ∀ k < n, ∀ (hk : μ ^ k = (↑ζ : R)), Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)

Tactic:
obtain ⟨k, _, hk⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one hμ hζ₁

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : (↑ζ : R) ^ n = (↑1 : R)
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
k : ℕ
left : k < n
hk : μ ^ k = (↑ζ : R)
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)

Tactic:
hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k

Premises used: Eq.rec, Int, Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : (↑ζ : R) ^ n = (↑1 : R)
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
k : ℕ
left : k < n
hk : μ ^ k = (↑ζ : R)
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)

Tactic:
exact hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
μ : R
hμ : IsPrimitiveRoot μ (orderOf χ)
a : F
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)

Tactic:
have : NeZero (orderOf χ) := ⟨χ.orderOf_pos.ne'⟩
  apply_mem_algebraAdjoin_of_pow_eq_one (pow_orderOf_eq_one χ) hμ a

Premises used: MulChar.apply_mem_algebraAdjoin_of_pow_eq_one, NeZero.mk, LT.lt.ne', pow_orderOf_eq_one, MulChar.orderOf_pos
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
h : p ∣ x - y
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {p}))
    ((Ideal.Quotient.mk (span {p}) : (a : R) → R ⧸ span {p}) x : HasQuotient.Quotient R (B := Ideal R) (span {p}))
    ((Ideal.Quotient.mk (span {p}) : (a : R) → R ⧸ span {p}) y : HasQuotient.Quotient R (B := Ideal R) (span {p}))

Tactic:
rw [← mem_span_singleton, ← Ideal.Quotient.eq] at h

Premises used: Ideal.Quotient.eq, Ideal.mem_span_singleton