no goals
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i : ι
y : { x // x ∈ H i }
⊢ ↑(noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y
apply MonoidHom.noncommPiCoprod_mulSingle