more style changes

Author: ntapiam

Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean

@@ -66,10 +66,10 @@ local notation "T[" M "]" => TensorAlgebra R M
 
 /-- Antipode in `TensorAlgebra R M` as an algebra map. -/
 def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
-  (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
+  (lift R <| (MulOpposite.opLinearEquiv R).comp <| -ι R).toLinearMap
 
 @[simp]
-lemma antipode_ι_apply (x : M) : antipode R (ι R x) = -(ι R) x := by
+lemma antipode_ι_apply (x : M) : antipode R (ι R x) = -ι R x := by
   simp [antipode]
 
 @[simp]
@@ -78,13 +78,13 @@ theorem antipode_antihom_apply (x y : T[M]) : antipode R (x * y) = antipode R y
 
 @[simp]
 theorem antipode_antihom : antipode R ∘ₗ mul' R T[M] =
-    mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ ((antipode R) ⊗ₘ (antipode R)) := by
+    mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ (antipode R ⊗ₘ antipode R) := by
   ext
   simp
 
 @[simp]
 lemma antipode_algebraMap_apply (r : R) :
-    antipode R ((algebraMap R T[M]) r) = algebraMap R T[M] r := by
+    antipode R (algebraMap R T[M] r) = algebraMap R T[M] r := by
   simp [antipode]
 
 open Algebra Bialgebra Coalgebra in