chore(data/pnat/basic): add mk_le_mk, mk_lt_mk, coe_le_coe, `co…

…e_lt_coe` (#2613)

src/data/pnat/basic.lean

@@ -66,6 +66,16 @@ instance : decidable_eq ℕ+ := λ (a b : ℕ+), by apply_instance
 instance : decidable_linear_order ℕ+ :=
 subtype.decidable_linear_order _
 
+@[simp] lemma mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
+  (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k := iff.rfl
+
+@[simp] lemma mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
+  (⟨n, hn⟩ : ℕ+) < ⟨k, hk⟩ ↔ n < k := iff.rfl
+
+@[simp, norm_cast] lemma coe_le_coe (n k : ℕ+) : (n:ℕ) ≤ k ↔ n ≤ k := iff.rfl
+
+@[simp, norm_cast] lemma coe_lt_coe (n k : ℕ+) : (n:ℕ) < k ↔ n < k := iff.rfl
+
 @[simp] theorem pos (n : ℕ+) : 0 < (n : ℕ) := n.2
 
 theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq

src/data/pnat/intervals.lean

@@ -12,21 +12,11 @@ namespace pnat
 def Ico (l u : ℕ+) : finset ℕ+ :=
 (finset.Ico l u).attach.map
   { to_fun := λ n, ⟨(n : ℕ), lt_of_lt_of_le l.2 (finset.Ico.mem.1 n.2).1⟩,
-    inj := λ n m h, subtype.ext.2 (by { replace h := congr_arg subtype.val h, exact h }) } -- why can't we do this directly?
+    -- why can't we do this directly?
+    inj := λ n m h, subtype.eq (by { replace h := congr_arg subtype.val h, exact h }) }
 
-@[simp] lemma Ico.mem {n m l : ℕ+} : l ∈ Ico n m ↔ n ≤ l ∧ l < m :=
-begin
-  dsimp [Ico],
-  simp only [finset.mem_attach, finset.mem_map, function.embedding.coe_fn_mk, exists_prop_of_true, subtype.exists],
-  split,
-  { rintro ⟨a, ⟨h, rfl⟩⟩,
-    simp at h,
-    exact ⟨h.1, h.2⟩ },
-  { rintro ⟨h₁, h₂⟩,
-    use l,
-    split; simp,
-    exact ⟨h₁, h₂⟩ }
-end
+@[simp] lemma Ico.mem : ∀ {n m l : ℕ+}, l ∈ Ico n m ↔ n ≤ l ∧ l < m :=
+by { rintro ⟨n, hn⟩ ⟨m, hm⟩ ⟨l, hl⟩, simp [pnat.Ico] }
 
 @[simp] lemma Ico.card (l u : ℕ+) : (Ico l u).card = u - l := by simp [pnat.Ico]