-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_attach_eq_prod_dite [Fintype α] (s : Finset α) (f : s → β) [DecidablePred (· ∈ s)] :
    ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Proof state:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ x ∈ (filter (fun x => x ∈ s) univ).attach, f ⟨↑x, ⋯⟩

Tactic:
congr

Result:
case h.e_1.e_p
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun x => x ∈ s) = fun x => x ∈ filter (fun x => x ∈ s) univ

case h.e_4.e_2.h
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ s = filter (fun x => x ∈ s) univ

case h.e_5
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ HEq (fun i => f i) fun x => f ⟨↑x, ⋯⟩

Proof state:
case h.e_5
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ HEq (fun i => f i) fun x => f ⟨↑x, ⋯⟩

Tactic:
apply Function.hfunext <;> simp +contextual [Subtype.heq_iff_coe_eq]

Result:
no goals

Proof state:
case h.e_4.e_2.h.h
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ filter (fun x => x ∈ s) univ

Tactic:
simp

Result:
no goals

Proof state:
case h.e_1.e_p.h.a
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ filter (fun x => x ∈ s) univ

Tactic:
simp

Result:
no goals

Proof state:
case h.e_4.e_2.h
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ s = filter (fun x => x ∈ s) univ

Tactic:
ext

Result:
case h.e_4.e_2.h.h
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ filter (fun x => x ∈ s) univ

Proof state:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ i : α, if h : i ∈ s then f ⟨i, h⟩ else 1

Tactic:
rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]

Result:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ x ∈ (filter (fun x => x ∈ s) univ).attach, f ⟨↑x, ⋯⟩

Proof state:
case h.e_1.e_p
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun x => x ∈ s) = fun x => x ∈ filter (fun x => x ∈ s) univ

Tactic:
ext

Result:
case h.e_1.e_p.h.a
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
inst✝¹ : Fintype α
s : Finset α
f : { x // x ∈ s } → β
inst✝ : DecidablePred fun x => x ∈ s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ filter (fun x => x ∈ s) univ