-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
⊢ 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 ℤ θ))
have h : emultiplicity (α := (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
    (↑(((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk sorry sorry sorry sorry :
              (↑{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))
            sorry)) :
      (ℤ ⧸ 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])
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]