refactor(data/set/finite): change type of set.finite.dependent_image (#6475)

The old lemma combined a statement similar to `set.finite.image` with
`set.finite.subset`. The new statement is a direct generalization of
`set.finite.image`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: urkud

src/analysis/analytic/composition.lean

@@ -590,8 +590,8 @@ end
 power series, here given a a finset.
 See also `comp_partial_sum`. -/
 def comp_partial_sum_target (m M N : ℕ) : finset (Σ n, composition n) :=
-set.finite.to_finset $ (finset.finite_to_set _).dependent_image
-  (comp_partial_sum_target_subset_image_comp_partial_sum_source m M N)
+set.finite.to_finset $ ((finset.finite_to_set _).dependent_image _).subset $
+  comp_partial_sum_target_subset_image_comp_partial_sum_source m M N
 
 @[simp] lemma mem_comp_partial_sum_target_iff {m M N : ℕ} {a : Σ n, composition n} :
   a ∈ comp_partial_sum_target m M N ↔

src/data/set/finite.lean

@@ -274,16 +274,12 @@ theorem infinite_of_infinite_image (f : α → β) {s : set α} (hs : (f '' s).i
   s.infinite :=
 mt (finite.image f) hs
 
-lemma finite.dependent_image {s : set α} (hs : finite s) {F : Π i ∈ s, β} {t : set β}
-  (H : ∀ y ∈ t, ∃ x (hx : x ∈ s), y = F x hx) : set.finite t :=
+lemma finite.dependent_image {s : set α} (hs : finite s) (F : Π i ∈ s, β) :
+  finite {y : β | ∃ x (hx : x ∈ s), y = F x hx} :=
 begin
-  let G : s → β := λ x, F x.1 x.2,
-  have A : t ⊆ set.range G,
-  { assume y hy,
-    rcases H y hy with ⟨x, hx, xy⟩,
-    refine ⟨⟨x, hx⟩, xy.symm⟩ },
-  letI : fintype s := finite.fintype hs,
-  exact (finite_range G).subset A
+  letI : fintype s := hs.fintype,
+  convert finite_range (λ x : s, F x x.2),
+  simp only [set_coe.exists, subtype.coe_mk, eq_comm],
 end
 
 instance fintype_map {α β} [decidable_eq β] :