-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
h :
  emultiplicity (α := (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
      (↑(((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk ⋯ ⋯ ⋯ ⋯ :
                (↑{J : Ideal (𝓞 K) |
                        Membership.mem (γ := Multiset (Ideal (𝓞 K)))
                          (normalizedFactors
                            (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})))
                          J} :
                    Type u_1) ≃
                  (↑{d : (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] |
                        Membership.mem (γ := Multiset (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
                          (normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ))) d} :
                    Type)) :
              (a :
                  (↑{J : Ideal (𝓞 K) | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)}))} :
                    Type u_1)) →
                (↑{d : (ℤ ⧸ span {(↑p : ℤ)})[X] |
                      d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ))} :
                  Type))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦
              Membership.mem (γ := Set (Ideal (𝓞 K)))
                {J : Ideal (𝓞 K) |
                  Membership.mem (γ := Multiset (Ideal (𝓞 K)))
                    (normalizedFactors (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)}))) J}
                x)
              (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
                      (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
                    (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦
                      Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
                      (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
                Ideal (𝓞 K))
              ⋯)) :
        (ℤ ⧸ span {(↑p : ℤ)})[X])
      (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)) =
    emultiplicity (α := (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
      ((mapEquiv (Int.quotientSpanNatEquivZMod p).symm : (a : (ZMod p)[X]) → (ℤ ⧸ span {(↑p : ℤ)})[X])
          (Polynomial.map (Int.castRingHom (ZMod p)) Q) :
        (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
      ((mapEquiv (Int.quotientSpanNatEquivZMod p).symm : (a : (ZMod p)[X]) → (ℤ ⧸ span {(↑p : ℤ)})[X])
          (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) :
        (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
h₁ :
  Membership.mem (γ := Multiset (Ideal (𝓞 K)))
    (normalizedFactors (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})))
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
            (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
      Ideal (𝓞 K))
⊢ emultiplicity.{u_1} (α := Ideal (𝓞 K))
      (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
              (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
            (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
              (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
        Ideal (𝓞 K))
      (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
    emultiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
rw [← emultiplicity_map_eq (mapEquiv (Int.quotientSpanNatEquivZMod p).symm),
      emultiplicity_factors_map_eq_emultiplicity inferInstance (by simp [NeZero.ne p])
      (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral]

Premises used: inferInstance, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, RingOfIntegers.not_dvd_exponent_iff, emultiplicity_map_eq, Int.quotientSpanNatEquivZMod, Iff.mp, NumberField.RingOfIntegers.isIntegral, RingEquiv.symm, Codisjoint.eq_top, Polynomial.mapEquiv