feat(data/set): replace set_coe.can_lift by subtype.can_lift (#14792

)
leanprover-community · Jun 23, 2022 · c3e3d1a · c3e3d1a
1 parent 4de20c5
commit c3e3d1a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
@@ -115,11 +115,6 @@ instance pi_set_coe.can_lift' (ι : Type u) (α : Type v) [ne : nonempty α] (s
   can_lift (s → α) (ι → α) :=
 pi_set_coe.can_lift ι (λ _, α) s
 
-instance set_coe.can_lift (s : set α) : can_lift α s :=
-{ coe := coe,
-  cond := λ a, a ∈ s,
-  prf := λ a ha, ⟨⟨a, ha⟩, rfl⟩ }
-
 end set
 
 section set_coe

diff --git a/src/tactic/lift.lean b/src/tactic/lift.lean
@@ -71,6 +71,11 @@ instance pi_subtype.can_lift' (ι : Sort*) (α : Sort*) [ne : nonempty α] (p :
   can_lift (subtype p → α) (ι → α) :=
 pi_subtype.can_lift ι (λ _, α) p
 
+instance subtype.can_lift {α : Sort*} (p : α → Prop) : can_lift α {x // p x} :=
+{ coe := coe,
+  cond := p,
+  prf := λ a ha, ⟨⟨a, ha⟩, rfl⟩ }
+
 namespace tactic
 
 /--