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
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)
⊢ 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 hi₁ : (τ : (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)
Cleared hypotheses: hi
-- 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
⊢ 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)ˣ)
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ 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
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
⊢ 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)ˣ)
have 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)ˣ)
Tactic: apply SetLike.ext'
-- 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
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)ˣ)
have 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)ˣ)
Tactic: refine Set.eq_of_subset_of_card_le ?_ ?_
-- 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
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)ˣ)
⊢ (↑(((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)ˣ)
have 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)
Tactic: refine Set.eq_of_subset_of_card_le ?_ ?_
-- 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
this : IsGalois ℚ K
⊢ 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)
have hn₁ : ¬p ∣ n
Tactic: replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
-- 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_1 : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ 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)
have 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)
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]
-- 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_1 : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ 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)
have h : orderOf (ZMod.unitOfCoprime p hn_1) ≤ Nat.card.{u_1} (↑(↑(stabilizer Gal(K/ℚ) P) : Set Gal(K/ℚ)) : Type u_1)
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]
-- 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_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)
⊢ 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)
have h₁ : orderOf (ZMod.unitOfCoprime p hn_1) ≤ Nat.card.{u_1} ↥(stabilizer Gal(K/ℚ) P)
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]
-- 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_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)
⊢ 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)
have h₂ : orderOf (ZMod.unitOfCoprime p hn_1) ≤
  ramificationIdxIn.{0, u_1} (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K) * inertiaDegIn.{0, u_1} (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)
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]
-- 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_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)
⊢ 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)
have h₃ : orderOf (ZMod.unitOfCoprime p hn_1) ≤
  ramificationIdxIn.{0, u_1} (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K) * orderOf (G := ZMod n) (↑p : ZMod n)
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]
-- 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_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)
⊢ 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)
have h₄ : orderOf (ZMod.unitOfCoprime p hn_1) ≤ 1 * orderOf (G := ZMod n) (↑p : ZMod n)
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]
-- 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_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)
⊢ 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)
have h₅ : orderOf (ZMod.unitOfCoprime p hn_1) ≤ orderOf (G := ZMod n) (↑p : ZMod n)
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]
-- 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_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)
⊢ 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)
have 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)
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]
-- 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_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)
⊢ 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)
have h₇ : orderOf (↑(ZMod.unitOfCoprime p hn_1) : ZMod n) ≤ orderOf (G := ZMod n) (↑p : ZMod n)
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]
-- 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_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)
⊢ 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)
have h₈ : orderOf (G := ZMod n) (↑p : ZMod n) ≤ orderOf (G := ZMod n) (↑p : ZMod n)
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]