diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 22188740a..ee6666e98 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -591,7 +591,7 @@ subst (add_comm b c) (subst (add_comm a c) (sub_add_add_right a b c))
 
 -- TODO: fix this
 theorem dist_def (n m : ℕ) : dist n m = (to_nat (of_nat n - m)) :=
-have H [fact] : of_nat n - m = psub (pair n m), from
+have H : of_nat n - m = psub (pair n m), from
   calc
     psub (pair n 0) + -psub (pair m 0) = psub (pair (n + 0) (0 + m)) : by simp
       ... = psub (pair n m) : by simp,
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 298f22b0d..99678953f 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -73,7 +73,7 @@ let f  := rec_measure default measure rec_val in
 case_strong_induction_on m
   (take x,
     have H1 : f' 0 x = default, from rfl,
-    have H2 [fact]: ¬ measure x < 0, from not_lt_zero,
+    have H2 : ¬ measure x < 0, from not_lt_zero,
     have H3 : restrict default measure f 0 x = default, from if_neg H2,
     show f' 0 x = restrict default measure f 0 x, from trans H1 (symm H3))
   (take m,
@@ -88,7 +88,7 @@ case_strong_induction_on m
               calc
                 f' m z = restrict default measure f m z : IH m le_refl z
                   ... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1)),
-          have H2 [fact] : f' (succ m) x = rec_val x f, from
+          have H2 : f' (succ m) x = rec_val x f, from
             calc
               f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
                 ... = rec_val x (f' m) : if_pos H1