nitpicks

CHANGELOG_UNRELEASED.md

@@ -116,6 +116,7 @@
 - in `normedtype.v`, added notations `^'+`, `^'-`, `+oo_R`, `-oo_R`
 - in `topology.v`
   + definition `quotient_topologicalType_mixin`, `quotient_topologicalType`
+  + definition `quotient_open`
   + lemma `pi_continuous`, `quotient_continuous`,`repr_comp_continuous`
 
 ### Changed

theories/topology.v

@@ -4761,24 +4761,23 @@ Definition fct_pseudoMetricType_mixin :=
 Canonical fct_pseudoMetricType := PseudoMetricType (T -> U) fct_pseudoMetricType_mixin.
 End fct_PseudoMetric.
 
-Section quotients. 
+Section quotients.
 Local Open Scope quotient_scope.
 Context {T : topologicalType} {Q : quotType T}.
 
 Canonical quotient_eq := EqType Q gen_eqMixin.
 Canonical quotient_choice := ChoiceType Q gen_choiceMixin.
 Canonical quotient_pointed := PointedType Q (\pi_Q point).
 
-Definition quotient_open (U : set Q) := open (\pi_Q@^-1` U).
+Definition quotient_open U := open (\pi_Q @^-1` U).
 
-Program Definition quotient_topologicalType_mixin := 
+Program Definition quotient_topologicalType_mixin :=
   @topologyOfOpenMixin Q quotient_open _ _ _.
-
 Next Obligation. by rewrite /quotient_open preimage_setT; exact: openT. Qed.
 Next Obligation. by move=> ? ? ? ?; exact: openI. Qed.
 Next Obligation. by move=> I f ofi; apply: bigcup_open => i _; exact: ofi. Qed.
 
-Let quotient_filtered := Filtered.Class (Pointed.class quotient_pointed) 
+Let quotient_filtered := Filtered.Class (Pointed.class quotient_pointed)
   (nbhs_of_open quotient_open).
 
 Canonical quotient_topologicalType := @Topological.Pack Q
@@ -4792,20 +4791,18 @@ Proof. exact/continuousP. Qed.
 Lemma quotient_continuous {Z : topologicalType} (f : Q' -> Z) :
   continuous f <-> continuous (f \o \pi_Q).
 Proof.
-split => /continuousP /= cts; apply/continuousP => A oA.
-  by rewrite comp_preimage; move/continuousP: pi_continuous; apply; exact: cts.
-by have := cts _ oA.
+split => /continuousP /= cts; apply/continuousP => A oA; last exact: cts.
+by rewrite comp_preimage; move/continuousP: pi_continuous; apply; exact: cts.
 Qed.
 
 Lemma repr_comp_continuous (Z : topologicalType) (g : T -> Z) :
-  continuous g -> {homo g : a b / a == b %[mod Q] >-> a == b} -> 
+  continuous g -> {homo g : a b / a == b %[mod Q] >-> a == b} ->
   continuous (g \o repr : Q' -> Z).
 Proof.
 move=> /continuousP ctsG rgE; apply/continuousP => A oA.
-rewrite /open /= /quotient_open comp_preimage; have := ctsG _ oA.
-have greprE : forall x, g (repr (\pi_Q x)) = g x.
-  by move=> x; apply/eqP; apply: rgE; rewrite reprK.
-by congr (open _); rewrite eqEsubset; split => x; rewrite /= greprE.
+rewrite /open/= /quotient_open (_ : _ @^-1` _ = g @^-1` A); first exact: ctsG.
+have greprE x : g (repr (\pi_Q x)) = g x by apply/eqP; rewrite rgE// reprK.
+by rewrite eqEsubset; split => x /=; rewrite greprE.
 Qed.
 
 End quotients.