From c4c2d703f6a977e80b72bf44e18a2d504e28f083 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Mon, 27 Mar 2017 18:49:57 -0400
Subject: [PATCH] feat(library/init/data): simplify int.transfer; add int and
 nat to zero_ne_one_class

---
 library/init/data/int/basic.lean  | 11 +++++------
 library/init/data/int/order.lean  |  2 +-
 library/init/data/nat/lemmas.lean |  3 +++
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index 8ae5da68d1..e3a2eef6b2 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -304,10 +304,9 @@ protected meta def transfer_core : tactic unit := do
     `int.rel_eq, `int.rel_zero, `int.rel_one,
     `int.rel_add, `int.rel_neg, `int.rel_mul]
 
-
-protected meta def transfer (distrib := ff) : tactic unit :=
-if distrib then `[abstract {int.transfer_core, simp [add_mul, mul_add], intros, trivial}]
-else `[abstract {int.transfer_core, simp, intros, trivial}]
+protected meta def transfer (distrib := tt) : tactic unit :=
+if distrib then `[int.transfer_core, simp [add_mul, mul_add]]
+else `[int.transfer_core, simp]
 
 instance : comm_ring int :=
 { add            := int.add,
@@ -342,7 +341,7 @@ instance : semiring int           := by apply_instance
 instance : ring int               := by apply_instance
 instance : distrib int            := by apply_instance
 
-protected lemma zero_ne_one : (0 : int) ≠ 1 :=
-by int.transfer
+instance : zero_ne_one_class ℤ :=
+{ zero := 0, one := 1, zero_ne_one := by int.transfer }
 
 end int
diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index bf6b8249f9..3c384ae95d 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -206,7 +206,7 @@ instance : decidable_linear_ordered_comm_ring int :=
   lt_irrefl       := int.lt_irrefl,
   add_le_add_left := @int.add_le_add_left,
   add_lt_add_left := @int.add_lt_add_left,
-  zero_ne_one     := int.zero_ne_one,
+  zero_ne_one     := zero_ne_one,
   mul_nonneg      := @int.mul_nonneg,
   mul_pos         := @int.mul_pos,
   le_iff_lt_or_eq := int.le_iff_lt_or_eq,
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index a269e2087d..cc0a00dd25 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -63,6 +63,9 @@ assume h, nat.no_confusion h
 protected lemma zero_ne_one : 0 ≠ (1 : ℕ) :=
 assume h, nat.no_confusion h
 
+instance : zero_ne_one_class ℕ :=
+{ zero := 0, one := 1, zero_ne_one := nat.zero_ne_one }
+
 lemma eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
 | 0     m := by simp [nat.zero_add]
 | (n+1) m := λ h,