feat(data/rat): move lemmas to right file, add nat cast lemmas, remove (#1333)

redundant lemma

Author: kappelmann

src/data/rat/basic.lean

@@ -217,6 +217,8 @@ theorem num_denom : ∀ a : ℚ, a = a.num /. a.denom
 
 theorem num_denom' (n d h c) : (⟨n, d, h, c⟩ : ℚ) = n /. d := num_denom _
 
+theorem of_int_eq_mk (z : ℤ) : of_int z = z /. 1 := num_denom' _ _ _ _
+
 @[elab_as_eliminator] theorem {u} num_denom_cases_on {C : ℚ → Sort u}
    : ∀ (a : ℚ) (H : ∀ n d, d > 0 → (int.nat_abs n).coprime d → C (n /. d)), C a
 | ⟨n, d, h, c⟩ H := by rw num_denom'; exact H n d h c

src/data/rat/cast.lean

@@ -9,8 +9,9 @@ import data.rat.order
 
 ## Summary
 
-We define the canonical injection from ℚ into an arbitrary division ring and prove various casting
-lemmas showing the well-behavedness of this injection.
+1. We define the canonical injection from ℚ into an arbitrary division ring and prove various
+casting lemmas showing the well-behavedness of this injection.
+2. We prove basic properties about the casts from ℤ and ℕ into ℚ (i.e. `(n : ℚ) = n / 1`) .
 
 ## Notations
 
@@ -37,6 +38,25 @@ protected def cast : ℚ → α
 
 @[priority 0] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩
 
+theorem coe_int_eq_mk : ∀ (z : ℤ), ↑z = z /. 1
+| (n : ℕ) := show (n:ℚ) = n /. 1,
+  by induction n with n IH n; simp [*, show (1:ℚ) = 1 /. 1, from rfl]
+| -[1+ n] := show (-(n + 1) : ℚ) = -[1+ n] /. 1, begin
+  induction n with n IH, {refl},
+  show -(n + 1 + 1 : ℚ) = -[1+ n.succ] /. 1,
+  rw [neg_add, IH],
+  simpa [show -1 = (-1) /. 1, from rfl]
+end
+
+theorem mk_eq_div (n d : ℤ) : n /. d = ((n : ℚ) / d) :=
+begin
+  by_cases d0 : d = 0, {simp [d0, div_zero]},
+  simp [division_def, coe_int_eq_mk, mul_def one_ne_zero d0]
+end
+
+theorem coe_int_eq_of_int (z : ℤ) : ↑z = of_int z :=
+(coe_int_eq_mk z).trans (of_int_eq_mk z).symm
+
 @[simp] theorem cast_of_int (n : ℤ) : (of_int n : α) = n :=
 show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one]
 
@@ -49,6 +69,9 @@ by rw coe_int_eq_of_int; refl
 @[simp, elim_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1 :=
 by rw coe_int_eq_of_int; refl
 
+theorem coe_nat_eq_mk (n : ℕ) : ↑n = n /. 1 :=
+by rw [← int.cast_coe_nat, coe_int_eq_mk]
+
 @[simp, elim_cast] theorem coe_nat_num (n : ℕ) : (n : ℚ).num = n :=
 by rw [← int.cast_coe_nat, coe_int_num]
 

src/data/rat/floor.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import data.rat.order
+import data.rat.cast
 /-!
 # Floor and Ceil Functions for Rational Numbers
 
@@ -38,7 +39,7 @@ theorem le_floor {z : ℤ} : ∀ {r : ℚ}, z ≤ floor r ↔ (z : ℚ) ≤ r
   rw [num_denom'],
   have h' := int.coe_nat_lt.2 h,
   conv { to_rhs,
-    rw [coe_int_eq_mk, mk_le zero_lt_one h', mul_one] },
+    rw [coe_int_eq_mk, rat.le_def zero_lt_one h', mul_one] },
   exact int.le_div_iff_mul_le h'
 end
 

src/data/rat/order.lean

@@ -131,13 +131,6 @@ show rat.nonneg a ↔ rat.nonneg (a - 0), by simp
 theorem num_nonneg_iff_zero_le : ∀ {a : ℚ}, 0 ≤ a.num ↔ 0 ≤ a
 | ⟨n, d, h, c⟩ := @nonneg_iff_zero_le ⟨n, d, h, c⟩
 
-theorem mk_le {a b c d : ℤ} (h₁ : b > 0) (h₂ : d > 0) :
-  a /. b ≤ c /. d ↔ a * d ≤ c * b :=
-by conv in (_ ≤ _) {
-  simp only [(≤), rat.le],
-  rw [sub_def (ne_of_gt h₂) (ne_of_gt h₁),
-      mk_nonneg _ (mul_pos h₂ h₁), ge, sub_nonneg] }
-
 protected theorem add_le_add_left {a b c : ℚ} : c + a ≤ c + b ↔ a ≤ b :=
 by unfold has_le.le rat.le; rw add_sub_add_left_eq_sub
 
@@ -176,28 +169,6 @@ lt_iff_lt_of_le_iff_le $
 by simpa [(by cases a; refl : (-a).num = -a.num)]
    using @num_nonneg_iff_zero_le (-a)
 
-theorem of_int_eq_mk (z : ℤ) : of_int z = z /. 1 := num_denom' _ _ _ _
-
-theorem coe_int_eq_mk : ∀ z : ℤ, ↑z = z /. 1
-| (n : ℕ) := show (n:ℚ) = n /. 1,
-  by induction n with n IH n; simp [*, show (1:ℚ) = 1 /. 1, from rfl]
-| -[1+ n] := show (-(n + 1) : ℚ) = -[1+ n] /. 1, begin
-  induction n with n IH, {refl},
-  show -(n + 1 + 1 : ℚ) = -[1+ n.succ] /. 1,
-  rw [neg_add, IH],
-  simpa [show -1 = (-1) /. 1, from rfl]
-end
-
-theorem coe_int_eq_of_int (z : ℤ) : ↑z = of_int z :=
-(coe_int_eq_mk z).trans (of_int_eq_mk z).symm
-
-theorem mk_eq_div (n d : ℤ) : n /. d = (n / d : ℚ) :=
-begin
-  by_cases d0 : d = 0, {simp [d0, div_zero]},
-  rw [division_def, coe_int_eq_mk, coe_int_eq_mk, inv_def,
-      mul_def one_ne_zero d0, one_mul, mul_one]
-end
-
 theorem abs_def (q : ℚ) : abs q = q.num.nat_abs /. q.denom :=
 begin
   have hz : (0:ℚ) = 0 /. 1 := rfl,