-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
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)
⊢ (↑(↑((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)
have 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)
Tactic: simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_mul, Submonoid.coe_mul,
    associatesEquivIsPrincipal_mul]