-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x y : Associates ↥R⁰
simp_rw :
  (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) (x * y)) :
            Associates R)) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) x) :
              Associates R)) :
        Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) y) :
              Associates R)) :
        Ideal R)
simp_rw₁ :
  (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (↑(HMul.hMul (α := ↥(Associates R)⁰) (β := ↥(Associates R)⁰)
                ((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) x :
                  ↥(Associates R)⁰)
                ((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) y :
                  ↥(Associates R)⁰)) :
            Associates R)) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) x) :
              Associates R)) :
        Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) y) :
              Associates R)) :
        Ideal R)
simp_rw₂ :
  (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (HMul.hMul (α := Associates R)
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) x) :
              Associates R)
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) y) :
              Associates R))) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) x) :
              Associates R)) :
        Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) y) :
              Associates R)) :
        Ideal R)
⊢ (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              (x * y)) :
          ↥(Ideal R)⁰) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x) :
            ↥(Ideal R)⁰) :
        Ideal R)
      (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                y) :
            ↥(Ideal R)⁰) :
        Ideal R)

Tactic:
simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_mul, Submonoid.coe_mul,
    associatesEquivIsPrincipal_mul]

Premises used: map_mul, Ideal.associatesEquivIsPrincipal_mul, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, Submonoid.coe_mul