ι : Type ?u.317398
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst
f : γ × α → β
⊢ ∏ p in r, f p = ∏ x in Finset.sigma s t, f (x.fst, x.snd)
ι : Type ?u.317398
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst
f : γ × α → β
⊢ ∏ p in r, f p = ∏ c in s, ∏ a in t c, f (c, a)
refine' Eq.trans _ (prod_sigma s t fun p => f (p.1, p.2))
no goals
ι : Type ?u.317398
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst
f : γ × α → β
⊢ ∏ p in r, f p = ∏ x in Finset.sigma s t, f (x.fst, x.snd)
exact
  prod_bij' (fun p _hp => ⟨p.1, p.2⟩) (fun p => mem_sigma.mpr ∘ (h p).mp)
    (fun p hp => congr_arg f Prod.mk.eta.symm) (fun p _hp => (p.1, p.2))
    (fun p => (h (p.1, p.2)).mpr ∘ mem_sigma.mp) (fun p _hp => Prod.mk.eta) fun p _hp => p.eta