awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1
have rw₁ : p ^ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p
Tactic: rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, ← absNorm_eq_pow_inertiaDeg' _ hp.out,
    absNorm_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1
have rw₂ : (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1}) = p
Tactic: rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, ← absNorm_eq_pow_inertiaDeg' _ hp.out,
    absNorm_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1
have rw₃ : p = p
Tactic: rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, ← absNorm_eq_pow_inertiaDeg' _ hp.out,
    absNorm_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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))
⊢ map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑 =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑 =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
⊢ map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑 =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
| ∏ i : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span (singleton (α := 𝓞 K) ((i : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K))
have h : ∀ (σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K), span (singleton (α := 𝓞 K) ((σ : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K))
Tactic: enter [2, σ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
| ∏ i : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span (singleton (α := 𝓞 K) ((i : (a : 𝓞 K) → 𝓞 K) (hζ.toInteger - 1) : 𝓞 K))
have h : ∀ (σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K), span {hζ.toInteger - 1}
Tactic: enter [2, σ]
    rw [span_singleton_eq_span_singleton.mpr
      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
⊢ ∏ 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)
have conv_lhs : ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
⊢ ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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)
⊢ ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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)
⊢ ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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)
⊢ ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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)
⊢ ∏ σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K, span {hζ.toInteger - 1} =
    HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K)
have rw₄ : HPow.hPow (α := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (Module.finrank ℚ K) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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))
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p ^ k * (p - 1)
have h : IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
Tactic: have h := isPrime_span_zeta_sub_one p k hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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})
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p ^ k * (p - 1)
have rw : Ne.{u_1 + 1} (α := Ideal (𝓞 K)) (map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) 𝒑) ⊥
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
have this₁ : Ne (α := Ideal ℤ) 𝒑 ⊥
Tactic: have : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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)) = 1
have 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/ℚ)
Tactic: have h_main := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn this (𝓞 K) Gal(K/ℚ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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/ℚ)
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
have hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
Tactic: have hζ := hK.zeta_spec
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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))
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
have this₁ : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
Tactic: have := liesOver_span_zeta_sub_one p k hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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}) 𝒑
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
have 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
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
Cleared hypotheses: h_main, this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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 := ℤ) 𝒑
⊢ P = span {hζ.toInteger - 1}
have this : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) P
Tactic: have : P ∈ primesOver 𝒑 (𝓞 K) := ⟨hP₁, hP₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ P = span {hζ.toInteger - 1}
have this₁ : 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ζ⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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})
⊢ P = span {hζ.toInteger - 1}
have this₁ : Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
Tactic: have := ncard_primesOver_of_prime_pow p k K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 := ℤ) 𝒑
⊢ inertiaDeg (R := ℤ) 𝒑 P = 1
have rw : inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑
    (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) sorry) 1}) =
  1
Tactic: rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDeg (R := ℤ) 𝒑 P = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 := ℤ) 𝒑
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)
have rw : ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑
    (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) sorry) 1}) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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)
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)
have rw₁ : p ^ k * (p - 1) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1
have rw : inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑
    (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) sorry) 1}) =
  1
Tactic: rw [inertiaDegIn_eq_inertiaDeg 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    inertiaDeg_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
rw :
  inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) ⋯) 1}) =
    1
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [inertiaDegIn_eq_inertiaDeg 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    inertiaDeg_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have rw : ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑
    (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) sorry) 1}) =
  p ^ k * (p - 1)
Tactic: rw [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    ramificationIdx_span_zeta_sub_one]