∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A →ₐc[R] B) (hf : Function.Bijective ⇑f) (a : A),
  (BialgEquiv.ofBijective f hf) a = f a