[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : Option α → M
s : Finset α
⊢ ∏ x in ↑insertNone s, f x = f none * ∏ x in s, f (some x)
[PROOFSTEP]
simp [insertNone]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x in ↑eraseNone s, f x = ∏ x in s, Option.elim' 1 f x
[PROOFSTEP]
classical calc
  ∏ x in eraseNone s, f x = ∏ x in (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
    (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
  _ = ∏ x in s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
  _ = ∏ x in s, Option.elim' 1 f x := prod_erase _ rfl
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x in ↑eraseNone s, f x = ∏ x in s, Option.elim' 1 f x
[PROOFSTEP]
calc
  ∏ x in eraseNone s, f x = ∏ x in (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
    (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
  _ = ∏ x in s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
  _ = ∏ x in s, Option.elim' 1 f x := prod_erase _ rfl
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x in map Embedding.some (↑eraseNone s), Option.elim' 1 f x = ∏ x in erase s none, Option.elim' 1 f x
[PROOFSTEP]
rw [map_some_eraseNone]
