awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst_6 : NeZero m
inst_7 : IsGalois.{0, u_1} ℚ ↥F
inst_8 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
simp_rw :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    m ∈ χ.conductorSet
simp_rw₁ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.FactorsThrough m
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.conductor ∣ m
have simp_rw₂ : Membership.mem (γ := Subgroup (DirichletCharacter R n))
    (((intermediateFieldEquivSubgroupChar n K R :
            OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
          (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
        F :
      Subgroup (DirichletCharacter R n))
    χ ↔
  (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
Tactic: simp_rw [← χ.mem_conductorSet_iff_conductor_dvd hdiv, χ.mem_conductorSet_iff,
    factorsThrough_iff_ker_unitsMap hdiv, mem_intermediateFieldEquivSubgroupChar_iff,
    SetLike.le_def, ← (galEquivZMod n K).forall_congr_right, MonoidHom.mem_ker,
    MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe, ← (galEquivZMod_restrictNormal_apply n K F hdiv _),
    EmbeddingLike.map_eq_one_iff, AlgEquiv.restrictNormal_eq_one_iff,
    IntermediateField.mem_fixingSubgroup_iff, Units.ext_iff, toUnitHom_eq, coe_equivToUnitHom,
    Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst_6 : NeZero m
inst_7 : IsGalois.{0, u_1} ℚ ↥F
inst_8 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
simp_rw :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    m ∈ χ.conductorSet
simp_rw₁ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.FactorsThrough m
simp_rw₂ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.conductor ∣ m
have simp_rw₃ : (∀ σ ∈ F.fixingSubgroup,
    Eq (α := R)
      ((χ : (a : ZMod n) → R)
          (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
        R)
      (1 : R)) ↔
  (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
Tactic: simp_rw [← χ.mem_conductorSet_iff_conductor_dvd hdiv, χ.mem_conductorSet_iff,
    factorsThrough_iff_ker_unitsMap hdiv, mem_intermediateFieldEquivSubgroupChar_iff,
    SetLike.le_def, ← (galEquivZMod n K).forall_congr_right, MonoidHom.mem_ker,
    MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe, ← (galEquivZMod_restrictNormal_apply n K F hdiv _),
    EmbeddingLike.map_eq_one_iff, AlgEquiv.restrictNormal_eq_one_iff,
    IntermediateField.mem_fixingSubgroup_iff, Units.ext_iff, toUnitHom_eq, coe_equivToUnitHom,
    Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst_6 : NeZero m
inst_7 : IsGalois.{0, u_1} ℚ ↥F
inst_8 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
simp_rw :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    m ∈ χ.conductorSet
simp_rw₁ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.FactorsThrough m
simp_rw₂ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
simp_rw₃ :
  (∀ σ ∈ F.fixingSubgroup,
      Eq (α := R)
        ((χ : (a : ZMod n) → R)
            (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
          R)
        (1 : R)) ↔
    (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.conductor ∣ m
have simp_rw₄ : (∀ σ ∈ F.fixingSubgroup,
    Eq (α := R)
      ((χ : (a : ZMod n) → R)
          (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
        R)
      (1 : R)) ↔
  ∀ ⦃x : (ZMod n)ˣ⦄, x ∈ (ZMod.unitsMap hdiv).ker → x ∈ (toUnitHom χ).ker
Tactic: simp_rw [← χ.mem_conductorSet_iff_conductor_dvd hdiv, χ.mem_conductorSet_iff,
    factorsThrough_iff_ker_unitsMap hdiv, mem_intermediateFieldEquivSubgroupChar_iff,
    SetLike.le_def, ← (galEquivZMod n K).forall_congr_right, MonoidHom.mem_ker,
    MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe, ← (galEquivZMod_restrictNormal_apply n K F hdiv _),
    EmbeddingLike.map_eq_one_iff, AlgEquiv.restrictNormal_eq_one_iff,
    IntermediateField.mem_fixingSubgroup_iff, Units.ext_iff, toUnitHom_eq, coe_equivToUnitHom,
    Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
⊢ IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
have rw : Prime (hζ.toInteger - 1)
Tactic: rw [Ideal.span_singleton_prime]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 : Prime (hζ.toInteger - 1)
⊢ IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
have rw₁ : hζ.toInteger - 1 ≠ 0
Tactic: rw [Ideal.span_singleton_prime]
-- 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))
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos : ∀ (h : p = 2), Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: by_cases h : p = 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))
pos : ∀ (h : p = 2), Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have neg : ∀ (h : ¬p = 2), Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: by_cases h : p = 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have hK₁ : IsCyclotomicExtension {2} ℚ K
Tactic: rw [h, zero_add, pow_one] at hK hζ
Cleared hypotheses: hK, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
hK₁ : IsCyclotomicExtension {2} ℚ K
hζ₁ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have hζ₂ : IsPrimitiveRoot ζ 2
Tactic: rw [h, zero_add, pow_one] at hK hζ
Cleared hypotheses: hK, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
hζ : IsPrimitiveRoot ζ 2
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos : Associated (M := ℤ) (-2) (↑p : ℤ)
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
hζ : IsPrimitiveRoot ζ 2
pos : Associated (M := ℤ) (-2) (↑p : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos₁ : Associated (M := ℤ) (-2) (↑2 : ℤ)
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
hζ : IsPrimitiveRoot ζ 2
pos : Associated (M := ℤ) (-2) (↑p : ℤ)
pos₁ : Associated (M := ℤ) (-2) (↑2 : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos₂ : Associated (M := ℤ) (-2) 2
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
hζ : IsPrimitiveRoot ζ 2
pos : Associated (M := ℤ) (-2) (↑p : ℤ)
pos₁ : Associated (M := ℤ) (-2) (↑2 : ℤ)
pos₂ : Associated (M := ℤ) (-2) 2
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos₃ : Associated (M := ℤ) 2 2
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {p ^ (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have hK₁ : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 2)} ℚ K
Tactic: rw [h, add_assoc, one_add_one_eq_two] at hK hζ
Cleared hypotheses: hK, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {p ^ (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hK₁ : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 2)} ℚ K
hζ₁ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have hζ₂ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 2))
Tactic: rw [h, add_assoc, one_add_one_eq_two] at hK hζ
Cleared hypotheses: hK, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 2)} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 2))
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos : Associated (M := ℤ) 2 (↑p : ℤ)
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 2)} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 2))
pos : Associated (M := ℤ) 2 (↑p : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos₁ : Associated (M := ℤ) 2 (↑2 : ℤ)
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 2)} ℚ K
hζ_1 : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 2))
pos : Associated (M := ℤ) 2 (↑p : ℤ)
pos₁ : Associated (M := ℤ) 2 (↑2 : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos₂ : Associated (M := ℤ) 2 2
Tactic: rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
-- 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 : p = 2
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos : ∀ [hK : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)),
  Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: cases k with
    | zero =>
      rw [h, zero_add, pow_one] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
    | succ n =>
      rw [h, add_assoc, one_add_one_eq_two] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
