wo destruct

theories/separation_axioms.v

@@ -1129,22 +1129,19 @@ End perfect_sets.
 Section sum_separations.
 Context {I : choiceType} {X : I -> topologicalType}.
 
-Lemma sum_hausdorff : 
+Lemma sum_hausdorff :
   (forall i, hausdorff_space (X i)) -> hausdorff_space {i & X i}.
 Proof.
-move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= ?sum_nbhsE /= => cl. 
-have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]).
-- by apply: existT_nbhs; exact: filterT.
-- by apply: existT_nbhs; exact: filterT.
-(* TODO: get rid of dependent destruct *)
-move=> p [/= [? _] <- [ ? _]] [] E; destruct E => _.
-congr( _ _); apply: hX => U V Ux Vy.
-have [] := cl (existT X j @` U) (existT X j @` V).
-- exact: existT_nbhs.
-- exact: existT_nbhs.
-move=> z [/= [l] ?] <- [r] Vr lr; exists l; split => //.
-move: Vr; have -> // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr.
-by move=> a b; case: (pselect (a = b)) => ?; [left | right].
-Qed. 
-
-End sum_separations.
+move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sum_nbhsE /= => cl.
+have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]);
+  [by apply: existT_nbhs; exact: filterT..|].
+move=> p [/= [_ _ <-] [_ _ [ji]]] _.
+rewrite {}ji {j} in x y cl *.
+congr existT; apply: hX => U V Ux Vy.
+have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|].
+move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //.
+rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr.
+by move=> a b; exact: pselect.
+Qed.
+
+End sum_separations.

theories/topology_theory/sum_topology.v

@@ -19,10 +19,10 @@ Local Open Scope ring_scope.
 Section sum_topology.
 Context {I : choiceType} {X : I -> topologicalType}.
 
-Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := 
-   (existT _ _) @ (nbhs (projT2 x)).
+Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} :=
+  existT _ _ @ nbhs (projT2 x).
 
-Lemma sum_nbhsE (i : I) (x : X i) : 
+Lemma sum_nbhsE (i : I) (x : X i) :
   sum_nbhs (existT _ i x) = (existT _ _) @ (nbhs x).
 Proof. by done. Qed.
 
@@ -32,62 +32,56 @@ Local Lemma sum_nbhs_proper x : ProperFilter (sum_nbhs x).
 Proof. by case: x => i xi; exact: fmap_proper_filter. Qed.
 
 Local Lemma sum_nbhs_singleton x A : sum_nbhs x A -> A x.
-Proof. by case: x => ? ? /=; apply: nbhs_singleton. Qed.
+Proof. by case: x => ? ? /=; exact: nbhs_singleton. Qed.
 
 Local Lemma sum_nbhs_nbhs x A: sum_nbhs x A -> sum_nbhs x (sum_nbhs^~ A).
-Proof. 
-case: x => i zi /=.
-  rewrite sum_nbhsE /= nbhsE /=; case => W [oW Wz WlA].
-  exists W; first by split.
-  move=> x /= ?; move/filterS: WlA; apply.
-  by apply: open_nbhs_nbhs.
+Proof.
+case: x => i Xi /=.
+rewrite sum_nbhsE /= nbhsE /= => -[W [oW Wz WlA]].
+by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs.
 Qed.
 
 HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i}
   sum_nbhs_proper sum_nbhs_singleton sum_nbhs_nbhs.
 
-Lemma existT_continuous (i : I) : continuous (existT X i). 
+Lemma existT_continuous (i : I) : continuous (existT X i).
 Proof. by move=> ? ?. Qed.
 
-Lemma existT_open_map (i : I) (A : set (X i)): open A -> open (existT X i @` A).
-Proof. 
-move=> oA; rewrite openE /interior /= => ?. 
-case=> x Ax <-; rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=.
+Lemma existT_open_map (i : I) (A : set (X i)) : open A -> open (existT X i @` A).
+Proof.
+move=> oA; rewrite openE /interior /= => iXi [x Ax <-].
+rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=.
 move: oA; rewrite openE => /(_ _ Ax); apply: filterS.
-by move=> z => Az; exists z.
+by move=> z Az; exists z.
 Qed.
 
-Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : 
+Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) :
   nbhs x U -> nbhs (existT _ i x) (existT _ i @` U).
-Proof. by move/filterS; apply; exact: preimage_image. Qed.
+Proof. exact/filterS/preimage_image. Qed.
 
-Lemma sum_openP (U : set {i & X i}) : 
-  open U <-> (forall i, open (existT _ i@^-1` U)).
+Lemma sum_openP (U : set {i & X i}) :
+  open U <-> forall i, open (existT _ i @^-1` U).
 Proof.
-split => ?.
-  by move=> i; apply: open_comp=> //; move=> y _; exact: existT_continuous.
-rewrite openE /interior; case=> i x Uxi.
-rewrite /nbhs /= sum_nbhsE; apply: open_nbhs_nbhs; split => //.
+split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous.
+rewrite openE => -[i x Uxi].
+by rewrite /interior /nbhs/= sum_nbhsE; exact: open_nbhs_nbhs.
 Qed.
 
-Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : 
+Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) :
   (forall i, continuous (f i)) -> continuous (sum_fun f).
 Proof. by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed.
 
-Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: (X i)]).
-Proof.
-by rewrite eqEsubset; split; case=> i x //=; first by move=> _; exists i.
-Qed.
+Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: X i]).
+Proof. by rewrite eqEsubset; split => [[i x] _|[]//]; exists i. Qed.
 
-Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> 
-  compact [set: {i&X i}].
+Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) ->
+  compact [set: {i & X i}].
 Proof.
-move=> fsetI cptX.
-rewrite sum_setUE -fsbig_setU //; apply: big_ind.
-- exact: compact0.
-- by move=> ? ? ? ?; exact: compactU.
-move=> i _; apply: continuous_compact; last exact: cptX.
-by apply: continuous_subspaceT; exact: existT_continuous.
+move=> fsetI cptX; rewrite sum_setUE -fsbig_setU//.
+apply: big_rec; first exact: compact0.
+move=> i ? _ cptx; apply: compactU => //.
+apply: continuous_compact; last exact: cptX.
+exact/continuous_subspaceT/existT_continuous.
 Qed.
 
 End sum_topology.