Geometry Bound set finite

lemma geometryBound_set_finite :    Set.Finite      { max 1 (∑ i ∈ I, i * a i + ∑ i ∈ I', i * b i + ∑ i ∈ I'', i * c i) -        (∑ i ∈ I, a i + ∑ i ∈ I', b i + ∑ i ∈ I'', c i) |        (I ⊆ Finset.Icc 1 d) (I' ⊆ Finset.Icc 1 d) (I'' ⊆ Finset.Icc 1 d) } := by  let f (I I' I'' : Finset ℕ) : ℝ :=    max 1 (∑ i ∈ I, i * a i + ∑ i ∈ I', i * b i + ∑ i ∈ I'', i * c i) -        (∑ i ∈ I, a i + ∑ i ∈ I', b i + ∑ i ∈ I'', c i)  have : { f I I' I'' | (I ⊆ Finset.Icc 1 d) (I' ⊆ Finset.Icc 1 d) (I'' ⊆ Finset.Icc 1 d) } =      (fun x ↦ f x.1 x.2.1 x.2.2) ''        ((Finset.Icc 1 d).powerset ×ˢ (Finset.Icc 1 d).powerset ×ˢ (Finset.Icc 1 d).powerset) := by    ext y    simp only [Set.mem_setOf_eq, Set.mem_image, Set.mem_prod, Finset.mem_coe, Finset.mem_powerset,      Prod.exists]    constructor    · rintro ⟨I, hI, I', hI', I'', hI'', rfl⟩      exact ⟨I, I', I'', ⟨hI, hI', hI''⟩, rfl⟩    · rintro ⟨I, I', I'', ⟨hI, hI', hI''⟩, rfl⟩      exact ⟨I, hI, I', hI', I'', hI'', rfl⟩  rw [this]  exact Set.Finite.image _ (Set.toFinite _)