diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 3a8958465a..dbdacd5a2c 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -375,17 +375,19 @@ Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1).
 
 Section reassociate_products.
 Context {X Y Z : Type}.
-Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) := 
-  (xyz.1.1,(xyz.1.2,xyz.2)).
 
-Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z := 
-  ((xyz.1,xyz.2.1),xyz.2.2).
+Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) :=
+  (xyz.1.1, (xyz.1.2, xyz.2)).
+
+Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z :=
+  ((xyz.1, xyz.2.1), xyz.2.2).
 
 Lemma left_assoc_prodK : cancel left_assoc_prod right_assoc_prod.
-Proof. by case;case. Qed.
+Proof. by case; case. Qed.
 
 Lemma right_assoc_prodK : cancel right_assoc_prod left_assoc_prod.
 Proof. by case => ? []. Qed.
+
 End reassociate_products.
 
 Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1).
diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
index f811bd70dc..77eab686af 100644
--- a/theories/topology_theory/product_topology.v
+++ b/theories/topology_theory/product_topology.v
@@ -234,35 +234,30 @@ Notation compact_setM := compact_setX (only parsing).
 
 Lemma swap_continuous {X Y : topologicalType} : continuous (@swap X Y).
 Proof.
-case=> a b W /=[[U V]][] /= Ua Vb UVW; exists (V, U); first by split.
-by case => //= ? ? [] ? ?; apply: UVW.
+case=> a b W /= [[U V]][] /= Ub Va UVW; exists (V, U); first by split.
+by case => //= ? ? [] ? ?; exact: UVW.
 Qed.
 
 Section reassociate_continuous.
 Context {X Y Z : topologicalType}.
 
-Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z). 
+Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z).
 Proof.
-case;case=> a b c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU.
+move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU.
 exists ((P `*` Q), R); first split.
-- exists (P, Q); first split => //=.
-  by case=> x y /= [Px Qy]; split => //.
-- done.
-- case; case=> x y z /= [][] ? ? ?; apply: PVU; split => //.
-  exact: QRV.
+- exists (P, Q); first by [].
+  by case=> x y /= [Px Qy].
+- by [].
+- by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV.
 Qed.
 
-Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z). 
+Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z).
 Proof.
 case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU.
-exists (P, (Q `*` R)); first split.
-- done. 
-- exists (Q, R); first split => //=.
-  by case=> ? ? /= [? ?]; split.
-- case=> x [y z] [? [? ?]]; apply: VRU; split => //.
-  exact: PQV.
+exists (P, (Q `*` R)); first split => //.
+- exists (Q, R); first by [].
+  by case=> ? ? /= [].
+- by case=> x [y z] [? [? ?]]; apply: VRU; split => //; exact: PQV.
 Qed.
 
 End reassociate_continuous.
-
-