awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)
have pos : ∀ (ζ : (i : ℕ) → L) (hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)),
  Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)
Tactic: choose ζ hζ using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)
have pos : Continuous (X := Gal(L/K)) (Y := ℤ_[p])
  (⇑(MonoidHom.comp (Units.coeHom ℤ_[p])
        (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L))) :
    (a : Gal(L/K)) → ℤ_[p])
Tactic: refine Continuous.of_coeHom_comp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p])
    (⇑(MonoidHom.comp (Units.coeHom ℤ_[p])
          (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L))) :
      (a : Gal(L/K)) → ℤ_[p])
have pos : ContinuousAt (X := Gal(L/K)) (Y := ℤ_[p])
  (⇑(MonoidHom.comp (Units.coeHom ℤ_[p])
        (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L))) :
    (a : Gal(L/K)) → ℤ_[p])
  1
Tactic: apply continuous_of_continuousAt_one
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ ContinuousAt (X := Gal(L/K)) (Y := ℤ_[p])
    (⇑(MonoidHom.comp (Units.coeHom ℤ_[p])
          (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L))) :
      (a : Gal(L/K)) → ℤ_[p])
    1
have pos : ∀ (ib : ℝ),
  0 < ib →
    ∃ (ia : Set Gal(L/K)),
      Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) ia ∧
        ∀ x ∈ id ia,
          Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ib)
            (((MonoidHom.comp (Units.coeHom ℤ_[p])
                      (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p)
                        (MulSemiringAction.toRingAut Gal(L/K) L)) :
                    Gal(L/K) →* ℤ_[p]) :
                  (a : Gal(L/K)) → ℤ_[p])
                x :
              ℤ_[p])
Tactic: rw [ContinuousAt, map_one, (galGroupBasis K L).nhds_one_hasBasis.tendsto_iff
    (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
⊢ ∃ (k : ℕ), k ≠ 0 ∧ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
have obtain : ∀ (k : ℕ) (hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε),
  ∃ (k : ℕ), k ≠ 0 ∧ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
Tactic: obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑(k + 1) : ℤ)) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))
have ha : LE.le (α := ℝ) 1 (↑p : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
ha : LE.le (α := ℝ) 1 (↑p : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑(k + 1) : ℤ)) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))
have hmn : k ≤ k + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
⊢ ∃ (ia : Set Gal(L/K)),
    Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) ia ∧
      ∀ x ∈ id ia,
        Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ε)
          (((MonoidHom.comp (Units.coeHom ℤ_[p])
                    (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
                  Gal(L/K) →* ℤ_[p]) :
                (a : Gal(L/K)) → ℤ_[p])
              x :
            ℤ_[p])
have pos : ∀ (k : ℕ) (hk' : k ≠ 0) (hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε),
  ∃ (ia : Set Gal(L/K)),
    Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) ia ∧
      ∀ x ∈ id ia,
        Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ε)
          (((MonoidHom.comp (Units.coeHom ℤ_[p])
                    (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
                  Gal(L/K) →* ℤ_[p]) :
                (a : Gal(L/K)) → ℤ_[p])
              x :
            ℤ_[p])
Tactic: obtain ⟨k, hk', hk⟩ : ∃ k : ℕ, k ≠ 0 ∧ p ^ (-k : ℤ) < ε := by
    obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε
    exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
⊢ ∃ (ia : Set Gal(L/K)),
    Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) ia ∧
      ∀ x ∈ id ia,
        Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ε)
          (((MonoidHom.comp (Units.coeHom ℤ_[p])
                    (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
                  Gal(L/K) →* ℤ_[p]) :
                (a : Gal(L/K)) → ℤ_[p])
              x :
            ℤ_[p])
have pos : IsIntegral K (ζ k)
Tactic: refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
pos : IsIntegral K (ζ k)
⊢ ∃ (ia : Set Gal(L/K)),
    Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) ia ∧
      ∀ x ∈ id ia,
        Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ε)
          (((MonoidHom.comp (Units.coeHom ℤ_[p])
                    (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
                  Gal(L/K) →* ℤ_[p]) :
                (a : Gal(L/K)) → ℤ_[p])
              x :
            ℤ_[p])
have pos₁ : ∀ (x : Gal(L/K)),
  Membership.mem (γ := Set Gal(L/K))
      (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) x →
    Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ε)
      (((MonoidHom.comp (Units.coeHom ℤ_[p])
                (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
              Gal(L/K) →* ℤ_[p]) :
            (a : Gal(L/K)) → ℤ_[p])
          x :
        ℤ_[p])
Tactic: refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
⊢ Membership.mem (α := ℤ_[p]) (γ := Set ℤ_[p]) (Metric.ball 1 ε)
    (((MonoidHom.comp (Units.coeHom ℤ_[p])
              (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
            Gal(L/K) →* ℤ_[p]) :
          (a : Gal(L/K)) → ℤ_[p])
        σ :
      ℤ_[p])
have pos : dist (α := ℤ_[p])
    (((MonoidHom.comp (Units.coeHom ℤ_[p])
              (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
            Gal(L/K) →* ℤ_[p]) :
          (a : Gal(L/K)) → ℤ_[p])
        σ :
      ℤ_[p])
    (1 : ℤ_[p]) ≤
  HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))
Tactic: refine lt_of_le_of_lt ?_ hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
⊢ dist (α := ℤ_[p])
      (((MonoidHom.comp (Units.coeHom ℤ_[p])
                (MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
              Gal(L/K) →* ℤ_[p]) :
            (a : Gal(L/K)) → ℤ_[p])
          σ :
        ℤ_[p])
      (1 : ℤ_[p]) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))
