cleaning

Author: t6s

classical/classical_orders.v

@@ -329,7 +329,7 @@ Lemma big_lexi_order_interval_prefix (i : interval (big_lexi_order K))
   itv_open_ends i -> x \in i ->
   exists n, same_prefix n x `<=` [set` i].
 Proof.
-move: i; case=> [][[]l|[]] [[]r|[]] /orP []// ?; rewrite ?in_itv /= ?andbT.
+move: i; case=> [][[]l|[]] [[]r|[]]// ?; rewrite ?in_itv /= ?andbT.
 - move=> /andP[lx xr].
   case E1 : (first_diff l x) => [m|]; first last.
     by move: lx; move/first_diff_NoneP : E1 ->; rewrite bnd_simp.

classical/set_interval.v

@@ -868,8 +868,8 @@ End closed_endpoints.
 Lemma itv_open_endsI {d} {T : orderType d} (i j : interval T) :
   itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O.
 Proof.
-move: i => [][[]a|[]] [[]b|[]] /orP []//= _;
-move: j => [][[]x|[]] [[]y|[]] /orP []//= _;
+move: i => [][[]a|[]] [[]b|[]]//=;
+move: j => [][[]x|[]] [[]y|[]]//=;
 by rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=;
   try ((by left)||(by right)).
 Qed.

theories/normedtype_theory/ereal_normedtype.v

@@ -496,7 +496,7 @@ apply/seteqP; split=> A.
   + case=> M [Mreal MA].
     exists `]-oo, M%:E[ => [|y/=]; rewrite in_itv/= ?ltNyr; last exact: MA.
     by split => //; left.
-- move=> [[ [[]/= r|[]] [[]/= s|[]] ]] [] /orP []// _.
+- move=> [[ [[]/= r|[]] [[]/= s|[]] ]][]// _.
   + move=> /[dup]/ltgte_fin_num/fineK <-; rewrite in_itv/=.
     move=> /andP[rx sx] rsA; apply: (nbhs_interval rx sx) => z rz zs.
     by apply: rsA =>/=; rewrite in_itv/= rz.

theories/topology_theory/num_topology.v

@@ -90,7 +90,7 @@ rewrite eqEsubset; split => U.
     by rewrite in_itv/= -lter_distl subrr normr0.
   apply: subset_trans xeU => z /=.
   by rewrite in_itv /= -lter_distl distrC.
-case => [][[[]l|[]]] [[]r|[]] [] /orP[]//= _.
+case => [][[[]l|[]]] [[]r|[]] []//= _.
 - move=> xlr lrU; exists (Order.min (x - l) (r - x)).
     by rewrite /= lt_min ?lterBDr ?add0r ?(itvP xlr).
   apply/(subset_trans _ lrU)/subset_ball_prop_in_itv.

theories/topology_theory/order_topology.v

@@ -95,7 +95,7 @@ Hint Resolve itv_open : core.
 
 Lemma itv_open_ends_open (i : interval T) : itv_open_ends i -> open [set` i].
 Proof.
-case: i; rewrite /itv_open_ends => [[[]t1|[]]] [[]t2|[]] /orP[]? => //.
+case: i; rewrite /itv_open_ends => [[[]t1|[]]] [[]t2|[]]// ?.
 by rewrite set_itvE; exact: openT.
 Qed.
 
@@ -225,7 +225,7 @@ pose j := \big[Order.meet/`]-oo, +oo[]_(i <- F) i.
 exists j; first split.
 - rewrite /j (@eq_fbig_cond _ _ _ _ _ F _ (mem F) _ id)//.
   + apply: (big_ind itv_open_ends) => //=; first exact: itv_open_endsI.
-    by rewrite /itv_open_ends;  move=> i /rayF /set_mem ->.
+    by rewrite /itv_open_ends; move=> i /rayF /set_mem ->.
   + by move=> p /=; rewrite !inE/=; exact: andb_id2l.
 - pose f (i : interval T) : Prop := x \in i; suff : f j by [].
   rewrite /j (@eq_fbig_cond _ _ _ _ _ F _ (mem F) _ id)//=.

theories/topology_theory/weak_topology.v

@@ -203,7 +203,7 @@ Let WeakU : topologicalType := @weak_topology (sub_type Y) X val.
 Lemma open_order_weak (U : set Y) : @open OrdU U -> @open WeakU U.
 Proof.
 rewrite ?openE /= /interior => + x Ux => /(_ x Ux); rewrite itv_nbhsE /=.
-move=> [][][[]l|[]] [[]r|[]][]/orP[]//= _ xlr /filterS; apply.
+move=> [][][[]l|[]] [[]r|[]][]//= _ xlr /filterS; apply.
 - exists `]l, r[%classic; split => //=; exists `]\val l, \val r[%classic.
     exact: itv_open.
   by rewrite eqEsubset; split => z; rewrite preimage_itv.