no goals
α : 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
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
no goals
α : 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
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
no goals
α : 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
rw [map_some_eraseNone]