-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
r : R
hr : r ≠ 0
I : (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} : Type u_1)
a : R
ha : Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} a
hx :
  ((normalizedFactorsEquivSpanNormalizedFactors hr :
          (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
            (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} : Type u_1)) :
        (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
          (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha) =
    I
rw :
  emultiplicity
      (↑(((Equiv.symm (normalizedFactorsEquivSpanNormalizedFactors hr) :
                (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1) ≃
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) :
              (a : (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1)) →
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
            (((normalizedFactorsEquivSpanNormalizedFactors hr :
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                    (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                      Type u_1)) :
                (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                  (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha))) :
        R)
      r =
    emultiplicity (α := Ideal R)
      (↑(((normalizedFactorsEquivSpanNormalizedFactors hr :
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1)) :
              (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha)) :
        Ideal R)
      (span {r})
rw₁ :
  emultiplicity
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha) : R) r =
    emultiplicity (α := Ideal R)
      (↑(((normalizedFactorsEquivSpanNormalizedFactors hr :
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1)) :
              (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha)) :
        Ideal R)
      (span {r})
rw₂ :
  emultiplicity a r =
    emultiplicity (α := Ideal R)
      (↑(((normalizedFactorsEquivSpanNormalizedFactors hr :
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1)) :
              (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha)) :
        Ideal R)
      (span {r})
rw₃ rw₄ :
  emultiplicity (α := Ideal R)
      (↑(((normalizedFactorsEquivSpanNormalizedFactors hr :
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1)) :
              (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha)) :
        Ideal R)
      (span {r}) =
    emultiplicity (α := Ideal R)
      (↑(((normalizedFactorsEquivSpanNormalizedFactors hr :
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1)) :
              (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha)) :
        Ideal R)
      (span {r})
⊢ emultiplicity
      (↑(((Equiv.symm (normalizedFactorsEquivSpanNormalizedFactors hr) :
                (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1) ≃
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) :
              (a : (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1)) →
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
            I) :
        R)
      r =
    emultiplicity (↑I : Ideal R) (span {r})

Tactic:
rw [hx.symm, Equiv.symm_apply_apply, Subtype.coe_mk,
    emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity hr ha]

Premises used: Subtype.coe_mk, Equiv.symm_apply_apply, Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, Eq.symm