awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
rw :
  ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) ⋯) 1}) =
    p ^ k * (p - 1)
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have rw₁ : p ^ k * (p - 1) = p ^ k * (p - 1)
Tactic: rw [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    ramificationIdx_span_zeta_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
have rw : ∀ (hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K) {ζ : K} (hζ : IsPrimitiveRoot ζ p)
  (hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)), IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})
Tactic: rw [← pow_one p] at hK hζ
Cleared hypotheses: hK, ζ, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1
have rw : ∀ (hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K) {ζ : K} (hζ : IsPrimitiveRoot ζ p)
  (hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)), inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1
Tactic: rw [← pow_one p] at hK hζ
Cleared hypotheses: hK, ζ, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p - 1
have rw : ∀ (hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K) {ζ : K} (hζ : IsPrimitiveRoot ζ p)
  (hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)),
  ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p - 1
Tactic: rw [← pow_one p] at hK hζ
Cleared hypotheses: hK, ζ, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ_1.toInteger - 1}) = p - 1
have rw : HPow.hPow (β := ℕ) p 0 * (p - 1) = p - 1
Tactic: rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
rw : HPow.hPow (β := ℕ) p 0 * (p - 1) = p - 1
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ_1.toInteger - 1}) = p - 1
have rw₁ : 1 * (p - 1) = p - 1
Tactic: rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
rw : HPow.hPow (β := ℕ) p 0 * (p - 1) = p - 1
rw₁ : 1 * (p - 1) = p - 1
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ_1.toInteger - 1}) = p - 1
have rw₂ : p - 1 = p - 1
Tactic: rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1
have hK₁ : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
Tactic: rw [← pow_one p] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
⊢ P = span {hζ.toInteger - 1}
have rw : ∀ (hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K) {ζ : K} (hζ : IsPrimitiveRoot ζ p)
  (hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)) (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (A := ℤ) 𝒑],
  P = span {hζ.toInteger - 1}
Tactic: rw [← pow_one p] at hK hζ
Cleared hypotheses: hK, ζ, hζ, P, hP₁, hP₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
⊢ inertiaDeg (R := ℤ) 𝒑 P = 1
have rw : inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta p ℚ K) sorry) 1}) = 1
Tactic: rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
rw :
  inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta p ℚ K) ⋯) 1}) = 1
⊢ inertiaDeg (R := ℤ) 𝒑 P = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
⊢ ramificationIdx (R := ℤ) 𝒑 P = p - 1
have rw : ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta p ℚ K) sorry) 1}) =
  p - 1
Tactic: rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, ramificationIdx_span_zeta_sub_one']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
rw :
  ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta p ℚ K) ⋯) 1}) =
    p - 1
