∀ {A : Type u_6} {B : Type u_7} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B]
  (toMulEquiv toMulEquiv_1 : A ≃* B) (e_toMulEquiv : toMulEquiv = toMulEquiv_1)
  (map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)),
  { toMulEquiv := toMulEquiv, map_star' := map_star' } = { toMulEquiv := toMulEquiv_1, map_star' := ⋯ }