awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
hζ :
  IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
have rw : IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A
  ↥A[HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
        HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂)]
Tactic: rw [sup_comm, (isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp h₁,
    (isCyclotomicExtension_singleton_iff_eq_adjoin n₂ C₂ hζ₂).mp h₂, ← adjoin_union,
    Set.union_singleton, hζ₁.adjoin_pair_eq A hζ₂ (NeZero.ne _) (NeZero.ne _) hζ]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
hζ :
  IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A
    ↥A[HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
          HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂)]
have this : NeZero (n₁.lcm n₂)
Tactic: have : NeZero (n₁.lcm n₂) := ⟨Nat.lcm_ne_zero (NeZero.ne _) (NeZero.ne _)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
F : IntermediateField K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{w, z} {n} K ↥F ↔ F = K⟮ζ⟯
have rw : IsCyclotomicExtension.{w, z} {n} K ↥F ↔ F.toSubalgebra = K[ζ]
Tactic: rw [← toSubalgebra_inj, adjoin_simple_toSubalgebra_of_isAlgebraic
    (hζ.isIntegral (NeZero.pos _)).tower_top.isAlgebraic]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₁
inst_4 : NeZero n₂
⊢ IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
have this : FiniteDimensional.{w, z} K ↥F₁
Tactic: have : FiniteDimensional K F₁ := IsCyclotomicExtension.finite_of_singleton n₁ K F₁
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₁
inst_4 : NeZero n₂
this : FiniteDimensional.{w, z} K ↥F₁
⊢ IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
have this₁ : IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁.toSubalgebra ⊔ F₂.toSubalgebra)
Tactic: have := IsCyclotomicExtension.lcm_sup n₁ n₂ F₁.toSubalgebra F₂.toSubalgebra
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₁
inst_4 : NeZero n₂
this_1 : FiniteDimensional.{w, z} K ↥F₁
this : IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁.toSubalgebra ⊔ F₂.toSubalgebra)
⊢ IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
have rwa : ∀ (this : IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂).toSubalgebra),
  IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
Tactic: rwa [← sup_toSubalgebra_of_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
⊢ ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ m) : L)
have obtain : ∀ (m : ℤ)
  (hm :
    ∀ (g_1 : ↥(rootsOfUnity n L)),
      (MulEquiv.toMonoidHom (MulEquiv.restrictRootsOfUnity (↑g : L ≃* L) n) :
            (a : ↥(rootsOfUnity n L)) → ↥(rootsOfUnity n L))
          g_1 =
        g_1 ^ m),
  ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ m) : L)
Tactic: obtain ⟨m, hm⟩ := MonoidHom.map_cyclic ((g : L ≃* L).restrictRootsOfUnity n).toMonoidHom
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
i k : ℕ
hi : k ≤ i
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ i) - aux g (p ^ k)
have obtain : ∀ (i : ℕ) (hi : k ≤ k + i), HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Tactic: obtain ⟨i, rfl⟩ := exists_add_of_le hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have obtain : ∀ (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + i))), HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Tactic: obtain ⟨ζ, hζ⟩ := HasEnoughRootsOfUnity.exists_primitiveRoot L (p ^ (k + i))
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
Tactic: have h := hζ.pow (a := p ^ i) (Nat.pos_of_neZero _) (Nat.pow_add' _ _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
⊢ ⋯.unit = ⋯.unit ^ p ^ i
have huv : (↑sorry.unit : L) = (↑(sorry.unit ^ p ^ i) : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have h_unit : sorry.unit = sorry.unit ^ p ^ i
Tactic: have h_unit : (h.isUnit NeZero.out).unit =
      (hζ.isUnit NeZero.out).unit ^ (p ^ i) := by ext; rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₁ : (g : (a : L) → L)
    (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) sorry.unit sorry) :
          Lˣ) :
      L) =
  (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) sorry.unit sorry) :
          Lˣ) ^
        aux g (p ^ (k + i))) :
    L)
Tactic: have H₁ := aux_spec g (p ^ (k + i))
    ⟨_, (hζ.isUnit_unit NeZero.out).mem_rootsOfUnity⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ :
  (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) ^
          aux g (p ^ (k + i))) :
      L)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₂ : (g : (a : L) → L)
    (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) sorry.unit sorry) : Lˣ) :
      L) =
  (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) sorry.unit sorry) : Lˣ) ^
        aux g (p ^ k)) :
    L)
Tactic: have H₂ := aux_spec g (p ^ k)
    ⟨_, (h.isUnit_unit NeZero.out).mem_rootsOfUnity⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ :
  (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) ^
          aux g (p ^ (k + i))) :
      L)
H₂ :
  (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) ⋯.unit ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) ⋯.unit ⋯) :
            Lˣ) ^
          aux g (p ^ k)) :
      L)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₃ : HPow.hPow (α := L) ((g : (a : L) → L) ζ : L) (p ^ i) = (↑(sorry.unit ^ aux g (p ^ k)) : L)
