diff --git a/library/standard/data/sum.lean b/library/standard/data/sum.lean
index 92cedad93c..28382b1047 100644
--- a/library/standard/data/sum.lean
+++ b/library/standard/data/sum.lean
@@ -32,19 +32,19 @@ sum_rec H1 H2 s
 theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
 let f := λs, rec_on s (λa, a1 = a) (λb, false) in
 have H1 : f (inl B a1), from rfl,
-have H2 : f (inl B a2), from @subst _ _ _ f H H1,
+have H2 : f (inl B a2), from subst H H1,
 H2
 
 theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
 let f := λs, rec_on s (λa', a = a') (λb, false) in
 have H1 : f (inl B a), from rfl,
-have H2 : f (inr A b), from @subst _ _ _ f H H1,
+have H2 : f (inr A b), from subst H H1,
 H2
 
 theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
 let f := λs, rec_on s (λa, false) (λb, b1 = b) in
 have H1 : f (inr A b1), from rfl,
-have H2 : f (inr A b2), from @subst _ _ _ f H H1,
+have H2 : f (inr A b2), from subst H H1,
 H2
 
 theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) :=
@@ -61,15 +61,15 @@ rec_on s1
     rec_on s2
       (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
       (take b2,
-	have H3 : (inl B a1 = inr A b2) ↔ false,
-	  from iff_intro inl_neq_inr (assume H4, false_elim _ H4),
-	show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3)))
+        have H3 : (inl B a1 = inr A b2) ↔ false,
+          from iff_intro inl_neq_inr (assume H4, false_elim _ H4),
+        show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3)))
   (take b1, show decidable (inr A b1 = s2), from
     rec_on s2
       (take a2,
-	have H3 : (inr A b1 = inl B a2) ↔ false,
-	  from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim _ H4),
-	show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
+        have H3 : (inr A b1 = inl B a2) ↔ false,
+          from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim _ H4),
+        show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
 end sum
\ No newline at end of file