more nits

Co-authored-by: Eric Wieser <[email protected]>

Mathlib/RingTheory/AdicCompletion/Basic.lean

@@ -244,14 +244,14 @@ instance [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
     { toFun := Subtype.val, map_zero' := rfl, map_add' := fun _ _ ↦ rfl }
   Subtype.val_injective.module S f val_smul
 
-instance instIsScalarTower [SMul T S] [SMul T R] [SMul S R] [SMul T M] [SMul S M]
-    [IsScalarTower S R M] [IsScalarTower T R M] [IsScalarTower T S M] :
-    IsScalarTower T S (AdicCompletion I M) where
-  smul_assoc r s f := by ext; simp [val_smul]
-
-instance instSMulCommClass [SMul T R] [SMul S R] [SMul T M] [SMul S M]
-    [IsScalarTower S R M] [IsScalarTower T R M] [SMulCommClass T S M] :
-    SMulCommClass T S (AdicCompletion I M) where
+instance instIsScalarTower [SMul S T] [SMul S R] [SMul T R] [SMul S M] [SMul T M]
+    [IsScalarTower S R M] [IsScalarTower T R M] [IsScalarTower S T M] :
+    IsScalarTower S T (AdicCompletion I M) where
+  smul_assoc s t f := by ext; simp [val_smul]
+
+instance instSMulCommClass [SMul S R] [SMul T R] [SMul S M] [SMul T M]
+    [IsScalarTower S R M] [IsScalarTower T R M] [SMulCommClass S T M] :
+    SMulCommClass S T (AdicCompletion I M) where
   smul_comm r s f := by ext; simp [val_smul, smul_comm]
 
 /-- The canonical inclusion from the completion to the product. -/