∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {f : A → B} {h : ∀ (x y : A), f (x + y) = f x + f y}
  {h₀ :
    ∀ (m : R) (x : A),
      { toFun := f, map_add' := h }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h }.toFun x}
  {h₁ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = CoalgebraStruct.counit}
  {h₂ :
    TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ
        CoalgebraStruct.comul =
      CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ }}
  {h₃ : B → A}
  {h₄ :
    Function.LeftInverse h₃
      { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun}
  {h₅ :
    Function.RightInverse h₃
      { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun},
  ⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄,
        right_inv := h₅ } =
    f