awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
⊢ Eq (α := (ZMod m)ˣ)
    (((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F) : (ZMod m)ˣ)
    ((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
      (ZMod m)ˣ)
have hζ : IsPrimitiveRoot (zeta m ℚ F) m
Tactic: have hζ := IsCyclotomicExtension.zeta_spec m ℚ F
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this :
  ζ ^
      ZMod.val (n := m)
        (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m) =
    ζ ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
⊢ Eq (α := (ZMod m)ˣ)
    (((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F) : (ZMod m)ˣ)
    ((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
      (ZMod m)ˣ)
have this₁ : Eq (α := ZMod m)
  (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m)
  (ZMod.cast (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n))
Tactic: rw [(hζ.isOfFinOrder (NeZero.ne _)).pow_inj_mod, ← hζ.eq_orderOf,
      ← ZMod.natCast_eq_natCast_iff', ZMod.natCast_val, ZMod.natCast_val, ZMod.cast_id] at this
Cleared hypotheses: this
-- 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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this :
  Eq (α := ZMod m)
    (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m)
    (ZMod.cast (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n))
⊢ Eq (α := (ZMod m)ˣ)
    (((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F) : (ZMod m)ˣ)
    ((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
      (ZMod m)ˣ)
have rwa : Eq (α := ZMod m)
  (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m)
  (↑((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ)) :
    ZMod m)
Tactic: rwa [Units.ext_iff]
-- 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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ Eq (α := (ZMod m)ˣ)
    (((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F) : (ZMod m)ˣ)
    ((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
      (ZMod m)ˣ)
have suffices : ζ ^
    ZMod.val (n := m)
      (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m) =
  ζ ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
Tactic: suffices ζ ^ (galEquivZMod m F (σ.restrictNormal F)).val.val = ζ ^ (galEquivZMod n K σ).val.val by
    rw [(hζ.isOfFinOrder (NeZero.ne _)).pow_inj_mod, ← hζ.eq_orderOf,
      ← ZMod.natCast_eq_natCast_iff', ZMod.natCast_val, ZMod.natCast_val, ZMod.cast_id] at this
    rwa [Units.ext_iff]
-- 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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ ζ ^
      ZMod.val (n := m)
        (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m) =
    ζ ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have a : Eq.{u_1 + 1} (α := K)
  ((algebraMap F K : (a : F) → K)
      (ζ ^
        ZMod.val (n := m)
          (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) :
            ZMod m)) :
    K)
  ((algebraMap F K : (a : F) → K)
      (ζ ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
    K)
Tactic: apply FaithfulSMul.algebraMap_injective F K
-- 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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ Eq.{u_1 + 1} (α := K)
    ((algebraMap F K : (a : F) → K)
        (ζ ^
          ZMod.val (n := m)
            (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) :
              ZMod m)) :
      K)
    ((algebraMap F K : (a : F) → K)
        (ζ ^
          ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
      K)
have a : HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) ζ : K) n = 1
Tactic: rw [map_pow, map_pow, ← galEquivZMod_apply_of_pow_eq, ← AlgEquiv.restrictNormal_commutes,
      galEquivZMod_apply_of_pow_eq m _ _ hζ.pow_eq_one, map_pow]
-- 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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) ζ : K) n = 1
have a : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) (ζ ^ n) : K) (1 : K)
Tactic: rw [← map_pow, (hζ.pow_eq_one_iff_dvd _).mpr h, map_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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
a : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) (ζ ^ n) : K) (1 : K)
⊢ HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) ζ : K) n = 1
have a₁ : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) 1 : K) (1 : K)
Tactic: rw [← map_pow, (hζ.pow_eq_one_iff_dvd _).mpr h, map_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
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
a : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) (ζ ^ n) : K) (1 : K)
a₁ : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) 1 : K) (1 : K)
⊢ HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) ζ : K) n = 1
have a₂ : Eq.{u_1 + 1} (α := K) 1 1
Tactic: rw [← map_pow, (hζ.pow_eq_one_iff_dvd _).mpr h, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
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) σ
⊢ 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)ˣ)
have hζ : IsPrimitiveRoot (zeta n ℚ K) n
Tactic: have hζ := IsCyclotomicExtension.zeta_spec n ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
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σ)
⊢ 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)ˣ)
have this : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
Tactic: have : CharP (ℤ ⧸ span {(p : ℤ)}) p := ringChar.of_eq <| Int.ringChar_idealQuot p
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
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
⊢ 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)ˣ)
have this₁ : Finite.{u_1 + 1} (𝓞 K ⧸ P)
Tactic: have : Finite (𝓞 K ⧸ P) := Ring.HasFiniteQuotients.finiteQuotient (NeZero.ne P)
-- 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
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)
⊢ 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)ˣ)
have 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)ˣ)
Tactic: obtain ⟨i, hi⟩ := FiniteField.exists_forall_apply_eq_pow (ℤ ⧸ span {(p : ℤ)}) p (𝓞 K ⧸ P) τ
-- 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
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)ˣ)
have 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)ˣ)
Tactic: refine ⟨i, ?_⟩
-- 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
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
have refine : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) n
Tactic: refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
      (by simpa using IsMaximal.ne_top inferInstance) ?_
-- 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
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
⊢ Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) n
have rw : (p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P).Coprime n
Tactic: rw [Ideal.absNorm_eq_pow_inertiaDeg' _ hp.out]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
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
⊢ 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)ˣ)
have h₀ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
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 (α := (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)ˣ)
have 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)
      ((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