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