⊢ ramificationIdx (R := ℤ) 𝒑 P = p - 1
have rw₁ : p - 1 = p - 1
Tactic: rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, ramificationIdx_span_zeta_sub_one']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1
have hK₁ : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
Tactic: rw [← pow_one p] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p - 1
have hK₁ : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
Tactic: rw [← pow_one p] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p - 1
have rw : HPow.hPow (β := ℕ) p 0 * (p - 1) = p - 1
Tactic: rw [ramificationIdxIn_eq_of_prime_pow p 0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
rw : HPow.hPow (β := ℕ) p 0 * (p - 1) = p - 1
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p - 1
have rw₁ : 1 * (p - 1) = p - 1
Tactic: rw [ramificationIdxIn_eq_of_prime_pow p 0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
rw : HPow.hPow (β := ℕ) p 0 * (p - 1) = p - 1
rw₁ : 1 * (p - 1) = p - 1
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p - 1
have rw₂ : p - 1 = p - 1
Tactic: rw [ramificationIdxIn_eq_of_prime_pow p 0, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have hm₁ : p.Coprime m
Tactic: replace hm : p.Coprime m := hp.out.coprime_iff_not_dvd.mpr hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
⊢ ¬p ∣ exponent ζ
have rw : ¬p ∣ 1
Tactic: rw [exponent_eq_one_iff.mpr <| adjoin_singleton_eq_top (zeta_spec m ℚ K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have h₁ : ¬p ∣ exponent ζ
Tactic: have h₁ : ¬ p ∣ exponent ζ := by
    rw [exponent_eq_one_iff.mpr <| adjoin_singleton_eq_top (zeta_spec m ℚ K)]
    exact hp.out.not_dvd_one
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
h₁ : ¬p ∣ exponent ζ
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have h₂ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod ζ p)
  (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
          (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
        (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
          Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
    (ZMod p)[X])
Tactic: have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
h₁ : ¬p ∣ exponent ζ
h₂ :
  Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod ζ p)
    (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
            (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
            Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
      (ZMod p)[X])
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have h₃ : inertiaDeg.{0, u_1} (R := ℤ) (S := 𝓞 K) 𝒑
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod h₁) :
            (a : ↥(monicFactorsMod ζ p)) → (↑(𝒑.primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod ζ p) x)
            (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                      (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
                    (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
                  (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
                    Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
              (ZMod p)[X])
            h₂)) :
      Ideal (𝓞 K)) =
  natDegree (R := ZMod p)
    (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
            (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
            Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
      (ZMod p)[X])
Tactic: have h₃ := inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
h₁ : ¬p ∣ exponent ζ
h₂ :
  Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod ζ p)
    (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
            (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
            Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
      (ZMod p)[X])
h₃ :
  inertiaDeg.{0, u_1} (R := ℤ) (S := 𝓞 K) 𝒑
      (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod h₁) :
              (a : ↥(monicFactorsMod ζ p)) → (↑(𝒑.primesOver (𝓞 K)) : Type u_1))
            (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod ζ p) x)
              (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                        (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
                      (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
                    (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
                      Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
                (ZMod p)[X])
              h₂)) :
        Ideal (𝓞 K)) =
    natDegree (R := ZMod p)
      (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
              (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
        (ZMod p)[X])
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have h₄ : inertiaDeg (R := ℤ) 𝒑 P =
  natDegree (R := ZMod p)
    (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
            (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
            Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
      (ZMod p)[X])
Tactic: simp only [Subtype.coe_eta, Equiv.symm_apply_apply] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
h₁ : ¬p ∣ exponent ζ
h₂ :
  Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod ζ p)
    (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
            (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
            Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
      (ZMod p)[X])
h₃ :
  inertiaDeg (R := ℤ) 𝒑 P =
    natDegree (R := ZMod p)
      (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
              (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
        (ZMod p)[X])
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have h₄ : Irreducible (M := (ZMod p)[X])
    (↑(((primesOverSpanEquivMonicFactorsMod h₁ : (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
            (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
            Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
      (ZMod p)[X]) ∧
  Monic (R := ZMod p)
      (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
              (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
        (ZMod p)[X]) ∧
    Dvd.dvd (α := (ZMod p)[X])
      (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
              (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P sorry)) :
        (ZMod p)[X])
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
Tactic: rw [Multiset.mem_toFinset, Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))] at h₂
Cleared hypotheses: h₂, h₃
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
m p : ℕ
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 := ℤ) 𝒑
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible (M := (ZMod p)[X])
      (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
              (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
        (ZMod p)[X]) ∧
    Monic (R := ZMod p)
        (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                  (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
                (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
              (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
                Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
          (ZMod p)[X]) ∧
      Dvd.dvd (α := (ZMod p)[X])
        (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                  (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
                (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
              (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
                Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
          (ZMod p)[X])
        (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
h₃ :
  inertiaDeg (R := ℤ) 𝒑 P =
    natDegree (R := ZMod p)
      (↑(((primesOverSpanEquivMonicFactorsMod h₁ :
                (↑(primesOver (A := ℤ) 𝒑 (𝓞 K)) : Type u_1) ≃ ↥(monicFactorsMod ζ p)) :
              (a : (↑(𝒑.primesOver (𝓞 K)) : Type u_1)) → ↥(monicFactorsMod ζ p))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) 𝒑 (𝓞 K)) x) P ⋯)) :
        (ZMod p)[X])
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have rw : orderOf (ZMod.unitOfCoprime (HPow.hPow (β := ℕ) p 1) sorry) = orderOf (G := ZMod m) (↑p : ZMod m)
Tactic: rw [h₃, natDegree_of_dvd_cyclotomic_of_irreducible (by simp) hm (f := 1) _ h₂.1]