Update Mathlib/RingTheory/HopfAlgebra/Basic.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

Author: hawkrobe

Mathlib/RingTheory/HopfAlgebra/Basic.lean

@@ -242,10 +242,8 @@ open Coalgebra WithConv LinearMap
 /-- Upgrade a bialgebra to a Hopf algebra by specifying a convolution inverse of the identity. -/
 noncomputable abbrev ofConvInverse [CommSemiring R] [Semiring A] [Bialgebra R A]
     (antipode : A →ₗ[R] A)
-    (mul_antipode_rTensor_comul :
-      toConv antipode * toConv LinearMap.id = (1 : WithConv (A →ₗ[R] A)))
-    (mul_antipode_lTensor_comul :
-      toConv LinearMap.id * toConv antipode = (1 : WithConv (A →ₗ[R] A))) :
+    (mul_antipode_rTensor_comul : toConv antipode * toConv LinearMap.id = 1)
+    (mul_antipode_lTensor_comul : toConv LinearMap.id * toConv antipode = 1) :
     HopfAlgebra R A where
   antipode := antipode
   mul_antipode_rTensor_comul := by simpa using congr(($mul_antipode_rTensor_comul).ofConv)