-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_apply_dite {s : Finset α} {p : α → Prop} {hp : DecidablePred p}
    [DecidablePred fun x => ¬p x] (f : ∀ x : α, p x → γ) (g : ∀ x : α, ¬p x → γ) (h : γ → β) :
    (∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) =
      (∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) *
        ∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2) :=
  calc
    (∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) =
        (∏ x ∈ s with p x, h (if hx : p x then f x hx else g x hx)) *
          ∏ x ∈ s with ¬p x, h (if hx : p x then f x hx else g x hx) :=
      (prod_filter_mul_prod_filter_not s p _).symm
    _ = (∏ x : {x ∈ s | p x}, h (if hx : p x.1 then f x.1 hx else g x.1 hx)) *
          ∏ x : {x ∈ s | ¬p x}, h (if hx : p x.1 then f x.1 hx else g x.1 hx) :=
      congr_arg₂ _ (prod_attach _ _).symm (prod_attach _ _).symm
    _ = (∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) *
          ∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2) :=
      congr_arg₂ _ (prod_congr rfl fun x _hx ↦
        congr_arg h (dif_pos <| by simpa using (mem_filter.mp x.2).2))
        (prod_congr rfl fun x _hx => congr_arg h (dif_neg <| by simpa using (mem_filter.mp x.2).2))

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
inst✝ : DecidablePred fun x => ¬p x
f : (x : α) → p x → γ
g : (x : α) → ¬p x → γ
h : γ → β
x : { x // x ∈ filter (fun x => ¬p x) s }
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
inst✝ : DecidablePred fun x => ¬p x
f : (x : α) → p x → γ
g : (x : α) → ¬p x → γ
h : γ → β
x : { x // x ∈ filter (fun x => p x) s }
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
inst✝ : DecidablePred fun x => ¬p x
f : (x : α) → p x → γ
g : (x : α) → ¬p x → γ
h : γ → β
x : { x // x ∈ filter (fun x => p x) s }
_hx : x ∈ univ
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
inst✝ : DecidablePred fun x => ¬p x
f : (x : α) → p x → γ
g : (x : α) → ¬p x → γ
h : γ → β
x : { x // x ∈ filter (fun x => p x) s }
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
inst✝ : DecidablePred fun x => ¬p x
f : (x : α) → p x → γ
g : (x : α) → ¬p x → γ
h : γ → β
x : { x // x ∈ filter (fun x => ¬p x) s }
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
inst✝ : DecidablePred fun x => ¬p x
f : (x : α) → p x → γ
g : (x : α) → ¬p x → γ
h : γ → β
x : { x // x ∈ filter (fun x => ¬p x) s }
_hx : x ∈ univ
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals