-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_finset_product' [DecidableEq α] [DecidableEq β] (s : Finset (α × β))
    (f : α × β → M) :
    (∏ᶠ (ab) (_ : ab ∈ s), f ab) =
      ∏ᶠ (a) (b) (_ : b ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)

Tactic:
simp_rw [finprod_mem_finset_eq_prod, this]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α), (Finset.filter (fun ab => ab.1 = a) s).prod f

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α), (Finset.filter (fun ab => ab.1 = a) s).prod f

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _
    (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst),
  ← Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∀ i ∈ s, ∃ a ∈ s, a.1 = i.1

Tactic:
exact fun x hx => ⟨x, hx, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)

Tactic:
rw [finprod_mem_finset_eq_prod]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s

Tactic:
simp only [Finset.mem_image]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
      (Finset.filter (fun x => x.1 = a) s).prod f
⊢ ∀ i ∈ s, ∃ a ∈ s, a.1 = i.1

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) =
    (Finset.filter (fun x => x.1 = a) s).prod f

Tactic:
refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop

Result:
no goals