-- 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)
⊢ 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])

Tactic:
simp only [primesOverSpanEquivMonicFactorsMod_symm_apply,
        Equiv.apply_symm_apply (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk _ _ _ _),
        Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom, mapEquiv_apply]

Premises used: Equiv.apply_symm_apply, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Polynomial.map_map, Polynomial.mapEquiv_apply, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Int.quotientSpanNatEquivZMod_comp_castRingHom