[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Finset γ
f : γ → α
g : γ → β
this : DecidableEq γ
⊢ ∀ ⦃a : γ⦄ {s : Finset γ},
    ¬a ∈ s →
      (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x) →
        (∏ x in insert a s, f x, ∏ x in insert a s, g x) = ∏ x in insert a s, (f x, g x)
[PROOFSTEP]
simp (config := { contextual := true }) [Prod.ext_iff]
[GOAL]
I : Type u_1
inst✝² : DecidableEq I
Z : I → Type u_2
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
⊢ ∏ i : I, Pi.mulSingle i (f i) = f
[PROOFSTEP]
ext a
[GOAL]
case h
I : Type u_1
inst✝² : DecidableEq I
Z : I → Type u_2
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
a : I
⊢ Finset.prod univ (fun i => Pi.mulSingle i (f i)) a = f a
[PROOFSTEP]
simp
[GOAL]
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
⊢ g = h
[PROOFSTEP]
cases nonempty_fintype I
[GOAL]
case intro
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
val✝ : Fintype I
⊢ g = h
[PROOFSTEP]
ext k
[GOAL]
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ ↑g k = ↑h k
[PROOFSTEP]
rw [← Finset.univ_prod_mulSingle k, g.map_prod, h.map_prod]
[GOAL]
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ ∏ x : I, ↑g (Pi.mulSingle x (k x)) = ∏ x : I, ↑h (Pi.mulSingle x (k x))
[PROOFSTEP]
simp only [H]
