diff --git a/src/data/sum/basic.lean b/src/data/sum/basic.lean
index 97240afc4bd21..590a4957cca64 100644
--- a/src/data/sum/basic.lean
+++ b/src/data/sum/basic.lean
@@ -286,6 +286,8 @@ 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 _ _] }
@@ -293,7 +295,7 @@ by { cases h, exacts [lex.inl (hr _ _ ‹_›), lex.inr (hs _ _ ‹_›), lex.se
 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) :=