awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
rw :
  multiplicity (α := (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 ℤ ζ)) =
    1
⊢ ramificationIdx (R := ℤ) 𝒑 P = 1

Tactic:
rw [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 ∣ 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ multiplicity (α := (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 ℤ ζ)) =
    1

Tactic:
multiplicity_eq_of_emultiplicity_eq_some (le_antisymm ?_ ?_)

Premises used: le_antisymm, multiplicity_eq_of_emultiplicity_eq_some
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ ¬IsUnit (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])

Tactic:
isUnit_iff_degree_eq_zero.not.mpr (Irreducible.degree_pos h₂.1).ne'

Premises used: Iff.mpr, Iff.not, Irreducible.degree_pos, LT.lt.ne', And.left, Polynomial.isUnit_iff_degree_eq_zero
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ ¬IsUnit (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])

Tactic:
exact isUnit_iff_degree_eq_zero.not.mpr (Irreducible.degree_pos h₂.1).ne'

Premises used: Iff.mpr, Iff.not, Irreducible.degree_pos, LT.lt.ne', And.left, Polynomial.isUnit_iff_degree_eq_zero
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ Separable (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))

Tactic:
(zeta_spec m ℚ K).toInteger_isPrimitiveRoot.separable_minpoly_mod hm

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, Rat, IsPrimitiveRoot.separable_minpoly_mod, IsCyclotomicExtension.zeta_spec
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ Separable (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))

Tactic:
exact (zeta_spec m ℚ K).toInteger_isPrimitiveRoot.separable_minpoly_mod hm

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, Rat, IsPrimitiveRoot.separable_minpoly_mod, IsCyclotomicExtension.zeta_spec
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ 1 ≤
    emultiplicity (α := (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:
Order.one_le_iff_pos.mpr <| emultiplicity_pos_of_dvd h₂.2.2

Premises used: Iff.mpr, emultiplicity_pos_of_dvd, And.right, Order.one_le_iff_pos
-- 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
ζ : 𝓞 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₃ :
  ramificationIdx (R := ℤ) 𝒑 P =
    multiplicity (α := (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 ℤ ζ))
⊢ 1 ≤
    emultiplicity (α := (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:
exact Order.one_le_iff_pos.mpr <| emultiplicity_pos_of_dvd h₂.2.2

Premises used: Iff.mpr, emultiplicity_pos_of_dvd, And.right, Order.one_le_iff_pos
-- 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
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ IsGalois ℚ K

Tactic:
have : IsGalois ℚ K := isGalois {m} ℚ K
-- 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
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
obtain :
  ∀ (P : Ideal (𝓞 K)),
    P.IsPrime → P.LiesOver (A := ℤ) 𝒑 → inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m)
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m)

Tactic:
obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)
-- 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
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left : P.IsPrime
right : P.LiesOver (A := ℤ) 𝒑
rw : inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
rw₁ rw₂ : orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m)
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m)

Tactic:
rw [inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDeg_eq_of_not_dvd p K P hm]

Premises used: IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd
-- 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
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
obtain : ∀ (P : Ideal (𝓞 K)), P.IsPrime → P.LiesOver (A := ℤ) 𝒑 → ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1

Tactic:
obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)