awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
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]ˣ)
⊢ 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
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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]ˣ)

Tactic:
Continuous.of_coeHom_comp ?_

Premises used: Continuous.of_coeHom_comp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
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])
⊢ 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:
refine Continuous.of_coeHom_comp ?_

Premises used: Continuous.of_coeHom_comp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
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
⊢ 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:
apply continuous_of_continuousAt_one

Premises used: continuous_of_continuousAt_one
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
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])
⊢ 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:
rw [ContinuousAt, map_one, (galGroupBasis K L).nhds_one_hasBasis.tendsto_iff
    (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))]

Premises used: Filter.HasBasis.tendsto_iff, ContinuousAt, galGroupBasis, GroupFilterBasis.nhds_one_hasBasis, map_one, Metric.nhds_basis_ball
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 < ε
obtain :
  ∀ (k : ℕ) (hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε),
    ∃ (k : ℕ), k ≠ 0 ∧ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
⊢ ∃ (k : ℕ), k ≠ 0 ∧ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε

Tactic:
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε

Premises used: PadicInt.exists_pow_neg_lt
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℤ)) < ε
⊢ k + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℝ)
hmn : k ≤ k + 1
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑(k + 1) : ℤ)) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℤ)) < ε
⊢ LE.le (α := ℝ) 1 (↑p : ℝ)

Tactic:
simp [‹Fact p.Prime›.1.one_le]

Premises used: Nat.Prime.one_le, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℤ)) < ε
⊢ k ≤ k + 1

Tactic:
simp [‹Fact p.Prime›.1.one_le]

Premises used: Nat.Prime.one_le, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℤ)) < ε
⊢ ∃ (k : ℕ), k ≠ 0 ∧ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε

Tactic:
exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 < ε
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])
⊢ ∃ (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⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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])

Tactic:
⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩

Premises used: And.intro, IntermediateField.adjoin, Exists.intro, IntermediateField.adjoin.finiteDimensional, Singleton.singleton, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
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])
⊢ ∃ (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:
refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℤ)) < ε
⊢ IsIntegral K (ζ k)

Tactic:
((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top

Premises used: IsPrimitiveRoot.isIntegral, IsIntegral.tower_top, Nat.pos_of_neZero
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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 : ℤ)) < ε
⊢ IsIntegral K (ζ k)

Tactic:
exact ((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top

Premises used: IsPrimitiveRoot.isIntegral, IsIntegral.tower_top, Nat.pos_of_neZero
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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])

Tactic:
lt_of_le_of_lt ?_ hk

Premises used: lt_of_le_of_lt, Set.Mem, setOf, Metric.ball
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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⟯))) σ
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 : ℤ))
⊢ 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])

Tactic:
refine lt_of_le_of_lt ?_ hk

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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⟯))) σ
pos :
  dist (α := ℤ_[p])
      (↑(((cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ) : (a : L ≃+* L) → ℤ_[p]ˣ) σ.toRingEquiv) : ℤ_[p]) 1 ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑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 : ℤ))

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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⟯))) σ
pos :
  Eq (α := ZMod (p ^ k)) 1
    (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ k))ˣ) : (a : L ≃+* L) → (ZMod (p ^ k))ˣ)
          σ.toRingEquiv) :
      ZMod (p ^ k))
⊢ dist (α := ℤ_[p])
      (↑(((cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ) : (a : L ≃+* L) → ℤ_[p]ˣ) σ.toRingEquiv) : ℤ_[p]) 1 ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑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]

Premises used: cyclotomicCharacter.toZModPow, dist_eq_norm, map_sub, sub_eq_zero, RingHom.mem_ker, eq_comm, PadicInt.norm_le_pow_iff_mem_span_pow, PadicInt.ker_toZModPow, map_one
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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⟯))) σ
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
⊢ Eq (α := ZMod (p ^ k)) 1
    (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ k))ˣ) : (a : L ≃+* L) → (ZMod (p ^ k))ˣ)
          σ.toRingEquiv) :
      ZMod (p ^ k))

Tactic:
apply modularCyclotomicCharacter.unique

Premises used: modularCyclotomicCharacter.unique
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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
pos :
  ∀ (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
⊢ (σ.toRingEquiv : (a : L) → L) (↑t : L) = (↑t : L) ^ ZMod.val (n := p ^ k) 1

Tactic:
obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht

Premises used: IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity, IsPrimitiveRoot.isUnit_unit, NeZero.out, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
pos₁ : p ^ k ≠ 1
⊢ (σ.toRingEquiv : (a : L) → L) (↑(⋯.unit ^ i) : L) = (↑(⋯.unit ^ i) : L) ^ ZMod.val (n := p ^ k) 1

Tactic:
rw [ZMod.val_one'', pow_one]

Premises used: ZMod.val_one'', pow_one
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)

Tactic:
hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩

Premises used: IntermediateField.mem_adjoin_simple_self, Subtype.mk, HPow.hPow, pow_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)

Tactic:
exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩

Premises used: IntermediateField.mem_adjoin_simple_self, Subtype.mk, HPow.hPow, pow_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
⊢ p ^ k ≠ 1

Tactic:
(one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne'

Premises used: Nat.Prime.one_lt, LT.lt.ne', one_lt_pow₀, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
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)
⊢ p ^ k ≠ 1

Tactic:
exact (one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne'

Premises used: Nat.Prime.one_lt, LT.lt.ne', one_lt_pow₀, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ NumberField K

Tactic:
haveI : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional {n} ℚ K)
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
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
⊢ (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)

Tactic:
simp