awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
this : IsGalois ℚ K
h :
  (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            (stabilizer Gal(K/ℚ) P) :
          Subgroup (ZMod n)ˣ) :
      Set (ZMod n)ˣ) ⊆
    (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
h₁ :
  Fintype.card (↑(↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ) : Type) ≤
    Fintype.card
      (↑(↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                    (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
                  (stabilizer Gal(K/ℚ) P) :
                Subgroup (ZMod n)ˣ) :
            Set (ZMod n)ˣ) :
        Type)
⊢ (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            (stabilizer Gal(K/ℚ) P) :
          Subgroup (ZMod n)ˣ) :
      Set (ZMod n)ˣ) =
    (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)

Tactic:
refine Set.eq_of_subset_of_card_le ?_ ?_

Premises used: Set.eq_of_subset_of_card_le
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
this : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : σ ∈ (↑(stabilizer Gal(K/ℚ) P) : Set Gal(K/ℚ))
⊢ Membership.mem (α := (ZMod n)ˣ) (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
    ((((↑(galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) →* (ZMod n)ˣ) : Gal(K/ℚ) →* (ZMod n)ˣ) :
          (a : Gal(K/ℚ)) → (ZMod n)ˣ)
        σ :
      (ZMod n)ˣ)

Tactic:
mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ

Premises used: Set.Mem, IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizer
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
this : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : σ ∈ (↑(stabilizer Gal(K/ℚ) P) : Set Gal(K/ℚ))
⊢ Membership.mem (α := (ZMod n)ˣ) (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
    ((((↑(galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) →* (ZMod n)ˣ) : Gal(K/ℚ) →* (ZMod n)ˣ) :
          (a : Gal(K/ℚ)) → (ZMod n)ˣ)
        σ :
      (ZMod n)ˣ)

Tactic:
exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ

Premises used: IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizer
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
this : IsGalois ℚ K
⊢ ¬p ∣ n

Tactic:
replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn_1 : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
h :
  orderOf (ZMod.unitOfCoprime p hn_1) ≤
    Nat.card
      (↑((⇑(↑(galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) →* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) ''
            (↑(stabilizer Gal(K/ℚ) P) : Set Gal(K/ℚ))) :
        Type)
⊢ Fintype.card (↑(↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn_1)) : Set (ZMod n)ˣ) : Type) ≤
    Fintype.card
      (↑(↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                    (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
                  (stabilizer Gal(K/ℚ) P) :
                Subgroup (ZMod n)ˣ) :
            Set (ZMod n)ˣ) :
        Type)

Tactic:
rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]

Premises used: SetLike.coe_sort_coe, MulEquiv.mapSubgroup_apply, Subgroup.coe_map, Nat.card_zpowers, Fintype.card_eq_nat_card
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn_1 : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ Ne (α := Ideal ℤ) (span {(↑p : ℤ)}) ⊥

Tactic:
simp [hp.out.ne_zero]

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn_1 : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
h : orderOf (ZMod.unitOfCoprime p hn_1) ≤ Nat.card.{u_1} (↑(↑(stabilizer Gal(K/ℚ) P) : Set Gal(K/ℚ)) : Type u_1)
h₁ : orderOf (ZMod.unitOfCoprime p hn_1) ≤ Nat.card.{u_1} ↥(stabilizer Gal(K/ℚ) P)
h₂ :
  orderOf (ZMod.unitOfCoprime p hn_1) ≤
    ramificationIdxIn.{0, u_1} (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K) * inertiaDegIn.{0, u_1} (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)
h₃ :
  orderOf (ZMod.unitOfCoprime p hn_1) ≤
    ramificationIdxIn.{0, u_1} (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K) * orderOf (G := ZMod n) (↑p : ZMod n)
h₄ : orderOf (ZMod.unitOfCoprime p hn_1) ≤ 1 * orderOf (G := ZMod n) (↑p : ZMod n)
h₅ : orderOf (ZMod.unitOfCoprime p hn_1) ≤ orderOf (G := ZMod n) (↑p : ZMod n)
h₆ :
  orderOf (G := ZMod n) ((Units.coeHom (ZMod n) : (a : (ZMod n)ˣ) → ZMod n) (ZMod.unitOfCoprime p hn_1) : ZMod n) ≤
    orderOf (G := ZMod n) (↑p : ZMod n)
