-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J
⊢ emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I) =
    emultiplicity
      (↑(((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' :
                Equiv.{u_2 + 1, u_1 + 1}
                  (↑{J : Ideal S |
                        Membership.mem (γ := Multiset (Ideal S))
                          (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J} :
                    Type u_2)
                  (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                    Type u_1)) :
              (a : (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2)) →
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1))
            (Subtype.mk (p := fun (x : Ideal S) ↦
              Membership.mem (γ := Set (Ideal S))
                {J : Ideal S |
                  Membership.mem (γ := Multiset (Ideal S))
                    (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J}
                x)
              J hJ)) :
        (R ⧸ I)[X])
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
have rw : emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I) =
  emultiplicity
    (↑(((Equiv.trans (β :=
                (↑{M : Ideal (R ⧸ I)[X] |
                      Membership.mem (γ := Multiset (Ideal (R ⧸ I)[X]))
                        (normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) M} :
                  Type u_1))
                (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx') sorry sorry :
                  Equiv.{u_2 + 1, u_1 + 1}
                    (↑{L : Ideal S |
                          Membership.mem (γ := Multiset (Ideal S))
                            (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) L} :
                      Type u_2)
                    (↑{M : Ideal (R ⧸ I)[X] |
                          Membership.mem (γ := Multiset (Ideal (R ⧸ I)[X]))
                            (normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) M} :
                      Type u_1))
                (Equiv.symm (Ideal.normalizedFactorsEquivSpanNormalizedFactors sorry) :
                  (↑{I_1 : Ideal (R ⧸ I)[X] |
                          Membership.mem (γ := Multiset (Ideal (R ⧸ I)[X]))
                            (normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) I_1} :
                      Type u_1) ≃
                    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                      Type u_1)) :
              Equiv.{u_2 + 1, u_1 + 1}
                (↑{L : Ideal S |
                      Membership.mem (γ := Multiset (Ideal S))
                        (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) L} :
                  Type u_2)
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1)) :
            (a : (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2)) →
              (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                Type u_1))
          (Subtype.mk (p := fun (x : Ideal S) ↦
            Membership.mem (γ := Set (Ideal S))
              {J : Ideal S |
                Membership.mem (γ := Multiset (Ideal S))
                  (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J}
              x)
            J hJ)) :
      (R ⧸ I)[X])
    (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
Tactic: rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Equiv.coe_trans, Function.comp_apply,
    Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity,
    IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity]