feat(Data/Finset/Image): add image_comp and image_comp_image (leanprover-community#39533)

The statement `image_comp` is worth adding because it matches the Set version, and also is more useful for rewriting in the forward direction.

Author: b-mehta

Mathlib/Data/Finset/Image.lean

@@ -349,6 +349,17 @@ theorem image_id' [DecidableEq α] : (s.image fun x => x) = s :=
 theorem image_image [DecidableEq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f) :=
   eq_of_veq <| by simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]
 
+/-- Reverse of `Finset.image_image`. The `Finset` analogue of `Set.image_comp`. -/
+theorem image_comp [DecidableEq γ] {g : β → γ} : s.image (g ∘ f) = (s.image f).image g :=
+  image_image.symm
+
+/-- Point-free form of `Finset.image_image`: `image` distributes over `Function.comp`. -/
+theorem image_comp_image [DecidableEq γ] {g : β → γ} :
+    image g ∘ image f = image (g ∘ f) := by ext s; simp [image_image]
+
+theorem image_comp_eq [DecidableEq γ] {g : β → γ} :
+    image (g ∘ f) = image g ∘ image f := image_comp_image.symm
+
 theorem image_comm {β'} [DecidableEq β'] [DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'}
     {g' : β' → γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
     (s.image g).image f = (s.image f').image g' := by simp_rw [image_image, comp_def, h_comm]

Mathlib/Data/Set/Image.lean

@@ -219,6 +219,8 @@ theorem image_comp (f : β → γ) (g : α → β) (a : Set α) : f ∘ g '' a =
 
 theorem image_comp_eq {g : β → γ} : image (g ∘ f) = image g ∘ image f := by grind
 
+theorem image_comp_image {g : β → γ} : image g ∘ image f = image (g ∘ f) := by grind
+
 /-- A variant of `image_comp`, useful for rewriting -/
 @[grind =]
 theorem image_image (g : β → γ) (f : α → β) (s : Set α) : g '' f '' s = (fun x => g (f x)) '' s :=