have pos : dist (α := ℤ_[p]) (↑(((cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ) : (a : L ≃+* L) → ℤ_[p]ˣ) σ.toRingEquiv) : ℤ_[p])
    1 ≤
  HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
⊢ dist (α := ℤ_[p])
      (↑(((cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ) : (a : L ≃+* L) → ℤ_[p]ˣ) σ.toRingEquiv) : ℤ_[p]) 1 ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))
have pos : Eq (α := ZMod (p ^ k)) 1
  (↑(((modularCyclotomicCharacter L sorry : (L ≃+* L) →* (ZMod (p ^ k))ˣ) : (a : L ≃+* L) → (ZMod (p ^ k))ˣ)
        σ.toRingEquiv) :
    ZMod (p ^ k))
Tactic: rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow,
      RingHom.mem_ker, map_sub, map_one, cyclotomicCharacter.toZModPow,
      sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
⊢ Eq (α := ZMod (p ^ k)) 1
    (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ k))ˣ) : (a : L ≃+* L) → (ZMod (p ^ k))ˣ)
          σ.toRingEquiv) :
      ZMod (p ^ k))
have pos : ∀ (t : Lˣ),
  Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) t →
    (σ.toRingEquiv : (a : L) → L) (↑t : L) = (↑t : L) ^ ZMod.val (n := p ^ k) 1
Tactic: apply modularCyclotomicCharacter.unique
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
t : Lˣ
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) t
⊢ (σ.toRingEquiv : (a : L) → L) (↑t : L) = (↑t : L) ^ ZMod.val (n := p ^ k) 1
have pos : ∀ (i : ℕ) (hi : i < p ^ k) (ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) (sorry.unit ^ i)),
  (σ.toRingEquiv : (a : L) → L) (↑(sorry.unit ^ i) : L) = (↑(sorry.unit ^ i) : L) ^ ZMod.val (n := p ^ k) 1
Tactic: obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
i : ℕ
hi : i < p ^ k
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) (⋯.unit ^ i)
⊢ (σ.toRingEquiv : (a : L) → L) (↑(⋯.unit ^ i) : L) = (↑(⋯.unit ^ i) : L) ^ ZMod.val (n := p ^ k) 1
have pos : (σ.toRingEquiv : (a : L) → L) (↑(sorry.unit ^ i) : L) = (↑(sorry.unit ^ i) : L)
Tactic: rw [ZMod.val_one'', pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : (i : ℕ) → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
σ : Gal(L/K)
hσ :
  Membership.mem (γ := Set Gal(L/K))
    (id ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) (IntermediateField.fixingSubgroup K⟮ζ k⟯))) σ
i : ℕ
hi : i < p ^ k
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) (⋯.unit ^ i)
pos : (σ.toRingEquiv : (a : L) → L) (↑(⋯.unit ^ i) : L) = (↑(⋯.unit ^ i) : L)
⊢ (σ.toRingEquiv : (a : L) → L) (↑(⋯.unit ^ i) : L) = (↑(⋯.unit ^ i) : L) ^ ZMod.val (n := p ^ k) 1
have pos₁ : p ^ k ≠ 1
Tactic: rw [ZMod.val_one'', pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have this : NumberField K
Tactic: haveI : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional {n} ℚ K)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have H₁ : (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
  gen (subOnePowerBasis ℚ hζ)
Tactic: have H₁ : (aeval (hζ.powerBasis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.subOnePowerBasis ℚ).gen := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have H₂ : (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
  gen (IsPrimitiveRoot.powerBasis ℚ hζ)
Tactic: have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have refine_1 : ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
  IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))
Tactic: refine discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
refine_1 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have refine_2 : ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
  minpoly ℚ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) =
    Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)))
Tactic: refine discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
refine_1 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))
refine_2 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    minpoly ℚ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) =
      Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)))
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have refine_3 : ∀ (i : Fin (dim (subOnePowerBasis ℚ hζ))) (j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))),
  IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))
Tactic: refine discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _