[Merged by Bors] - feat: port CanLift instances for PNat

Mathlib/Data/PNat/Basic.lean

@@ -410,7 +410,6 @@ theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) := by
     | succ n =>
       use ⟨n.succ, n.succ_pos⟩
       rw [← coe_inj, h, mul_coe, mk_coe]
-      exact k.property
 #align pnat.dvd_iff PNat.dvd_iff
 
 theorem dvd_iff' {k m : ℕ+} : k ∣ m ↔ mod m k = k := by

Mathlib/Data/PNat/Defs.lean

@@ -11,6 +11,8 @@ Authors: Mario Carneiro, Neil Strickland
 
 import Mathlib.Algebra.NeZero
 import Mathlib.Order.Basic
+import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Lift
 
 /-!
 # The positive natural numbers
@@ -33,8 +35,12 @@ notation "ℕ+" => PNat
 instance : One ℕ+ :=
   ⟨⟨1, Nat.zero_lt_one⟩⟩
 
+/-- The underlying natural number -/
+@[coe]
+def PNat.val : ℕ+ → ℕ := Subtype.val
+
 instance coePNatNat : Coe ℕ+ ℕ :=
-  ⟨Subtype.val⟩
+  ⟨PNat.val⟩
 #align coe_pnat_nat coePNatNat
 
 instance : Repr ℕ+ :=
@@ -46,8 +52,9 @@ instance (n : ℕ) : OfNat ℕ+ (n+1) :=
 
 namespace PNat
 
+-- Note: similar to Subtype.coe_mk
 -- Porting note: no `simp` due to eagerly elaborated coercions
-theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n :=
+theorem mk_coe (n h) : (PNat.val (⟨n, h⟩ : ℕ+) : ℕ) = n :=
   rfl
 #align pnat.mk_coe PNat.mk_coe
 
@@ -284,20 +291,17 @@ def divExact (m k : ℕ+) : ℕ+ :=
 
 end PNat
 
--- Porting note: `lift` tactic is not implemented yet.
-/-
 section CanLift
 
-instance Nat.canLiftPNat : CanLift ℕ ℕ+ coe ((· < ·) 0) :=
+instance Nat.canLiftPNat : CanLift ℕ ℕ+ (↑) (fun n => 0 < n) :=
   ⟨fun n hn => ⟨Nat.toPNat' n, PNat.toPNat'_coe hn⟩⟩
 #align nat.can_lift_pnat Nat.canLiftPNat
 
-instance Int.canLiftPNat : CanLift ℤ ℕ+ coe ((· < ·) 0) :=
+instance Int.canLiftPNat : CanLift ℤ ℕ+ (↑) ((0 < ·)) :=
   ⟨fun n hn =>
     ⟨Nat.toPNat' (Int.natAbs n), by
-      rw [coe_coe, Nat.toPNat'_coe, if_pos (Int.nat_abs_pos_of_ne_zero hn.ne'),
-        Int.nat_abs_of_nonneg hn.le]⟩⟩
+      rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'), Int.ofNat_eq_coe,
+        Int.natAbs_of_nonneg hn.le]⟩⟩
 #align int.can_lift_pnat Int.canLiftPNat
 
 end CanLift
--/

Mathlib/Data/PNat/Find.lean

@@ -26,7 +26,7 @@ instance decidablePredExistsNat : DecidablePred fun n' : ℕ => ∃ (n : ℕ+)(_
   fun n' =>
   decidable_of_iff' (∃ h : 0 < n', p ⟨n', h⟩) <|
     Subtype.exists.trans <| by
-      simp_rw [Subtype.coe_mk, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']
+      simp_rw [mk_coe, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']
 #align pnat.decidable_pred_exists_nat PNat.decidablePredExistsNat
 
 --include h

test/lift.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.WithOne.Defs
 import Mathlib.Data.Set.Image
 import Mathlib.Data.List.Lemmas
 import Mathlib.Data.Rat.Defs
+import Mathlib.Data.PNat.Defs
 
 /-! Some tests of the `lift` tactic. -/
 
@@ -189,3 +190,21 @@ example (x : WithBot Unit) (h : x ≠ ⊥) : True := by
   guard_hyp x : Unit
   guard_hyp h : (x : WithBot Unit) ≠ ⊥
   trivial
+
+example (n : ℕ) (hn : 0 < n) : True := by
+  lift n to ℕ+
+  · guard_target =ₛ 0 < n
+    exact hn
+
+  guard_hyp n : ℕ+
+  guard_hyp hn : 0 < (n : ℕ)
+  trivial
+
+example (n : ℤ) (hn : 0 < n) : True := by
+  lift n to ℕ+
+  · guard_target =ₛ 0 < n
+    exact hn
+
+  guard_hyp n : ℕ+
+  guard_hyp hn : 0 < (n : ℤ)
+  trivial