awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ p = (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})

Tactic:
(absNorm_span_zeta_sub_one ..).symm

Premises used: IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Ne (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) ⊥

Tactic:
(Submodule.ne_bot_iff _).mpr ⟨p, p_mem_span_zeta_sub_one p k hζ, NeZero.natCast_ne p (𝓞 K)⟩

Premises used: Iff.mpr, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, Nat.cast, And.intro, Submodule.ne_bot_iff, Exists.intro, NumberField.RingOfIntegers, NeZero.natCast_ne
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
rw : Eq (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))
⊢ LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑

Tactic:
rw [liesOver_iff]

Premises used: Ideal.liesOver_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Eq (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))

Tactic:
Ideal.IsMaximal.eq_of_le (Int.ideal_span_isMaximal_of_prime p) IsPrime.ne_top' ?_

Premises used: Int.ideal_span_isMaximal_of_prime, Ideal.IsMaximal.eq_of_le, Ideal.IsPrime.ne_top'
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
refine : LE.le (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))
⊢ Eq (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))

Tactic:
refine Ideal.IsMaximal.eq_of_le (Int.ideal_span_isMaximal_of_prime p) IsPrime.ne_top' ?_

Premises used: Int.ideal_span_isMaximal_of_prime, Ideal.IsMaximal.eq_of_le, Ideal.IsPrime.ne_top'
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
rw : Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)
⊢ LE.le (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))

Tactic:
rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]

Premises used: Ideal.span_singleton_le_iff_mem, map_natCast, algebraMap_int_eq, Ideal.mem_comap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)

Tactic:
p_mem_span_zeta_sub_one p k hζ

Premises used: Set.Mem, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)

Tactic:
exact p_mem_span_zeta_sub_one p k hζ

Premises used: IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑

Tactic:
have := liesOver_span_zeta_sub_one p k hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
rw : p ^ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = HPow.hPow (β := ℕ) p 1
rw₁ : p ^ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p
rw₂ : (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1}) = p
rw₃ rw₄ : p = p
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1

Tactic:
rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, ← absNorm_eq_pow_inertiaDeg' _ hp.out,
    absNorm_span_zeta_sub_one]

Premises used: Nat.Prime.one_lt, Ideal.absNorm_eq_pow_inertiaDeg', pow_one, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Nat.pow_right_inj, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ IsGalois ℚ K

Tactic:
have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : IsGalois ℚ K
⊢ IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))

Tactic:
IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).symm _

Premises used: AlgEquiv.symm, Rat, IsGalois.of_equiv_equiv, Int, FractionRing.algEquiv, RingHom.ext, IsFractionRing.algEquiv_commutes, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : IsGalois ℚ K
⊢ IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))

Tactic:
refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).symm _

Premises used: IsGalois.of_equiv_equiv, RingHom.ext
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : IsGalois ℚ K
⊢ IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))

Tactic:
have : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K)) := by
    refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).symm _
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this_1 : IsGalois ℚ K
this : IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))
rw :
  ∏ i : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span (singleton (α := 𝓞 K) ((i : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K)) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
⊢ map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑 =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)

Tactic:
rw [map_span, Set.image_singleton, span_singleton_eq_span_singleton.mpr
    ((associated_norm_zeta_sub_one p k hζ).symm.map (algebraMap ℤ (𝓞 K))),
    ← Algebra.intNorm_eq_norm, Algebra.algebraMap_intNorm_of_isGalois, ← prod_span_singleton]

Premises used: Iff.mpr, Ideal.span_singleton_eq_span_singleton, Set.image_singleton, Algebra.algebraMap, Ideal.map_span, Int, Associated.symm, Algebra.intNorm_eq_norm, Algebra.algebraMap_intNorm_of_isGalois, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, Associated.map, Ideal.prod_span_singleton, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this_1 : IsGalois ℚ K
this : IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))
h : ∀ (σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K), span (singleton (α := 𝓞 K) ((σ : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K))
| ∏ i : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span (singleton (α := 𝓞 K) ((i : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K))

Tactic:
enter [2, σ]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this_1 : IsGalois ℚ K
this : IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))
h : ∀ (σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K), span {hζ.toInteger - 1}
| ∏ i : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span (singleton (α := 𝓞 K) ((i : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K))

Tactic:
enter [2, σ]
    rw [span_singleton_eq_span_singleton.mpr
      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this_1 : IsGalois ℚ K
this : IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))
conv_lhs :
  ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
⊢ ∏ i : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span (singleton (α := 𝓞 K) ((i : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K)) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)

Tactic:
conv_lhs =>
    enter [2, σ]
    rw [span_singleton_eq_span_singleton.mpr
      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this_1 : IsGalois ℚ K
this : IsGalois.{0, u_1} (FractionRing ℤ) (FractionRing (𝓞 K))
rw :
  HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Finset.card.{u_1} (α := 𝓞 K ≃ₐ[ℤ] 𝓞 K) Finset.univ) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
rw₁ :
  HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Fintype.card.{u_1} (𝓞 K ≃ₐ[ℤ] 𝓞 K)) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
rw₂ :
  HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Fintype.card.{u_1} Gal(K/ℚ)) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
rw₃ :
  HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Nat.card.{u_1} Gal(K/ℚ)) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
rw₄ rw₅ :
  HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K) =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
⊢ ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)

Tactic:
rw [Finset.prod_const, Finset.card_univ, ← Fintype.card_congr (galRestrict ℤ ℚ K (𝓞 K)).toEquiv,
    ← Nat.card_eq_fintype_card, IsGalois.card_aut_eq_finrank]