Tactic: simp only [IsUnit.unit_spec, map_pow] at H₁ H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : HPow.hPow (α := L) ((g : (a : L) → L) ζ : L) (p ^ i) = (↑(⋯.unit ^ aux g (p ^ k)) : L)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₃ : (sorry.unit ^ aux g (p ^ (k + i))) ^ p ^ i / (sorry.unit ^ p ^ i) ^ aux g (p ^ k) = 1
Tactic: rw [H₁, ← Units.val_pow_eq_pow_val, ← Units.ext_iff, h_unit, ← div_eq_one] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i / (⋯.unit ^ p ^ i) ^ aux g (p ^ k) = 1
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₃ : sorry.unit ^ (aux g (p ^ (k + i)) * (↑(p ^ i) : ℤ) - (↑(p ^ i) : ℤ) * aux g (p ^ k)) = 1
Tactic: simp only [← zpow_natCast, ← zpow_mul, div_eq_mul_inv, ← zpow_sub] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : ⋯.unit ^ (aux g (p ^ (k + i)) * (↑(p ^ i) : ℤ) - (↑(p ^ i) : ℤ) * aux g (p ^ k)) = 1
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₃ : (↑(p ^ (k + i)) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
Tactic: rw [(hζ.isUnit_unit NeZero.out).zpow_eq_one_iff_dvd, mul_comm, ← mul_sub] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : (↑(p ^ (k + i)) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
| (↑(p ^ (k + i)) : ℤ)
have rw : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ)
Tactic: rw [Nat.pow_add', Nat.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : (↑(p ^ (k + i)) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have H₃ : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
Tactic: conv_lhs at H₂ => rw [Nat.pow_add', Nat.cast_mul]
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have rwa : ∀ (H₂ : (↑(p ^ k) : ℤ) ∣ aux g (p ^ (k + i)) - aux g (p ^ k)),
  HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Tactic: rwa [mul_dvd_mul_iff_left (by simp [NeZero.ne p]), Nat.cast_pow] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
rwa :
  ∀ (H₂ : (↑(p ^ k) : ℤ) ∣ aux g (p ^ (k + i)) - aux g (p ^ k)),
    HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
have rwa₁ : ∀ (H₂ : HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)),
  HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Tactic: rwa [mul_dvd_mul_iff_left (by simp [NeZero.ne p]), Nat.cast_pow] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (g : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)
have rw : (↑(↑(t ^ aux g n) : Lˣ) : L) = (↑((↑t : Lˣ) ^ (aux g n % (↑(Fintype.card.{u} ↥(rootsOfUnity n L)) : ℤ))) : L)
Tactic: rw [modularCyclotomicCharacter.aux_spec g n t, ← zpow_natCast, modularCyclotomicCharacter.toFun,
    ZMod.val_intCast, ← Subgroup.coe_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ c.val) : L)
⊢ c = χ₀ n g
have apply : ∀ (ζ : ↥(rootsOfUnity n L)), ζ ^ c.val = ζ ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)
Tactic: apply IsCyclic.ext Nat.card_eq_fintype_card (fun ζ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ c.val) : L)
ζ : ↥(rootsOfUnity n L)
⊢ ζ ^ c.val = ζ ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)
have hc₁ : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
Tactic: specialize hc ζ
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
⊢ ζ ^ c.val = ζ ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)
have suffices : (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)
Tactic: suffices ((ζ ^ c.val : Lˣ) : L) = (ζ ^ (χ₀ n g).val : Lˣ) by exact_mod_cast this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
⊢ (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)
have rw : (↑((↑ζ : Lˣ) ^ c.val) : L) = (g : (a : L) → L) (↑(↑ζ : Lˣ) : L)
Tactic: rw [← toFun_spec g ζ, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
rw : (↑((↑ζ : Lˣ) ^ c.val) : L) = (g : (a : L) → L) (↑(↑ζ : Lˣ) : L)
⊢ (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)
have rw₁ : (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
Tactic: rw [← toFun_spec g ζ, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
⊢ Eq (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n (RingEquiv.refl L)) 1
have refine : ∀ (t : ↥(rootsOfUnity n L)),
  (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
Tactic: refine (toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
have this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
Tactic: have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
have inl : ∀ (h : 1 < Fintype.card.{u} ↥(rootsOfUnity n L)),
  (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
Tactic: obtain (h | h) := this.lt_or_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
inl :
  ∀ (h : 1 < Fintype.card.{u} ↥(rootsOfUnity n L)),
    (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
      (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
have inr : ∀ (h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)),
  (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
Tactic: obtain (h | h) := this.lt_or_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 < Fintype.card.{u} ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
have this₁ : Fact (1 < Fintype.card.{u} ↥(rootsOfUnity n L))
Tactic: have := Fact.mk h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
have this₁ : Subsingleton.{u + 1} ↥(rootsOfUnity n L)
Tactic: have := Fintype.card_le_one_iff_subsingleton.mp h.ge