h₇ : orderOf (↑(ZMod.unitOfCoprime p hn_1) : ZMod n) ≤ orderOf (G := ZMod n) (↑p : ZMod n)
h₈ h₉ : orderOf (G := ZMod n) (↑p : ZMod n) ≤ orderOf (G := ZMod n) (↑p : ZMod n)
⊢ orderOf (ZMod.unitOfCoprime p hn_1) ≤
    Nat.card
      (↑((⇑(MulEquiv.toEquiv (galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) :
              (a : Gal(K/ℚ)) → (ZMod n)ˣ) ''
            (↑(stabilizer Gal(K/ℚ) P) : Set Gal(K/ℚ))) :
        Type)

Tactic:
rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)})
      (by simp [hp.out.ne_zero]), inertiaDegIn_eq_of_not_dvd p K hn,
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime]

Premises used: SetLike.coe_sort_coe, Ideal.card_stabilizer_eq, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, Nat.cast, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, Nat.card_image_equiv, Units.coeHom_apply, Ideal.span, ZMod.coe_unitOfCoprime, Singleton.singleton, orderOf_injective, Units.coeHom_injective, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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)ˣ)
χ : DirichletCharacter R n
H : Subgroup Gal(K/ℚ)
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      ((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
          (((subgroupGalEquivSubgroupChar n K R :
                OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ)) (Subgroup (DirichletCharacter R n))ᵒᵈ) :
              (a : Subgroup Gal(K/ℚ)) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
            H) :
        Subgroup (DirichletCharacter R n))
      χ ↔
    ∀ σ ∈ H,
      Eq (α := R)
        ((χ : (a : ZMod n) → R)
            (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
          R)
        (1 : R)

Tactic:
simp [subgroupGalEquivSubgroupChar]

Premises used: IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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)ˣ)
σ : Gal(K/ℚ)
Y : Subgroup (DirichletCharacter R n)
⊢ Membership.mem (γ := Subgroup Gal(K/ℚ))
      (((OrderIso.symm (subgroupGalEquivSubgroupChar n K R) :
              OrderIso.{u_2, u_1} (Subgroup (DirichletCharacter R n))ᵒᵈ (Subgroup Gal(K/ℚ))) :
            (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup Gal(K/ℚ))
          ((OrderDual.toDual : (a : Subgroup (DirichletCharacter R n)) → (Subgroup (DirichletCharacter R n))ᵒᵈ) Y) :
        Subgroup Gal(K/ℚ))
      σ ↔
    ∀ χ ∈ Y,
      Eq (α := R)
        ((χ : (a : ZMod n) → R)
            (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
          R)
        (1 : R)

Tactic:
simp only [subgroupGalEquivSubgroupChar, OrderIso.symm_trans_apply, MulEquiv.symm_mapSubgroup,
    MulEquiv.coe_mapSubgroup, Subgroup.mem_map_equiv, MulEquiv.symm_symm,
    mem_subgroupOrderIsoSubgroupMulChar_symm_iff]

Premises used: OrderIso.symm_trans_apply, IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar, Subgroup.mem_map_equiv, MulEquiv.coe_mapSubgroup, MulChar.mem_subgroupOrderIsoSubgroupMulChar_symm_iff, MulEquiv.symm_symm, MulEquiv.symm_mapSubgroup
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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 : IsMulCommutative.{u_1} Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
rw :
  Nat.card
      (HasQuotient.Quotient (ZMod n)ˣ (B := Subgroup (ZMod n)ˣ)
        (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            H :
          Subgroup (ZMod n)ˣ)) =
    Nat.card.{u_1} (Gal(K/ℚ) ⧸ H)
⊢ Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            (((subgroupGalEquivSubgroupChar n K R :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ)) (Subgroup (DirichletCharacter R n))ᵒᵈ) :
                (a : Subgroup Gal(K/ℚ)) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              H) :
          Subgroup (DirichletCharacter R n)) =
    Nat.card.{u_1} (Gal(K/ℚ) ⧸ H)

Tactic:
rw [subgroupGalEquivSubgroupChar, OrderIso.trans_apply, card_subgroupOrderIsoSubgroupMulChar]

Premises used: IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar, OrderIso.trans_apply, MulChar.card_subgroupOrderIsoSubgroupMulChar
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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 : IsMulCommutative.{u_1} Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card
      (HasQuotient.Quotient (ZMod n)ˣ (B := Subgroup (ZMod n)ˣ)
        (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            H :
          Subgroup (ZMod n)ˣ)) =
    Nat.card.{u_1} (Gal(K/ℚ) ⧸ H)

Tactic:
Nat.card_congr (QuotientGroup.congr _ _ (galEquivZMod n K) rfl).symm.toEquiv

Premises used: IsCyclotomicExtension.Rat.galEquivZMod, MulEquiv.toEquiv, Nat.card_congr, QuotientGroup.congr, MulEquiv.symm, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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 : IsMulCommutative.{u_1} Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card
      (HasQuotient.Quotient (ZMod n)ˣ (B := Subgroup (ZMod n)ˣ)
        (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            H :
          Subgroup (ZMod n)ˣ)) =
    Nat.card.{u_1} (Gal(K/ℚ) ⧸ H)

Tactic:
exact Nat.card_congr (QuotientGroup.congr _ _ (galEquivZMod n K) rfl).symm.toEquiv

Premises used: IsCyclotomicExtension.Rat.galEquivZMod, MulEquiv.toEquiv, Nat.card_congr, QuotientGroup.congr, MulEquiv.symm, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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
χ : DirichletCharacter R n
⊢ 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))
      χ ↔
    ∀ σ ∈ 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)

Tactic:
simp [intermediateFieldEquivSubgroupChar]

Premises used: IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar
-- 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 : Prime (hζ.toInteger - 1)
rw₁ : hζ.toInteger - 1 ≠ 0
⊢ IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})

Tactic:
rw [Ideal.span_singleton_prime]

Premises used: Ideal.span_singleton_prime
-- 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))
⊢ Prime (hζ.toInteger - 1)

Tactic:
hζ.zeta_sub_one_prime

Premises used: IsPrimitiveRoot.zeta_sub_one_prime
-- 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))
⊢ Prime (hζ.toInteger - 1)

Tactic:
exact hζ.zeta_sub_one_prime

Premises used: IsPrimitiveRoot.zeta_sub_one_prime
-- 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))
⊢ hζ.toInteger - 1 ≠ 0

Tactic:
Prime.ne_zero hζ.zeta_sub_one_prime

Premises used: Prime.ne_zero, IsPrimitiveRoot.zeta_sub_one_prime
-- 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))
⊢ hζ.toInteger - 1 ≠ 0

Tactic:
exact Prime.ne_zero hζ.zeta_sub_one_prime

Premises used: Prime.ne_zero, IsPrimitiveRoot.zeta_sub_one_prime
-- 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))
pos : ∀ (h : p = 2), Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
neg : ∀ (h : ¬p = 2), Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
by_cases h : p = 2
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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)
⊢ IsCyclotomicExtension {2} ℚ K

Tactic:
rw [h, zero_add, pow_one] at hK hζ

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
rw [h, zero_add, pow_one] at hK hζ

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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)
⊢ IsPrimitiveRoot ζ 2

Tactic:
rw [h, zero_add, pow_one] at hK hζ

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
pos₃ pos₄ : Associated (M := ℤ) 2 2
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, Int.ofNat_two, Associated.neg_left_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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))
⊢ IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 2)} ℚ K

Tactic:
rw [h, add_assoc, one_add_one_eq_two] at hK hζ

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
⊢ IsPrimitiveRoot ζ (p ^ (n + 1 + 1))

Tactic:
rw [h, add_assoc, one_add_one_eq_two] at hK hζ

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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))
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 2))

Tactic:
rw [h, add_assoc, one_add_one_eq_two] at hK hζ

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 : ℤ)
pos₂ pos₃ : Associated (M := ℤ) 2 2
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, Int.ofNat_two
-- 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 : 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 : ℤ) : ℤ)
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 : ℤ) : ℤ)
⊢ 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]

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, add_assoc, Int.ofNat_two, zero_add, one_add_one_eq_two, pow_one, Associated.neg_left_iff
-- 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 : ¬p = 2
neg neg₁ : Associated (M := ℤ) (↑p : ℤ) (↑p : ℤ)
⊢ Associated (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
rw [hζ.norm_toInteger_sub_one_of_prime_ne_two h]

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two
-- 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))
⊢ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1}) = p

Tactic:
simpa using congr_arg absNorm <|
    span_singleton_eq_span_singleton.mpr <| associated_norm_zeta_sub_one p k hζ

Premises used: Iff.mpr, Ideal.span_singleton_eq_span_singleton, Ideal.absNorm, congr_arg, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, DFunLike.coe
-- 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))
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1})
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})) : 𝓞 K)

Tactic:
Ideal.absNorm_mem _

Premises used: Ideal.absNorm_mem
-- 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 : p = (absNorm : (a : Ideal (𝓞 K)) → ℕ) (span {hζ.toInteger - 1})
convert_3 : Nontrivial.{u_1} (𝓞 K)
convert_4 : IsDedekindDomain.{u_1} (𝓞 K)
convert_5 : Module.Free.{0, u_1} ℤ (𝓞 K)
⊢ Membership.mem (γ := Ideal (𝓞 K)) (span {hζ.toInteger - 1}) (↑p : 𝓞 K)

Tactic:
convert! Ideal.absNorm_mem _

Premises used: Ideal.absNorm_mem