Cleared hypotheses: k, hK, 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 : p = 2
pos :
  ∀ [hK : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)),
    Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have pos₁ : ∀ (n : ℕ) [hK : IsCyclotomicExtension {p ^ (n + 1 + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))),
  Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: cases k with
    | zero =>
      rw [h, zero_add, pow_one] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
    | succ n =>
      rw [h, add_assoc, one_add_one_eq_two] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
Cleared hypotheses: k, hK, 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 : ¬p = 2
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have neg : Associated (M := ℤ) (↑p : ℤ) (↑p : ℤ)
Tactic: rw [hζ.norm_toInteger_sub_one_of_prime_ne_two 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))
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)
have h : p = (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})
Tactic: convert! Ideal.absNorm_mem _
-- 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 : p = (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)
have convert_3 : Nontrivial.{u_1} (𝓞 K)
Tactic: convert! Ideal.absNorm_mem _
-- 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 : p = (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})
convert_3 : Nontrivial.{u_1} (𝓞 K)
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)
have convert_4 : IsDedekindDomain.{u_1} (𝓞 K)
Tactic: convert! Ideal.absNorm_mem _
-- 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 : p = (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})
convert_3 : Nontrivial.{u_1} (𝓞 K)
convert_4 : IsDedekindDomain.{u_1} (𝓞 K)
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)
have convert_5 : Module.Free.{0, u_1} ℤ (𝓞 K)
Tactic: convert! Ideal.absNorm_mem _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
⊢ LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
have rw : Eq (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))
Tactic: rw [liesOver_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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}))
have refine : LE.le (α := 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' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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))
⊢ LE.le (α := Ideal ℤ) 𝒑 (under ℤ (B := 𝓞 K) (span {hζ.toInteger - 1}))
have rw : Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)
Tactic: rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]
-- 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))
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 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
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : LiesOver (A := ℤ) (B := 𝓞 K) (span {hζ.toInteger - 1}) 𝒑
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1
have rw : p ^ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = HPow.hPow (β := ℕ) p 1
Tactic: rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, ← absNorm_eq_pow_inertiaDeg' _ hp.out,
    absNorm_span_zeta_sub_one]