case intro
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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
cases nonempty_fintype I
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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
case intro
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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
ext k
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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))
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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
rw [← Finset.univ_prod_mulSingle k, g.map_prod, h.map_prod]
no goals
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_3
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_2
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))
simp only [H]