-- Module: Mathlib.NumberTheory.KummerDedekind
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
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') ⋯ ⋯ :
                    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 ⋯) :
                    (↑{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))
rw₁ :
  emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I) =
    emultiplicity
      (↑(Function.comp (β :=
            (↑{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 ⋯) :
                  (↑{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)) :
              (a :
                  (↑{M : Ideal (R ⧸ I)[X] |
                        M ∈ normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})} :
                    Type u_1)) →
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1))
            (⇑(IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx') ⋯ ⋯ :
                  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)) :
              (a : (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2)) →
                (↑{M : Ideal (R ⧸ I)[X] |
                      M ∈ normalizedFactors (span {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))
rw₂ :
  emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I) =
    emultiplicity
      (↑(((Equiv.symm (Ideal.normalizedFactorsEquivSpanNormalizedFactors ⋯) :
                (↑{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)) :
              (a :
                  (↑{M : Ideal (R ⧸ I)[X] |
                        M ∈ normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})} :
                    Type u_1)) →
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1))
            (((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx') ⋯ ⋯ :
                  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)) :
                (a : (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2)) →
                  (↑{M : Ideal (R ⧸ I)[X] |
                        M ∈ normalizedFactors (span {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))
rw₃ :
  emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I) =
    emultiplicity (α := Ideal (R ⧸ I)[X])
      (↑(((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx') ⋯ ⋯ :
                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)) :
              (a : (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2)) →
                (↑{M : Ideal (R ⧸ I)[X] |
                      M ∈ normalizedFactors (span {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)) :
        Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
rw₄ rw₅ :
  emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I) =
    emultiplicity J (Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ 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))

Tactic:
rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Equiv.coe_trans, Function.comp_apply,
    Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity,
    IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity]

Premises used: Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Function.comp_apply, Equiv.coe_trans