refine' ⟨fun ⟨u, hu⟩ => ⟨⟨(MulEquiv.prodUnits.toFun u).1, (Prod.eq_iff_fst_eq_snd_eq.1 hu).1⟩,
  ⟨(MulEquiv.prodUnits.toFun u).2, (Prod.eq_iff_fst_eq_snd_eq.1 hu).2⟩⟩, fun ⟨⟨u₁, h₁⟩, ⟨u₂, h₂⟩⟩ =>
    ⟨MulEquiv.prodUnits.invFun (u₁, u₂), Prod.eq_iff_fst_eq_snd_eq.2 ⟨h₁, h₂⟩⟩⟩
M✝ : Type ?u.2605
N✝ : Type ?u.2608
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x z : M × N
⊢ Associated x z ↔ Associated x.1 z.1 ∧ Associated x.2 z.2
no goals