chore(RingTheory/Bialgebra/TensorProduct): enable backward.defeqAttrib.useBackward for comm

The `rw [comul a]` inside `comm` no longer matches after upstream changes to
defeq attribute handling. Locally re-enabling the backward behaviour with
`set_option backward.defeqAttrib.useBackward true` restores the previous
elaboration and lets the existing proof go through.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: kim-em

Mathlib/RingTheory/Bialgebra/TensorProduct.lean

@@ -167,6 +167,7 @@ end Heterogeneous
 section Homogeneous
 variable (R S A B) [Bialgebra R A] [Bialgebra R B]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The tensor product of `R`-bialgebras is commutative, up to bialgebra isomorphism. -/
 @[expose] def comm : A ⊗[R] B ≃ₐc[R] B ⊗[R] A :=
   .ofAlgEquiv (Algebra.TensorProduct.comm R A B) (by ext <;> simp) <| by