α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a =
    ∏ a : β, ∏ s : { x // f x = a }, g (↑(Equiv.sigmaFiberEquiv f) { fst := a, snd := s })
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a = ∏ a : α, g a
rw [← (Equiv.sigmaFiberEquiv f).prod_comp, ← univ_sigma_univ, prod_sigma]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a =
    ∏ a : β, ∏ s : { x // f x = a }, g (↑(Equiv.sigmaFiberEquiv f) { fst := a, snd := s })
rfl