Attached lists and list-to-finset products

Two facts used wherever a proof enumerates a finite set as a list and then maps or multiplies over it: mapping a function defined on the attached subtype agrees with mapping the total function, and a list product is the finset product of the finset the list enumerates.

theorem RS.attachWith_map_eq {β : Type u_1} {γ : Type u_2} {p : β → Prop} (fsub : { g : β // p g } → γ) (ftot : β → γ) (hpt : ∀ (g : β) (hg : p g), fsub ⟨g, hg⟩ = ftot g) (l : List β) (H : ∀ g ∈ l, p g) : List.map fsub (l.attachWith p H) = List.map ftot l

Mapping over an attached list agrees with mapping the total function, when the two agree pointwise.

theorem RS.list_map_prod_eq_finset_prod {β : Type u_1} {M : Type u_2} [CommMonoid M] (s : Finset β) (l : List β) (hl : ↑l = s.val) (f : β → M) : (List.map f l).prod = ∏ g ∈ s, f g

A list product is the finset product of the finset the list enumerates.