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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
⊢ IsPrimitiveRoot (zeta n ℚ K) n

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec n ℚ K
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
⊢ CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p

Tactic:
have : CharP (ℤ ⧸ span {(p : ℤ)}) p := ringChar.of_eq <| Int.ringChar_idealQuot p
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
⊢ Finite.{u_1 + 1} (𝓞 K ⧸ P)

Tactic:
have : Finite (𝓞 K ⧸ P) := Ring.HasFiniteQuotients.finiteQuotient (NeZero.ne P)
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
obtain :
  ∀ (i : ℕ)
    (hi :
      ∀ (x : 𝓞 K ⧸ P),
        (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i),
    Membership.mem (α := (ZMod n)ˣ) (γ := Subgroup (ZMod n)ˣ) (Subgroup.zpowers (ZMod.unitOfCoprime p hn))
      (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ : (ZMod n)ˣ)
⊢ Membership.mem (α := (ZMod n)ˣ) (γ := Subgroup (ZMod n)ˣ) (Subgroup.zpowers (ZMod.unitOfCoprime p hn))
    (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ : (ZMod n)ˣ)

Tactic:
obtain ⟨i, hi⟩ := FiniteField.exists_forall_apply_eq_pow (ℤ ⧸ span {(p : ℤ)}) p (𝓞 K ⧸ P) τ

Premises used: FiniteField.exists_forall_apply_eq_pow, Int, Nat.cast, HasQuotient.Quotient, Ideal.span, Singleton.singleton, NumberField.RingOfIntegers
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
⊢ Membership.mem (α := (ZMod n)ˣ) (γ := Subgroup (ZMod n)ˣ) (Subgroup.zpowers (ZMod.unitOfCoprime p hn))
    (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ : (ZMod n)ˣ)

Tactic:
⟨i, ?_⟩

Premises used: Set.Mem, setOf, Nat.cast, Exists.intro, Set.range
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
refine :
  Eq (α := (ZMod n)ˣ) ((fun (x : ℤ) ↦ ZMod.unitOfCoprime p hn ^ x) (↑i : ℤ) : (ZMod n)ˣ)
    (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ : (ZMod n)ˣ)
⊢ Membership.mem (α := (ZMod n)ˣ) (γ := Subgroup (ZMod n)ˣ) (Subgroup.zpowers (ZMod.unitOfCoprime p hn))
    (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ : (ZMod n)ˣ)

Tactic:
refine ⟨i, ?_⟩
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)

Tactic:
simpa using IsMaximal.ne_top inferInstance

Premises used: inferInstance, Ideal.IsMaximal.ne_top
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
refine : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) n
⊢ IsPrimitiveRoot (M := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) n

Tactic:
refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
      (by simpa using IsMaximal.ne_top inferInstance) ?_

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, IsPrimitiveRoot.idealQuotient_mk
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
rw : (p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P).Coprime n
⊢ Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) n

Tactic:
rw [Ideal.absNorm_eq_pow_inertiaDeg' _ hp.out]

Premises used: Ideal.absNorm_eq_pow_inertiaDeg', 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 : p.Coprime n
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
⊢ (p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P).Coprime n

Tactic:
Nat.Coprime.pow_left _ hn

Premises used: Nat.Coprime.pow_left
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
⊢ (p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P).Coprime n

Tactic:
exact Nat.Coprime.pow_left _ hn

Premises used: Nat.Coprime.pow_left
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
⊢ IsPrimitiveRoot (M := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) n

Tactic:
have h₀ : IsPrimitiveRoot (Ideal.Quotient.mk P hζ.toInteger) n := by
    refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
      (by simpa using IsMaximal.ne_top inferInstance) ?_
    rw [Ideal.absNorm_eq_pow_inertiaDeg' _ hp.out]
    exact Nat.Coprime.pow_left _ 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 : p.Coprime n
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
h₀ : IsPrimitiveRoot (M := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) n
⊢ Eq (α := 𝓞 K ⧸ P)
    (((((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
                    (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
                  ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
                (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
              (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x)
                σ hσ) :
            Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
          (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
        ((algebraMap (𝓞 K ⧸ P) (𝓞 K ⧸ P) : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
          ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger)) :
      𝓞 K ⧸ P)
    ((algebraMap (𝓞 K ⧸ P) (𝓞 K ⧸ P) : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
        ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P)
          ((↑(Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ
                  hσ) :
              Gal(K/ℚ)) •
            hζ.toInteger)) :
      𝓞 K ⧸ P)

Tactic:
have h₁ := IsFractionRing.stabilizerHom_apply_apply_mk Gal(K/ℚ) (Ideal.span {(p : ℤ)}) P
      (ℤ ⧸ span {(p : ℤ)}) (𝓞 K ⧸ P) ⟨σ, hσ⟩ hζ.toInteger
-- 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
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
h₀ : IsPrimitiveRoot (M := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) n
h₁ :
  Eq (α := 𝓞 K ⧸ P)
    (((((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
                    (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
                  ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
                (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
              (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x)
                σ hσ) :
            Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
          (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
        ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger) :
      𝓞 K ⧸ P)
    ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) (σ • hζ.toInteger) : 𝓞 K ⧸ P)
⊢ (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger) =
    HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P)
      (Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i)

Tactic:
specialize hi (Ideal.Quotient.mk P hζ.toInteger)

Premises used: Ideal.Quotient.mk, IsPrimitiveRoot.toInteger, DFunLike.coe
-- 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
⊢ IsGalois ℚ K

Tactic:
have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
-- 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)ˣ)
⊢ Eq (α := Subgroup (ZMod n)ˣ)
    (((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)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)

Tactic:
apply SetLike.ext'

Premises used: SetLike.ext'
-- 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
⊢ (↑(((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:
Set.eq_of_subset_of_card_le ?_ ?_

Premises used: Set.eq_of_subset_of_card_le