α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x)) *
      ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) =
    (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ a : α, dite (p a) (f a) (g a) = (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
simp only [prod_dite, attach_eq_univ]
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x) = ∏ a : { a // p a }, f ↑a (_ : p ↑a)

case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) = ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x)) *
      ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) =
    (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
congr 1
no goals
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x) = ∏ a : { a // p a }, f ↑a (_ : p ↑a)
exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // p x } => f x x.2
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => p x) univ ↔ p x
simp
no goals
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) = ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // ¬p x } => g x x.2
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.60200
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => ¬p x) univ ↔ ¬p x
simp