Premises used: Fintype.card_congr, Finset.card_univ, IsGalois.card_aut_eq_finrank, Rat, MulEquiv.toEquiv, Int, Finset.prod_const, galRestrict, NumberField.RingOfIntegers, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})

Tactic:
have h := isPrime_span_zeta_sub_one p k hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
rw : Ne.{u_1 + 1} (α := Ideal (𝓞 K)) (map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑) ⊥
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p ^ k * (p - 1)

Tactic:
rw [← Nat.totient_prime_pow_succ hp.out, ← finrank _ K,
    IsDedekindDomain.ramificationIdx_eq_multiplicity _ h, map_eq_span_zeta_sub_one_pow p k hζ,
    multiplicity_pow_self (span_zeta_sub_one_ne_bot p k hζ) (isUnit_iff.not.mpr h.ne_top)]

Premises used: Iff.mpr, Iff.not, multiplicity_pow_self, IsCyclotomicExtension.Rat.span_zeta_sub_one_ne_bot, Ideal.isUnit_iff, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsCyclotomicExtension.Rat.finrank, Nat.totient_prime_pow_succ, Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity, Ideal.IsPrime.ne_top, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
⊢ Ne (α := Ideal ℤ) 𝒑 ⊥

Tactic:
simpa using hp.out.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
⊢ Ne.{u_1 + 1} (α := Ideal (𝓞 K)) (map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑) ⊥

Tactic:
exact map_ne_bot_of_ne_bot <| by simpa using hp.out.ne_zero

Premises used: Ideal.map_ne_bot_of_ne_bot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
⊢ IsGalois ℚ K

Tactic:
have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
⊢ Ne (α := Ideal ℤ) 𝒑 ⊥

Tactic:
simpa using hp.out.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
⊢ Ne (α := Ideal ℤ) 𝒑 ⊥

Tactic:
have : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this_1 : IsGalois ℚ K
this : Ne (α := Ideal ℤ) 𝒑 ⊥
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) *
      (ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) * inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K)) =
    Nat.card.{u_1} Gal(K/ℚ)

Tactic:
have h_main := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn this (𝓞 K) Gal(K/ℚ)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this_1 : IsGalois ℚ K
this : Ne (α := Ideal ℤ) 𝒑 ⊥
h_main :
  Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) *
      (ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) * inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K)) =
    Nat.card.{u_1} Gal(K/ℚ)
⊢ IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))

Tactic:
have hζ := hK.zeta_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this_1 : IsGalois ℚ K
this : Ne (α := Ideal ℤ) 𝒑 ⊥
h_main :
  Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) *
      (ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) * inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K)) =
    Nat.card.{u_1} Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
⊢ LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑

Tactic:
have := liesOver_span_zeta_sub_one p k hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this_1 : IsGalois ℚ K
this_2 : Ne (α := Ideal ℤ) 𝒑 ⊥
h_main :
  Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) *
      (ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) * inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K)) =
    Nat.card.{u_1} Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
this : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
rwa :
  ∀
    (h_main :
      Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) * Module.finrank ℚ K = Module.finrank ℚ K)
    (this : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑), Module.finrank ℚ K ≠ 0
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1

Tactic:
rwa [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hζ.toInteger - 1}) Gal(K/ℚ),
    inertiaDegIn_eq_inertiaDeg 𝒑 (span {hζ.toInteger - 1}) Gal(K/ℚ),
    inertiaDeg_span_zeta_sub_one,
    ramificationIdx_span_zeta_sub_one, mul_one, ← Nat.totient_prime_pow_succ hp.out,
    ← finrank _ K, IsGaloisGroup.card_eq_finrank Gal(K/ℚ) ℚ K, Nat.mul_eq_right] at h_main

Premises used: Rat, Nat.mul_eq_right, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, AlgEquiv, IsCyclotomicExtension.Rat.finrank, Nat.totient_prime_pow_succ, mul_one, IsGaloisGroup.card_eq_finrank, Fact.out, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this_1 : IsGalois ℚ K
this_2 : Ne (α := Ideal ℤ) 𝒑 ⊥
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) * Module.finrank ℚ K = Module.finrank ℚ K
this : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
⊢ Module.finrank ℚ K ≠ 0

Tactic:
Module.finrank_pos.ne'

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this_1 : IsGalois ℚ K
this_2 : Ne (α := Ideal ℤ) 𝒑 ⊥
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) * Module.finrank ℚ K = Module.finrank ℚ K
this : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
⊢ Module.finrank ℚ K ≠ 0

Tactic:
exact Module.finrank_pos.ne'

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
⊢ Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) P

Tactic:
have : P ∈ primesOver 𝒑 (𝓞 K) := ⟨hP₁, hP₂⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
this : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) P
⊢ Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) (span {hζ.toInteger - 1})

Tactic:
have : span {hζ.toInteger - 1} ∈ primesOver 𝒑 (𝓞 K) :=
    ⟨isPrime_span_zeta_sub_one p k hζ, liesOver_span_zeta_sub_one p k hζ⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
this_1 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) P
this : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) (span {hζ.toInteger - 1})
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1

Tactic:
have := ncard_primesOver_of_prime_pow p k K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
this_1 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) P
this_2 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) (span {hζ.toInteger - 1})
this : Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
⊢ P = span {hζ.toInteger - 1}

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
rw :
  inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) ⋯) 1}) =
    1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ inertiaDeg (R := ℤ) 𝒑 P = 1

Tactic:
rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one]

Premises used: IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
rw :
  ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) ⋯) 1}) =
    p ^ k * (p - 1)
rw₁ rw₂ : p ^ k * (p - 1) = p ^ k * (p - 1)
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)

Tactic:
rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, ramificationIdx_span_zeta_sub_one]

Premises used: IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, IsCyclotomicExtension.zeta_spec, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one