∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (f : A → B) (f' : B → A) (h₁ : Function.LeftInverse f' f) (h₂ : Function.RightInverse f' f)
  (h₃ :
    ∀ (x y : A),
      { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₅ :
    ∀ (a : A),
      { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) =
        star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)),
  { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ }.symm =
    let __src := StarRingEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅;
    { toFun := f', invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯ }