feat(data/sum/basic): sum.lift_rel is a subrelation of sum.lex (#…

…15358)

Also trivial spacing fix.

src/data/sum/basic.lean

@@ -286,14 +286,16 @@ instance [decidable_rel r] [decidable_rel s] : decidable_rel (lex r s)
 protected lemma lift_rel.lex {a b : α ⊕ β} (h : lift_rel r s a b) : lex r s a b :=
 by { cases h, exacts [lex.inl ‹_›, lex.inr ‹_›] }
 
+lemma lift_rel_subrelation_lex : subrelation (lift_rel r s) (lex r s) := λ a b, lift_rel.lex
+
 lemma lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : lex r₁ s₁ x y) :
   lex r₂ s₂ x y :=
 by { cases h, exacts [lex.inl (hr _ _ ‹_›), lex.inr (hs _ _ ‹_›), lex.sep _ _] }
 
 lemma lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : lex r₁ s x y) : lex r₂ s x y :=
 h.mono hr $ λ _ _, id
 
-lemma lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b)  (h : lex r s₁ x y) : lex r s₂ x y :=
+lemma lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : lex r s₁ x y) : lex r s₂ x y :=
 h.mono (λ _ _, id) hs
 
 lemma lex_acc_inl {a} (aca : acc r a) : acc (lex r s) (inl a) :=