∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Mul (Ms j)]
  [inst_1 : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j),
  MulEquiv.piCongrRight es =
    { toFun := fun x j => (es j) (x j), invFun := fun x j => (es j).symm (x j), left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }