/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot

! This file was ported from Lean 3 source module algebra.big_operators.pi
! leanprover-community/mathlib commit fa2309577c7009ea243cffdf990cd6c84f0ad497
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Card
import Mathlib.Algebra.Group.Prod
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Ring.Pi

/-!
# Big operators for Pi Types

This file contains theorems relevant to big operators in binary and arbitrary product
of monoids and groups
-/


open BigOperators

namespace Pi

@[
to_additive: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → AddMonoid (β a)] (a : α) (l : List ((a : α) → β a)),
  List.sum l a = List.sum (List.map (fun f => f a) l)
to_additive]
theorem 
list_prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Monoid (β a)] (a : α) (l : List ((a : α) → β a)),
  List.prod l a = List.prod (List.map (fun f => f a) l)
list_prod_apply {
α: Type ?u.2
α : 
Type _: Type (?u.2+1)
Type _} {
β: α → Type ?u.7
β : 
α: Type ?u.2
α → 
Type _: Type (?u.7+1)
Type _} [∀ 
a: ?m.11
a, 
Monoid: Type ?u.14 → Type ?u.14
Monoid (
β: α → Type ?u.7
β 
a: ?m.11
a)] (
a: α
a : 
α: Type ?u.2
α)
    (
l: List ((a : α) → β a)
l : 
List: Type ?u.20 → Type ?u.20
List (∀ 
a: ?m.22
a, 
β: α → Type ?u.7
β 
a: ?m.22
a)) : 
l: List ((a : α) → β a)
l.
prod: {α : Type ?u.29} → [inst : Mul α] → [inst : One α] → List α → α
prod 
a: α
a = (
l: List ((a : α) → β a)
l.
map: {α : Type ?u.1886} → {β : Type ?u.1885} → (α → β) → List α → List β
map fun 
f: (a : α) → β a
f : ∀ 
a: ?m.1895
a, 
β: α → Type ?u.7
β 
a: ?m.1895
a ↦ 
f: (a : α) → β a
f 
a: α
a).
prod: {α : Type ?u.1902} → [inst : Mul α] → [inst : One α] → List α → α
prod :=
  (
evalMonoidHom: {I : Type ?u.2513} → (f : I → Type ?u.2512) → [inst : (i : I) → MulOneClass (f i)] → (i : I) → ((i : I) → f i) →* f i
evalMonoidHom 
β: α → Type u_2
β 
a: α
a).
map_list_prod: ∀ {M : Type ?u.3156} {N : Type ?u.3157} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (l : List M),
  ↑f (List.prod l) = List.prod (List.map (↑f) l)
map_list_prod 
_: List ?m.3164
_
#align pi.list_prod_apply 
Pi.list_prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Monoid (β a)] (a : α) (l : List ((a : α) → β a)),
  List.prod l a = List.prod (List.map (fun f => f a) l)
Pi.list_prod_apply
#align pi.list_sum_apply 
Pi.list_sum_apply: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → AddMonoid (β a)] (a : α) (l : List ((a : α) → β a)),
  List.sum l a = List.sum (List.map (fun f => f a) l)
Pi.list_sum_apply

@[
to_additive: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → AddCommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)),
  Multiset.sum s a = Multiset.sum (Multiset.map (fun f => f a) s)
to_additive]
theorem 
multiset_prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → CommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)),
  Multiset.prod s a = Multiset.prod (Multiset.map (fun f => f a) s)
multiset_prod_apply {
α: Type ?u.3356
α : 
Type _: Type (?u.3356+1)
Type _} {
β: α → Type ?u.3361
β : 
α: Type ?u.3356
α → 
Type _: Type (?u.3361+1)
Type _} [∀ 
a: ?m.3365
a, 
CommMonoid: Type ?u.3368 → Type ?u.3368
CommMonoid (
β: α → Type ?u.3361
β 
a: ?m.3365
a)] (
a: α
a : 
α: Type ?u.3356
α)
    (
s: Multiset ((a : α) → β a)
s : 
Multiset: Type ?u.3374 → Type ?u.3374
Multiset (∀ 
a: ?m.3376
a, 
β: α → Type ?u.3361
β 
a: ?m.3376
a)) : 
s: Multiset ((a : α) → β a)
s.
prod: {α : Type ?u.3383} → [inst : CommMonoid α] → Multiset α → α
prod 
a: α
a = (
s: Multiset ((a : α) → β a)
s.
map: {α : Type ?u.3445} → {β : Type ?u.3444} → (α → β) → Multiset α → Multiset β
map fun 
f: (a : α) → β a
f : ∀ 
a: ?m.3454
a, 
β: α → Type ?u.3361
β 
a: ?m.3454
a ↦ 
f: (a : α) → β a
f 
a: α
a).
prod: {α : Type ?u.3461} → [inst : CommMonoid α] → Multiset α → α
prod :=
  (
evalMonoidHom: {I : Type ?u.3489} → (f : I → Type ?u.3488) → [inst : (i : I) → MulOneClass (f i)] → (i : I) → ((i : I) → f i) →* f i
evalMonoidHom 
β: α → Type u_2
β 
a: α
a).
map_multiset_prod: ∀ {α : Type ?u.4386} {β : Type ?u.4387} [inst : CommMonoid α] [inst_1 : CommMonoid β] (f : α →* β) (s : Multiset α),
  ↑f (Multiset.prod s) = Multiset.prod (Multiset.map (↑f) s)
map_multiset_prod 
_: Multiset ?m.4394
_
#align pi.multiset_prod_apply 
Pi.multiset_prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → CommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)),
  Multiset.prod s a = Multiset.prod (Multiset.map (fun f => f a) s)
Pi.multiset_prod_apply
#align pi.multiset_sum_apply 
Pi.multiset_sum_apply: ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → AddCommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)),
  Multiset.sum s a = Multiset.sum (Multiset.map (fun f => f a) s)
Pi.multiset_sum_apply

end Pi

@[
to_additive: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → AddCommMonoid (β a)] (a : α) (s : Finset γ)
  (g : γ → (a : α) → β a), Finset.sum s (fun c => g c) a = ∑ c in s, g c a
to_additive (attr:=simp)]
theorem 
Finset.prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → CommMonoid (β a)] (a : α) (s : Finset γ)
  (g : γ → (a : α) → β a), Finset.prod s (fun c => g c) a = ∏ c in s, g c a
Finset.prod_apply {
α: Type u_1
α : 
Type _: Type (?u.4567+1)
Type _} {
β: α → Type u_2
β : 
α: Type ?u.4567
α → 
Type _: Type (?u.4572+1)
Type _} {
γ: ?m.4575
γ} [∀ 
a: ?m.4579
a, 
CommMonoid: Type ?u.4582 → Type ?u.4582
CommMonoid (
β: α → Type ?u.4572
β 
a: ?m.4579
a)] (
a: α
a : 
α: Type ?u.4567
α)
    (
s: Finset γ
s : 
Finset: Type ?u.4588 → Type ?u.4588
Finset 
γ: ?m.4575
γ) (
g: γ → (a : α) → β a
g : 
γ: ?m.4575
γ → ∀ 
a: ?m.4594
a, 
β: α → Type ?u.4572
β 
a: ?m.4594
a) : (∏ 
c: ?m.4608
c in 
s: Finset γ
s, 
g: γ → (a : α) → β a
g 
c: ?m.4608
c) 
a: α
a = ∏ 
c: ?m.4676
c in 
s: Finset γ
s, 
g: γ → (a : α) → β a
g 
c: ?m.4676
c 
a: α
a :=
  (
Pi.evalMonoidHom: {I : Type ?u.4703} → (f : I → Type ?u.4702) → [inst : (i : I) → MulOneClass (f i)] → (i : I) → ((i : I) → f i) →* f i
Pi.evalMonoidHom 
β: α → Type u_2
β 
a: α
a).
map_prod: ∀ {β : Type ?u.5602} {α : Type ?u.5601} {γ : Type ?u.5600} [inst : CommMonoid β] [inst_1 : CommMonoid γ] (g : β →* γ)
  (f : α → β) (s : Finset α), ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod 
_: ?m.5612 → ?m.5611
_ 
_: Finset ?m.5612
_
#align finset.prod_apply 
Finset.prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → CommMonoid (β a)] (a : α) (s : Finset γ)
  (g : γ → (a : α) → β a), Finset.prod s (fun c => g c) a = ∏ c in s, g c a
Finset.prod_apply
#align finset.sum_apply 
Finset.sum_apply: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → AddCommMonoid (β a)] (a : α) (s : Finset γ)
  (g : γ → (a : α) → β a), Finset.sum s (fun c => g c) a = ∑ c in s, g c a
Finset.sum_apply

/-- An 'unapplied' analogue of `Finset.prod_apply`. -/
@[
to_additive: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → AddCommMonoid (β a)] (s : Finset γ)
  (g : γ → (a : α) → β a), ∑ c in s, g c = fun a => ∑ c in s, g c a
to_additive "An 'unapplied' analogue of `Finset.sum_apply`."]
theorem 
Finset.prod_fn: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → CommMonoid (β a)] (s : Finset γ)
  (g : γ → (a : α) → β a), ∏ c in s, g c = fun a => ∏ c in s, g c a
Finset.prod_fn {
α: Type u_1
α : 
Type _: Type (?u.5852+1)
Type _} {
β: α → Type u_2
β : 
α: Type ?u.5852
α → 
Type _: Type (?u.5857+1)
Type _} {
γ: ?m.5860
γ} [∀ 
a: ?m.5864
a, 
CommMonoid: Type ?u.5867 → Type ?u.5867
CommMonoid (
β: α → Type ?u.5857
β 
a: ?m.5864
a)] (
s: Finset γ
s : 
Finset: Type ?u.5871 → Type ?u.5871
Finset 
γ: ?m.5860
γ)
    (
g: γ → (a : α) → β a
g : 
γ: ?m.5860
γ → ∀ 
a: ?m.5877
a, 
β: α → Type ?u.5857
β 
a: ?m.5877
a) : (∏ 
c: ?m.5891
c in 
s: Finset γ
s, 
g: γ → (a : α) → β a
g 
c: ?m.5891
c) = fun 
a: ?m.5953
a ↦ ∏ 
c: ?m.5962
c in 
s: Finset γ
s, 
g: γ → (a : α) → β a
g 
c: ?m.5962
c 
a: ?m.5953
a :=
  
funext: ∀ {α : Sort ?u.5992} {β : α → Sort ?u.5991} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
_: ?m.6007
_ ↦ 
Finset.prod_apply: ∀ {α : Type ?u.6009} {β : α → Type ?u.6010} {γ : Type ?u.6011} [inst : (a : α) → CommMonoid (β a)] (a : α)
  (s : Finset γ) (g : γ → (a : α) → β a), Finset.prod s (fun c => g c) a = ∏ c in s, g c a
Finset.prod_apply 
_: ?m.6012
_ 
_: Finset ?m.6014
_ 
_: ?m.6014 → (a : ?m.6012) → ?m.6013 a
_
#align finset.prod_fn 
Finset.prod_fn: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → CommMonoid (β a)] (s : Finset γ)
  (g : γ → (a : α) → β a), ∏ c in s, g c = fun a => ∏ c in s, g c a
Finset.prod_fn
#align finset.sum_fn 
Finset.sum_fn: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → AddCommMonoid (β a)] (s : Finset γ)
  (g : γ → (a : α) → β a), ∑ c in s, g c = fun a => ∑ c in s, g c a
Finset.sum_fn

@[
to_additive: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : Fintype γ] [inst_1 : (a : α) → AddCommMonoid (β a)] (a : α)
  (g : γ → (a : α) → β a), Finset.sum Finset.univ (fun c => g c) a = ∑ c : γ, g c a
to_additive]
theorem 
Fintype.prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : Fintype γ] [inst_1 : (a : α) → CommMonoid (β a)] (a : α)
  (g : γ → (a : α) → β a), Finset.prod Finset.univ (fun c => g c) a = ∏ c : γ, g c a
Fintype.prod_apply {
α: Type u_1
α : 
Type _: Type (?u.6174+1)
Type _} {
β: α → Type ?u.6179
β : 
α: Type ?u.6174
α → 
Type _: Type (?u.6179+1)
Type _} {
γ: Type u_3
γ : 
Type _: Type (?u.6182+1)
Type _} [
Fintype: Type ?u.6185 → Type ?u.6185
Fintype 
γ: Type ?u.6182
γ]
    [∀ 
a: ?m.6189
a, 
CommMonoid: Type ?u.6192 → Type ?u.6192
CommMonoid (
β: α → Type ?u.6179
β 
a: ?m.6189
a)] (
a: α
a : 
α: Type ?u.6174
α) (
g: γ → (a : α) → β a
g : 
γ: Type ?u.6182
γ → ∀ 
a: ?m.6201
a, 
β: α → Type ?u.6179
β 
a: ?m.6201
a) : (∏ 
c: ?m.6265
c, 
g: γ → (a : α) → β a
g 
c: ?m.6265
c) 
a: α
a = ∏ 
c: ?m.6389
c, 
g: γ → (a : α) → β a
g 
c: ?m.6389
c 
a: α
a :=
  
Finset.prod_apply: ∀ {α : Type ?u.6415} {β : α → Type ?u.6416} {γ : Type ?u.6417} [inst : (a : α) → CommMonoid (β a)] (a : α)
  (s : Finset γ) (g : γ → (a : α) → β a), Finset.prod s (fun c => g c) a = ∏ c in s, g c a
Finset.prod_apply 
a: α
a 
Finset.univ: {α : Type ?u.6422} → [inst : Fintype α] → Finset α
Finset.univ 
g: γ → (a : α) → β a
g
#align fintype.prod_apply 
Fintype.prod_apply: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : Fintype γ] [inst_1 : (a : α) → CommMonoid (β a)] (a : α)
  (g : γ → (a : α) → β a), Finset.prod Finset.univ (fun c => g c) a = ∏ c : γ, g c a
Fintype.prod_apply
#align fintype.sum_apply 
Fintype.sum_apply: ∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : Fintype γ] [inst_1 : (a : α) → AddCommMonoid (β a)] (a : α)
  (g : γ → (a : α) → β a), Finset.sum Finset.univ (fun c => g c) a = ∑ c : γ, g c a
Fintype.sum_apply

@[to_additive 
prod_mk_sum: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] (s : Finset γ)
  (f : γ → α) (g : γ → β), (∑ x in s, f x, ∑ x in s, g x) = ∑ x in s, (f x, g x)
prod_mk_sum]
theorem 
prod_mk_prod: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] (s : Finset γ) (f : γ → α)
  (g : γ → β), (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x)
prod_mk_prod {
α: Type u_1
α 
β: Type ?u.6591
β 
γ: Type u_3
γ : 
Type _: Type (?u.6594+1)
Type _} [
CommMonoid: Type ?u.6597 → Type ?u.6597
CommMonoid 
α: Type ?u.6588
α] [
CommMonoid: Type ?u.6600 → Type ?u.6600
CommMonoid 
β: Type ?u.6591
β] (
s: Finset γ
s : 
Finset: Type ?u.6603 → Type ?u.6603
Finset 
γ: Type ?u.6594
γ) (
f: γ → α
f : 
γ: Type ?u.6594
γ → 
α: Type ?u.6588
α)
    (
g: γ → β
g : 
γ: Type ?u.6594
γ → 
β: Type ?u.6591
β) : (∏ 
x: ?m.6651
x in 
s: Finset γ
s, 
f: γ → α
f 
x: ?m.6651
x, ∏ 
x: ?m.6699
x in 
s: Finset γ
s, 
g: γ → β
g 
x: ?m.6699
x) = ∏ 
x: ?m.6723
x in 
s: Finset γ
s, (
f: γ → α
f 
x: ?m.6723
x, 
g: γ → β
g 
x: ?m.6723
x) :=
  haveI := 
Classical.decEq: (α : Sort ?u.6790) → DecidableEq α
Classical.decEq 
γ: Type u_3
γ
  
Finset.induction_on: ∀ {α : Type ?u.6796} {p : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
  p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, ¬a ∈ s → p s → p (insert a s)) → p s
Finset.induction_on 
s: Finset γ
s 
rfl: ∀ {α : Sort ?u.6866} {a : α}, a = a
rfl (by
Goals accomplished! 🐙 
α: 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)simp (config := { contextual := 
true: Bool
true }) [
Prod.ext_iff: ∀ {α : Type ?u.7045} {β : Type ?u.7046} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff]
Goals accomplished! 🐙)
#align prod_mk_prod 
prod_mk_prod: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] (s : Finset γ) (f : γ → α)
  (g : γ → β), (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x)
prod_mk_prod
#align prod_mk_sum 
prod_mk_sum: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] (s : Finset γ)
  (f : γ → α) (g : γ → β), (∑ x in s, f x, ∑ x in s, g x) = ∑ x in s, (f x, g x)
prod_mk_sum

section MulSingle

variable {
I: Type ?u.13588
I : 
Type _: Type (?u.13613+1)
Type _} [
DecidableEq: Sort ?u.13616 → Sort (max1?u.13616)
DecidableEq 
I: Type ?u.13613
I] {
Z: I → Type ?u.13602
Z : 
I: Type ?u.13613
I → 
Type _: Type (?u.17784+1)
Type _}

variable [∀ 
i: ?m.13631
i, 
CommMonoid: Type ?u.13634 → Type ?u.13634
CommMonoid  (
Z: I → Type ?u.13627
Z 
i: ?m.13606
i)]

@[
to_additive: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → AddCommMonoid (Z i)] [inst_2 : Fintype I]
  (f : (i : I) → Z i), ∑ i : I, Pi.single i (f i) = f
to_additive]
theorem 
Finset.univ_prod_mulSingle: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → CommMonoid (Z i)] [inst_2 : Fintype I]
  (f : (i : I) → Z i), ∏ i : I, Pi.mulSingle i (f i) = f
Finset.univ_prod_mulSingle [
Fintype: Type ?u.13638 → Type ?u.13638
Fintype 
I: Type ?u.13613
I] (
f: (i : I) → Z i
f : ∀ 
i: ?m.13642
i, 
Z: I → Type ?u.13627
Z 
i: ?m.13642
i) :
    (∏ 
i: ?m.13706
i, 
Pi.mulSingle: {I : Type ?u.13709} →
  {f : I → Type ?u.13708} → [inst : DecidableEq I] → [inst : (i : I) → One (f i)] → (i : I) → f i → (j : I) → f j
Pi.mulSingle 
i: ?m.13706
i (
f: (i : I) → Z i
f 
i: ?m.13706
i)) = 
f: (i : I) → Z i
f := by
Goals accomplished! 🐙
  
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) = fext 
a: ?α
a
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

h
Finset.prod univ (fun i => Pi.mulSingle i (f i)) a = f a
  
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) = fsimp
Goals accomplished! 🐙
#align finset.univ_prod_mul_single 
Finset.univ_prod_mulSingle: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → CommMonoid (Z i)] [inst_2 : Fintype I]
  (f : (i : I) → Z i), ∏ i : I, Pi.mulSingle i (f i) = f
Finset.univ_prod_mulSingle
#align finset.univ_sum_single 
Finset.univ_sum_single: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → AddCommMonoid (Z i)] [inst_2 : Fintype I]
  (f : (i : I) → Z i), ∑ i : I, Pi.single i (f i) = f
Finset.univ_sum_single

@[
to_additive: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → AddCommMonoid (Z i)] [inst_2 : Finite I]
  (G : Type u_2) [inst_3 : AddCommMonoid G] (g h : ((i : I) → Z i) →+ G),
  (∀ (i : I) (x : Z i), ↑g (Pi.single i x) = ↑h (Pi.single i x)) → g = h
to_additive]
theorem 
MonoidHom.functions_ext: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → CommMonoid (Z i)] [inst_2 : Finite I]
  (G : Type u_2) [inst_3 : CommMonoid G] (g h : ((i : I) → Z i) →* G),
  (∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)) → g = h
MonoidHom.functions_ext [
Finite: Sort ?u.17795 → Prop
Finite 
I: Type ?u.17770
I] (
G: Type ?u.17798
G : 
Type _: Type (?u.17798+1)
Type _) [
CommMonoid: Type ?u.17801 → Type ?u.17801
CommMonoid 
G: Type ?u.17798
G] (
g: ((i : I) → Z i) →* G
g 
h: ((i : I) → Z i) →* G
h : (∀ 
i: ?m.19246
i, 
Z: I → Type ?u.17784
Z 
i: ?m.19246
i) →* 
G: Type ?u.17798
G)
    (
H: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
H : ∀ 
i: ?m.19255
i 
x: ?m.19258
x, 
g: ((i : I) → Z i) →* G
g (
Pi.mulSingle: {I : Type ?u.26313} →
  {f : I → Type ?u.26312} → [inst : DecidableEq I] → [inst : (i : I) → One (f i)] → (i : I) → f i → (j : I) → f j
Pi.mulSingle 
i: ?m.19255
i 
x: ?m.19258
x) = 
h: ((i : I) → Z i) →* G
h (
Pi.mulSingle: {I : Type ?u.34535} →
  {f : I → Type ?u.34534} → [inst : DecidableEq I] → [inst : (i : I) → One (f i)] → (i : I) → f i → (j : I) → f j
Pi.mulSingle 
i: ?m.19255
i 
x: ?m.19258
x)) : 
g: ((i : I) → Z i) →* G
g = 
h: ((i : I) → Z i) →* G
h := by
Goals accomplished! 🐙
  
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 = hcases 
nonempty_fintype: ∀ (α : Type ?u.34687) [inst : Finite α], Nonempty (Fintype α)
nonempty_fintype 
I: Type u_1
I
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

intro
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 = hext 
k: ?M
k
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

intro.h
↑g k = ↑h k
  
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 = hrw [
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

intro.h
↑g k = ↑h k← 
Finset.univ_prod_mulSingle: ∀ {I : Type ?u.36099} [inst : DecidableEq I] {Z : I → Type ?u.36100} [inst_1 : (i : I) → CommMonoid (Z i)]
  [inst_2 : Fintype I] (f : (i : I) → Z i), ∏ i : I, Pi.mulSingle i (f i) = f
Finset.univ_prod_mulSingle 
k: ?M
k,
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

intro.h
↑g (∏ i : I, Pi.mulSingle i (k i)) = ↑h (∏ i : I, Pi.mulSingle i (k i)) 
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

intro.h
↑g k = ↑h k
g: ((i : I) → Z i) →* G
g.
map_prod: ∀ {β : Type ?u.36181} {α : Type ?u.36180} {γ : Type ?u.36179} [inst : CommMonoid β] [inst_1 : CommMonoid γ] (g : β →* γ)
  (f : α → β) (s : Finset α), ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod,
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

intro.h
∏ x : I, ↑g (Pi.mulSingle x (k x)) = ↑h (∏ i : I, Pi.mulSingle i (k i)) 
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

intro.h
↑g k = ↑h k
h: ((i : I) → Z i) →* G
h.
map_prod: ∀ {β : Type ?u.36376} {α : Type ?u.36375} {γ : Type ?u.36374} [inst : CommMonoid β] [inst_1 : CommMonoid γ] (g : β →* γ)
  (f : α → β) (s : Finset α), ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod
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

intro.h
∏ x : I, ↑g (Pi.mulSingle x (k x)) = ∏ x : I, ↑h (Pi.mulSingle x (k x))]
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

intro.h
∏ x : I, ↑g (Pi.mulSingle x (k x)) = ∏ x : I, ↑h (Pi.mulSingle x (k x))
  
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 = hsimp only [
H: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
H]
Goals accomplished! 🐙
#align monoid_hom.functions_ext 
MonoidHom.functions_ext: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → CommMonoid (Z i)] [inst_2 : Finite I]
  (G : Type u_2) [inst_3 : CommMonoid G] (g h : ((i : I) → Z i) →* G),
  (∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)) → g = h
MonoidHom.functions_ext
#align add_monoid_hom.functions_ext 
AddMonoidHom.functions_ext: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → AddCommMonoid (Z i)] [inst_2 : Finite I]
  (G : Type u_2) [inst_3 : AddCommMonoid G] (g h : ((i : I) → Z i) →+ G),
  (∀ (i : I) (x : Z i), ↑g (Pi.single i x) = ↑h (Pi.single i x)) → g = h
AddMonoidHom.functions_ext

/-- This is used as the ext lemma instead of `MonoidHom.functions_ext` for reasons explained in
note [partially-applied ext lemmas]. -/
@[
to_additive: ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → AddCommMonoid (Z i)] [inst_2 : Finite I]
  (M : Type u_2) [inst_3 : AddCommMonoid M] (g h : ((i : I) → Z i) →+ M),
  (∀ (i : I), AddMonoidHom.comp g (AddMonoidHom.single Z i) = AddMonoidHom.comp h (AddMonoidHom.single Z i)) → g = h
to_additive (attr := ext)
      "\nThis is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons
      explained in note [partially-applied ext lemmas]."]
theorem 
MonoidHom.functions_ext': ∀ [inst : Finite I] (M : Type u_2) [inst : CommMonoid M] (g h : ((i : I) → Z i) →* M),
  (∀ (i : I), comp g (single Z i) = comp h (single Z i)) → g = h
MonoidHom.functions_ext' [
Finite: Sort ?u.37310 → Prop
Finite 
I: Type ?u.37285
I] (
M: Type u_2
M : 
Type _: Type (?u.37313+1)
Type _) [
CommMonoid: Type ?u.37316 → Type ?u.37316
CommMonoid 
M: Type ?u.37313
M] (
g: ((i : I) → Z i) →* M
g 
h: ((i : I) → Z i) →* M
h : (∀ 
i: ?m.37322
i, 
Z: I → Type ?u.37299
Z 
i: ?m.38761
i) →* 
M: Type ?u.37313
M)
    (
H: ∀ (i : I), comp g (single Z i) = comp h (single Z i)
H : ∀ 
i: ?m.38770
i, 
g: ((i : I) → Z i) →* M
g.
comp: {M : Type ?u.38776} →
  {N : Type ?u.38775} →
    {P : Type ?u.38774} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp (
MonoidHom.single: {I : Type ?u.38797} →
  (f : I → Type ?u.38796) →
    [inst : DecidableEq I] → [inst : (i : I) → MulOneClass (f i)] → (i : I) → f i →* (i : I) → f i
MonoidHom.single 
Z: I → Type ?u.37299
Z 
i: ?m.38770
i) = 
h: ((i : I) → Z i) →* M
h.
comp: {M : Type ?u.40075} →
  {N : Type ?u.40074} →
    {P : Type ?u.40073} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp (
MonoidHom.single: {I : Type ?u.40092} →
  (f : I → Type ?u.40091) →
    [inst : DecidableEq I] → [inst : (i : I) → MulOneClass (f i)] → (i : I) → f i →* (i : I) → f i
MonoidHom.single 
Z: I → Type ?u.37299
Z 
i: ?m.38770
i)) : 
g: ((i : I) → Z i) →* M
g = 
h: ((i : I) → Z i) →* M
h :=
  
g: ((i : I) → Z i) →* M
g.
functions_ext: ∀ {I : Type ?u.40131} [inst : DecidableEq I] {Z : I → Type ?u.40133} [inst_1 : (i : I) → CommMonoid (Z i)]
  [inst_2 : Finite I] (G : Type ?u.40132) [inst_3 : CommMonoid G] (g h : ((i : I) → Z i) →* G),
  (∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)) → g = h
functions_ext 
M: Type u_2
M 
h: ((i : I) → Z i) →* M
h fun 
i: ?m.40249
i => 
FunLike.congr_fun: ∀ {F : Sort ?u.40251} {α : Sort ?u.40253} {β : α → Sort ?u.40252} [i : FunLike F α β] {f g : F},
  f = g → ∀ (x : α), ↑f x = ↑g x
FunLike.congr_fun (
H: ∀ (i : I), comp g (single Z i) = comp h (single Z i)
H 
i: ?m.40249
i)
#align monoid_hom.functions_ext' 
MonoidHom.functions_ext': ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → CommMonoid (Z i)] [inst_2 : Finite I]
  (M : Type u_2) [inst_3 : CommMonoid M] (g h : ((i : I) → Z i) →* M),
  (∀ (i : I), MonoidHom.comp g (MonoidHom.single Z i) = MonoidHom.comp h (MonoidHom.single Z i)) → g = h
MonoidHom.functions_ext'
#align add_monoid_hom.functions_ext' 
AddMonoidHom.functions_ext': ∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_3} [inst_1 : (i : I) → AddCommMonoid (Z i)] [inst_2 : Finite I]
  (M : Type u_2) [inst_3 : AddCommMonoid M] (g h : ((i : I) → Z i) →+ M),
  (∀ (i : I), AddMonoidHom.comp g (AddMonoidHom.single Z i) = AddMonoidHom.comp h (AddMonoidHom.single Z i)) → g = h
AddMonoidHom.functions_ext'

end MulSingle

section RingHom

open Pi

variable {
I: Type ?u.47778
I : 
Type _: Type (?u.47753+1)
Type _} [
DecidableEq: Sort ?u.47739 → Sort (max1?u.47739)
DecidableEq 
I: Type ?u.47736
I] {
f: I → Type ?u.47792
f : 
I: Type ?u.47753
I → 
Type _: Type (?u.47767+1)
Type _}

variable [∀ 
i: ?m.47796
i, 
NonAssocSemiring: Type ?u.47799 → Type ?u.47799
NonAssocSemiring (
f: I → Type ?u.47792
f 
i: ?m.47771
i)]

@[ext]
theorem 
RingHom.functions_ext: ∀ {I : Type u_1} [inst : DecidableEq I] {f : I → Type u_3} [inst_1 : (i : I) → NonAssocSemiring (f i)]
  [inst_2 : Finite I] (G : Type u_2) [inst_3 : NonAssocSemiring G] (g h : ((i : I) → f i) →+* G),
  (∀ (i : I) (x : f i), ↑g (single i x) = ↑h (single i x)) → g = h
RingHom.functions_ext [
Finite: Sort ?u.47803 → Prop
Finite 
I: Type ?u.47778
I] (
G: Type ?u.47806
G : 
Type _: Type (?u.47806+1)
Type _) [
NonAssocSemiring: Type ?u.47809 → Type ?u.47809
NonAssocSemiring 
G: Type ?u.47806
G] (
g: ((i : I) → f i) →+* G
g 
h: ((i : I) → f i) →+* G
h : (∀ 
i: ?m.47871
i, 
f: I → Type ?u.47792
f 
i: ?m.47871
i) →+* 
G: Type ?u.47806
G)
    (
H: ∀ (i : I) (x : f i), ↑g (single i x) = ↑h (single i x)
H : ∀ (
i: I
i : 
I: Type ?u.47778
I) (
x: f i
x : 
f: I → Type ?u.47792
f 
i: I
i), 
g: ((i : I) → f i) →+* G
g (
single: {I : Type ?u.54848} →
  {f : I → Type ?u.54847} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single 
i: I
i 
x: f i
x) = 
h: ((i : I) → f i) →+* G
h (
single: {I : Type ?u.62645} →
  {f : I → Type ?u.62644} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single 
i: I
i 
x: f i
x)) : 
g: ((i : I) → f i) →+* G
g = 
h: ((i : I) → f i) →+* G
h :=
  
RingHom.coe_addMonoidHom_injective: ∀ {α : Type ?u.62799} {β : Type ?u.62800} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β},
  Function.Injective fun f => ↑f
RingHom.coe_addMonoidHom_injective <|
    @
AddMonoidHom.functions_ext: ∀ {I : Type ?u.62817} [inst : DecidableEq I] {Z : I → Type ?u.62819} [inst_1 : (i : I) → AddCommMonoid (Z i)]
  [inst_2 : Finite I] (G : Type ?u.62818) [inst_3 : AddCommMonoid G] (g h : ((i : I) → Z i) →+ G),
  (∀ (i : I) (x : Z i), ↑g (single i x) = ↑h (single i x)) → g = h
AddMonoidHom.functions_ext 
I: Type ?u.47778
I _ 
f: I → Type ?u.47792
f _ _ 
G: Type u_2
G _ (
g: ((i : I) → f i) →+* G
g : (∀ 
i: ?m.62831
i, 
f: I → Type ?u.47792
f 
i: ?m.62831
i) →+ 
G: Type u_2
G) 
h: ((i : I) → f i) →+* G
h 
H: ∀ (i : I) (x : f i), ↑g (single i x) = ↑h (single i x)
H
#align ring_hom.functions_ext 
RingHom.functions_ext: ∀ {I : Type u_1} [inst : DecidableEq I] {f : I → Type u_3} [inst_1 : (i : I) → NonAssocSemiring (f i)]
  [inst_2 : Finite I] (G : Type u_2) [inst_3 : NonAssocSemiring G] (g h : ((i : I) → f i) →+* G),
  (∀ (i : I) (x : f i), ↑g (single i x) = ↑h (single i x)) → g = h
RingHom.functions_ext

end RingHom

namespace Prod

variable {
α: Type ?u.64455
α 
β: Type ?u.65562
β 
γ: Type ?u.64437
γ : 
Type _: Type (?u.64458+1)
Type _} [
CommMonoid: Type ?u.65568 → Type ?u.65568
CommMonoid 
α: Type ?u.64455
α] [
CommMonoid: Type ?u.64467 → Type ?u.64467
CommMonoid 
β: Type ?u.65562
β] {
s: Finset γ
s : 
Finset: Type ?u.64470 → Type ?u.64470
Finset 
γ: Type ?u.64437
γ} {
f: γ → α × β
f : 
γ: Type ?u.64461
γ → 
α: Type ?u.64431
α × 
β: Type ?u.64434
β}

@[
to_additive: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∑ c in s, f c).fst = ∑ c in s, (f c).fst
to_additive]
theorem 
fst_prod: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∏ c in s, f c).fst = ∏ c in s, (f c).fst
fst_prod : (∏ 
c: ?m.64488
c in 
s: Finset γ
s, 
f: γ → α × β
f 
c: ?m.64488
c).
1: {α : Type ?u.64542} → {β : Type ?u.64541} → α × β → α
1 = ∏ 
c: ?m.64552
c in 
s: Finset γ
s, (
f: γ → α × β
f 
c: ?m.64552
c).
1: {α : Type ?u.64555} → {β : Type ?u.64554} → α × β → α
1 :=
  (
MonoidHom.fst: (M : Type ?u.64574) → (N : Type ?u.64573) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M × N →* M
MonoidHom.fst 
α: Type ?u.64455
α 
β: Type ?u.64458
β).
map_prod: ∀ {β : Type ?u.65407} {α : Type ?u.65406} {γ : Type ?u.65405} [inst : CommMonoid β] [inst_1 : CommMonoid γ] (g : β →* γ)
  (f : α → β) (s : Finset α), ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod 
f: γ → α × β
f 
s: Finset γ
s
#align prod.fst_prod 
Prod.fst_prod: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∏ c in s, f c).fst = ∏ c in s, (f c).fst
Prod.fst_prod
#align prod.fst_sum 
Prod.fst_sum: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∑ c in s, f c).fst = ∑ c in s, (f c).fst
Prod.fst_sum

@[
to_additive: ∀ {α : Type u_2} {β : Type u_1} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∑ c in s, f c).snd = ∑ c in s, (f c).snd
to_additive]
theorem 
snd_prod: (∏ c in s, f c).snd = ∏ c in s, (f c).snd
snd_prod : (∏ 
c: ?m.65592
c in 
s: Finset γ
s, 
f: γ → α × β
f 
c: ?m.65592
c).
2: {α : Type ?u.65646} → {β : Type ?u.65645} → α × β → β
2 = ∏ 
c: ?m.65656
c in 
s: Finset γ
s, (
f: γ → α × β
f 
c: ?m.65656
c).
2: {α : Type ?u.65659} → {β : Type ?u.65658} → α × β → β
2 :=
  (
MonoidHom.snd: (M : Type ?u.65678) → (N : Type ?u.65677) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M × N →* N
MonoidHom.snd 
α: Type ?u.65559
α 
β: Type ?u.65562
β).
map_prod: ∀ {β : Type ?u.66511} {α : Type ?u.66510} {γ : Type ?u.66509} [inst : CommMonoid β] [inst_1 : CommMonoid γ] (g : β →* γ)
  (f : α → β) (s : Finset α), ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod 
f: γ → α × β
f 
s: Finset γ
s
#align prod.snd_prod 
Prod.snd_prod: ∀ {α : Type u_2} {β : Type u_1} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∏ c in s, f c).snd = ∏ c in s, (f c).snd
Prod.snd_prod
#align prod.snd_sum 
Prod.snd_sum: ∀ {α : Type u_2} {β : Type u_1} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Finset γ}
  {f : γ → α × β}, (∑ c in s, f c).snd = ∑ c in s, (f c).snd
Prod.snd_sum

end Prod