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.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])
rw : orderOf (ZMod.unitOfCoprime (HPow.hPow (β := ℕ) p 1) ⋯) = orderOf (G := ZMod m) (↑p : ZMod m)
rw₁ :
  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])
    (cyclotomic m (ZMod p))
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)

Tactic:
rw [h₃, natDegree_of_dvd_cyclotomic_of_irreducible (by simp) hm (f := 1) _ h₂.1]

Premises used: Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, And.left
-- 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])
⊢ orderOf (ZMod.unitOfCoprime (HPow.hPow (β := ℕ) p 1) ⋯) = orderOf (G := ZMod m) (↑p : ZMod m)

Tactic:
simpa using (orderOf_injective _ Units.coeHom_injective (ZMod.unitOfCoprime p hm)).symm

Premises used: ZMod.unitOfCoprime, Eq.symm, orderOf_injective, Units.coeHom_injective
-- 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])
⊢ 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])
    (cyclotomic m (ZMod p))

Tactic:
dvd_trans h₂.2.2 ?_

Premises used: dvd_trans, And.right
-- 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])
refine : Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)) (cyclotomic m (ZMod p))
⊢ 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])
    (cyclotomic m (ZMod p))

Tactic:
refine dvd_trans h₂.2.2 ?_

Premises used: dvd_trans, And.right
-- 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])
⊢ Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (↑ζ : K)))
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (↑(IsPrimitiveRoot.toInteger (ζ := zeta m ℚ K) ⋯) : K)))

Tactic:
simp [ζ]
-- 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) ⋯
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 ∣ 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 ∣ 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 ∣ 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 ∣ 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 ∣ 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])
⊢ ramificationIdx.{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)) =
    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 ℤ ζ))

Tactic:
have h₃ := ramificationIdx_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 ∣ 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₃ :
  ramificationIdx.{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)) =
    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 ℤ ζ))
⊢ 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 ℤ ζ))

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 ∣ 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₃ :
  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 ℤ ζ))
⊢ 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