awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
rw :
  inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) ⋯) 1}) =
    1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1

Tactic:
rw [inertiaDegIn_eq_inertiaDeg 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    inertiaDeg_span_zeta_sub_one]

Premises used: IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
rw :
  ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑
      (span {HSub.hSub (α := 𝓞 K) (IsPrimitiveRoot.toInteger (ζ := zeta (p ^ (k + 1)) ℚ K) ⋯) 1}) =
    p ^ k * (p - 1)
rw₁ rw₂ : p ^ k * (p - 1) = p ^ k * (p - 1)
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    ramificationIdx_span_zeta_sub_one]

Premises used: IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
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})
⊢ IsPrime (α := 𝓞 K) (span {hζ.toInteger - 1})

Tactic:
rw [← pow_one p] at hK hζ

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
⊢ IsPrime (α := 𝓞 K) (span {hζ_1.toInteger - 1})

Tactic:
isPrime_span_zeta_sub_one p 0 hζ

Premises used: IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
⊢ IsPrime (α := 𝓞 K) (span {hζ_1.toInteger - 1})

Tactic:
exact isPrime_span_zeta_sub_one p 0 hζ

Premises used: IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
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
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = 1

Tactic:
rw [← pow_one p] at hK hζ

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ_1.toInteger - 1}) = 1

Tactic:
inertiaDeg_span_zeta_sub_one p 0 hζ

Premises used: IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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)
⊢ inertiaDeg (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ_1.toInteger - 1}) = 1

Tactic:
exact inertiaDeg_span_zeta_sub_one p 0 hζ

Premises used: IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
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
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ.toInteger - 1}) = p - 1

Tactic:
rw [← pow_one p] at hK hζ

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
rw₂ rw₃ : p - 1 = p - 1
⊢ ramificationIdx (R := ℤ) (S := 𝓞 K) 𝒑 (span {hζ_1.toInteger - 1}) = p - 1

Tactic:
rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]

Premises used: pow_zero, OfNat.ofNat, one_mul, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K

Tactic:
rw [← pow_one p] at hK

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1

Tactic:
ncard_primesOver_of_prime_pow p 0 K

Premises used: IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
⊢ Set.ncard.{u_1} (α := Ideal (𝓞 K)) (primesOver (A := ℤ) 𝒑 (𝓞 K)) = 1

Tactic:
exact ncard_primesOver_of_prime_pow p 0 K

Premises used: IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 := ℤ) 𝒑
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}
⊢ P = span {hζ.toInteger - 1}

Tactic:
rw [← pow_one p] at hK hζ

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
ζ : K
hζ_1 : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
⊢ P = span {hζ_1.toInteger - 1}

Tactic:
eq_span_zeta_sub_one_of_liesOver p 0 K hζ P

Premises used: IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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)
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
⊢ P = span {hζ_1.toInteger - 1}

Tactic:
exact eq_span_zeta_sub_one_of_liesOver p 0 K hζ P

Premises used: IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ inertiaDeg (R := ℤ) 𝒑 P = 1

Tactic:
rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one']

Premises used: IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
rw₁ rw₂ : p - 1 = p - 1
⊢ ramificationIdx (R := ℤ) 𝒑 P = p - 1

Tactic:
rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, ramificationIdx_span_zeta_sub_one']

Premises used: IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1

Tactic:
inertiaDegIn_eq_of_prime_pow p 0 K

Premises used: IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1

Tactic:
exact inertiaDegIn_eq_of_prime_pow p 0 K

Premises used: IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
rw₂ rw₃ : p - 1 = p - 1
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p - 1

Tactic:
rw [ramificationIdxIn_eq_of_prime_pow p 0, pow_zero, one_mul]

Premises used: pow_zero, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, OfNat.ofNat, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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
⊢ p.Coprime m

Tactic:
replace hm : p.Coprime m := hp.out.coprime_iff_not_dvd.mpr hm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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) ⋯
rw : ¬p ∣ 1
⊢ ¬p ∣ exponent ζ

Tactic:
rw [exponent_eq_one_iff.mpr <| adjoin_singleton_eq_top (zeta_spec m ℚ K)]

Premises used: Iff.mpr, Rat, RingOfIntegers.exponent_eq_one_iff, IsCyclotomicExtension.zeta_spec, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 ∣ 1

Tactic:
hp.out.not_dvd_one

Premises used: Nat.Prime.not_dvd_one, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 ∣ 1

Tactic:
exact hp.out.not_dvd_one

Premises used: Nat.Prime.not_dvd_one, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 ζ

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
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 ζ
⊢ 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])

Tactic:
have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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.{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])

Tactic:
have h₃ := inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' h₁ h₂
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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 =
    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])

Tactic:
simp only [Subtype.coe_eta, Equiv.symm_apply_apply] at h₃

Premises used: Equiv.symm_apply_apply, Subtype.coe_eta
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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])
⊢ 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 ℤ ζ))

Tactic:
rw [Multiset.mem_toFinset, Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))] at h₂

Premises used: minpoly.monic, Polynomial.map_monic_ne_zero, Polynomial.mem_normalizedFactors_iff, NumberField.RingOfIntegers.isIntegral, Multiset.mem_toFinset
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
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])
⊢ Fintype.card (ZMod p) = HPow.hPow (β := ℕ) p 1

Tactic:
simp