chore(Logic/Basic): deprecate Classical.subtype_of_exists

Also golf its only use in the library.

Author: urkud

Mathlib/Logic/Basic.lean

@@ -1031,7 +1031,11 @@ theorem some_spec₂ {α : Sort*} {p : α → Prop} {h : ∃ a, p a} (q : α →
     (hpq : ∀ a, p a → q a) : q (choose h) := hpq _ <| choose_spec _
 #align classical.some_spec2 Classical.some_spec₂
 
-/-- A version of `Classical.indefiniteDescription` which is definitionally equal to a pair -/
+/-- A version of `Classical.indefiniteDescription` which is definitionally equal to a pair.
+
+In Lean 4, this definition is defeq to `Classical.indefiniteDescription`,
+so it is deprecated. -/
+@[deprecated Classical.indefiniteDescription (since := "2024-07-04")]
 noncomputable def subtype_of_exists {α : Type*} {P : α → Prop} (h : ∃ x, P x) : { x // P x } :=
   ⟨Classical.choose h, Classical.choose_spec h⟩
 #align classical.subtype_of_exists Classical.subtype_of_exists
@@ -1041,7 +1045,7 @@ protected noncomputable def byContradiction' {α : Sort*} (H : ¬(α → False))
   Classical.choice <| (peirce _ False) fun h ↦ (H fun a ↦ h ⟨a⟩).elim
 #align classical.by_contradiction' Classical.byContradiction'
 
-/-- `classical.byContradiction'` is equivalent to lean's axiom `classical.choice`. -/
+/-- `Classical.byContradiction'` is equivalent to lean's axiom `Classical.choice`. -/
 def choice_of_byContradiction' {α : Sort*} (contra : ¬(α → False) → α) : Nonempty α → α :=
   fun H ↦ contra H.elim
 #align classical.choice_of_by_contradiction' Classical.choice_of_byContradiction'

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -2168,15 +2168,9 @@ theorem mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β
 
 theorem mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β)
     (h : s ⊆ range f) : lift.{u} #s ≤ lift.{v} #(f ⁻¹' s) := by
-  rw [lift_mk_le.{0}]
-  refine ⟨⟨?_, ?_⟩⟩
-  · rintro ⟨y, hy⟩
-    rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩
-    exact ⟨x, hy⟩
-  rintro ⟨y, hy⟩ ⟨y', hy'⟩; dsimp
-  rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩
-  rcases Classical.subtype_of_exists (h hy') with ⟨x', rfl⟩
-  simp; intro hxx'; rw [hxx']
+  rw [← image_preimage_eq_iff] at h
+  nth_rewrite 1 [← h]
+  apply mk_image_le_lift
 #align cardinal.mk_preimage_of_subset_range_lift Cardinal.mk_preimage_of_subset_range_lift
 
 theorem mk_preimage_of_injective_of_subset_range_lift {β : Type v} (f : α → β) (s : Set β)