Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Simon Hudon, Patrick Massot

! This file was ported from Lean 3 source module algebra.big_operators.pi
! 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.11a, Monoid: Type ?u.14 → Type ?u.14Monoid (β: α → Type ?u.7β a: ?m.11a)] (a: αa : α: Type ?u.2α)
(l: List ((a : α) → β a)l : List: Type ?u.20 → Type ?u.20List (∀ a: ?m.22a, β: α → Type ?u.7β a: ?m.22a)) : 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 : α) → β af : ∀ a: ?m.1895a, β: α → Type ?u.7β a: ?m.1895a ↦ f: (a : α) → β af 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 ievalMonoidHom β: α → 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.3365a, CommMonoid: Type ?u.3368 → Type ?u.3368CommMonoid (β: α → Type ?u.3361β a: ?m.3365a)] (a: αa : α: Type ?u.3356α)
(s: Multiset ((a : α) → β a)s : Multiset: Type ?u.3374 → Type ?u.3374Multiset (∀ a: ?m.3376a, β: α → Type ?u.3361β a: ?m.3376a)) : 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 : α) → β af : ∀ a: ?m.3454a, β: α → Type ?u.3361β a: ?m.3454a ↦ f: (a : α) → β af 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 ievalMonoidHom β: α → 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 ato_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 aFinset.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.4579a, CommMonoid: Type ?u.4582 → Type ?u.4582CommMonoid (β: α → Type ?u.4572β a: ?m.4579a)] (a: αa : α: Type ?u.4567α)
(s: Finset γs : Finset: Type ?u.4588 → Type ?u.4588Finset γ: ?m.4575γ) (g: γ → (a : α) → β ag : γ: ?m.4575γ → ∀ a: ?m.4594a, β: α → Type ?u.4572β a: ?m.4594a) : (∏ c: ?m.4608c in s: Finset γs, g: γ → (a : α) → β ag c: ?m.4608c) a: αa = ∏ c: ?m.4676c in s: Finset γs, g: γ → (a : α) → β ag c: ?m.4676c 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 iPi.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 aFinset.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 aFinset.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 ato_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 aFinset.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.5864a, CommMonoid: Type ?u.5867 → Type ?u.5867CommMonoid (β: α → Type ?u.5857β a: ?m.5864a)] (s: Finset γs : Finset: Type ?u.5871 → Type ?u.5871Finset γ: ?m.5860γ)
(g: γ → (a : α) → β ag : γ: ?m.5860γ → ∀ a: ?m.5877a, β: α → Type ?u.5857β a: ?m.5877a) : (∏ c: ?m.5891c in s: Finset γs, g: γ → (a : α) → β ag c: ?m.5891c) = fun a: ?m.5953a ↦ ∏ c: ?m.5962c in s: Finset γs, g: γ → (a : α) → β ag c: ?m.5962c a: ?m.5953a :=
funext: ∀ {α : Sort ?u.5992} {β : α → Sort ?u.5991} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext 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 aFinset.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 aFinset.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 aFinset.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 ato_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 aFintype.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.6185Fintype γ: Type ?u.6182γ]
[∀ a: ?m.6189a, CommMonoid: Type ?u.6192 → Type ?u.6192CommMonoid (β: α → Type ?u.6179β a: ?m.6189a)] (a: αa : α: Type ?u.6174α) (g: γ → (a : α) → β ag : γ: Type ?u.6182γ → ∀ a: ?m.6201a, β: α → Type ?u.6179β a: ?m.6201a) : (∏ c: ?m.6265c, g: γ → (a : α) → β ag c: ?m.6265c) a: αa = ∏ c: ?m.6389c, g: γ → (a : α) → β ag c: ?m.6389c 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 aFinset.prod_apply a: αa Finset.univ: {α : Type ?u.6422} → [inst : Fintype α] → Finset αFinset.univ g: γ → (a : α) → β ag
#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 aFintype.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 aFintype.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.6597CommMonoid α: Type ?u.6588α] [CommMonoid: Type ?u.6600 → Type ?u.6600CommMonoid β: Type ?u.6591β] (s: Finset γs : Finset: Type ?u.6603 → Type ?u.6603Finset γ: Type ?u.6594γ) (f: γ → αf : γ: Type ?u.6594γ → α: Type ?u.6588α)
(g: γ → βg : γ: Type ?u.6594γ → β: Type ?u.6591β) : (∏ x: ?m.6651x in s: Finset γs, f: γ → αf x: ?m.6651x, ∏ x: ?m.6699x in s: Finset γs, g: γ → βg x: ?m.6699x) = ∏ x: ?m.6723x in s: Finset γs, (f: γ → αf x: ?m.6723x, g: γ → βg x: ?m.6723x) :=
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 sFinset.induction_on s: Finset γs rfl: ∀ {α : Sort ?u.6866} {a : α}, a = arfl (byGoals accomplished! 🐙 α: Type u_1β: Type u_2γ: Type u_3inst✝¹: 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: Booltrue }) [Prod.ext_iff: ∀ {α : Type ?u.7045} {β : Type ?u.7046} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.sndProd.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.13588I : Type _: Type (?u.13613+1)Type _} [DecidableEq: Sort ?u.13616 → Sort (max1?u.13616)DecidableEq I: Type ?u.13613I] {Z: I → Type ?u.13602Z : I: Type ?u.13613I → Type _: Type (?u.17784+1)Type _}

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

@[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) = fto_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) = fFinset.univ_prod_mulSingle [Fintype: Type ?u.13638 → Type ?u.13638Fintype I: Type ?u.13613I] (f: (i : I) → Z if : ∀ i: ?m.13642i, Z: I → Type ?u.13627Z i: ?m.13642i) :
(∏ i: ?m.13706i, 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 jPi.mulSingle i: ?m.13706i (f: (i : I) → Z if i: ?m.13706i)) = f: (i : I) → Z if := byGoals accomplished! 🐙
I: Type u_1inst✝²: DecidableEq IZ: I → Type u_2inst✝¹: (i : I) → CommMonoid (Z i)inst✝: Fintype If: (i : I) → Z i∏ i : I, Pi.mulSingle i (f i) = fext a: ?αaI: Type u_1inst✝²: DecidableEq IZ: I → Type u_2inst✝¹: (i : I) → CommMonoid (Z i)inst✝: Fintype If: (i : I) → Z ia: IhFinset.prod univ (fun i => Pi.mulSingle i (f i)) a = f a
I: Type u_1inst✝²: DecidableEq IZ: I → Type u_2inst✝¹: (i : I) → CommMonoid (Z i)inst✝: Fintype If: (i : I) → Z i∏ i : I, Pi.mulSingle i (f i) = fsimpGoals 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) = fFinset.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) = fFinset.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 = hto_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 = hMonoidHom.functions_ext [Finite: Sort ?u.17795 → PropFinite I: Type ?u.17770I] (G: Type ?u.17798G : Type _: Type (?u.17798+1)Type _) [CommMonoid: Type ?u.17801 → Type ?u.17801CommMonoid G: Type ?u.17798G] (g: ((i : I) → Z i) →* Gg h: ((i : I) → Z i) →* Gh : (∀ i: ?m.19246i, Z: I → Type ?u.17784Z i: ?m.19246i) →* G: Type ?u.17798G)
(H: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)H : ∀ i: ?m.19255i x: ?m.19258x, g: ((i : I) → Z i) →* Gg (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 jPi.mulSingle i: ?m.19255i x: ?m.19258x) = h: ((i : I) → Z i) →* Gh (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 jPi.mulSingle i: ?m.19255i x: ?m.19258x)) : g: ((i : I) → Z i) →* Gg = h: ((i : I) → Z i) →* Gh := byGoals accomplished! 🐙
I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (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_1II: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Iintrog = h
I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)g = hext k: ?MkI: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h↑g k = ↑h k
I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)g = hrw [I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.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) = fFinset.univ_prod_mulSingle k: ?Mk,I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h↑g (∏ i : I, Pi.mulSingle i (k i)) = ↑h (∏ i : I, Pi.mulSingle i (k i)) I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h↑g k = ↑h kg: ((i : I) → Z i) →* Gg.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_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h∏ x : I, ↑g (Pi.mulSingle x (k x)) = ↑h (∏ i : I, Pi.mulSingle i (k i)) I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h↑g k = ↑h kh: ((i : I) → Z i) →* Gh.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_prodI: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h∏ x : I, ↑g (Pi.mulSingle x (k x)) = ∏ x : I, ↑h (Pi.mulSingle x (k x))]I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)val✝: Fintype Ik: (i : I) → Z iintro.h∏ x : I, ↑g (Pi.mulSingle x (k x)) = ∏ x : I, ↑h (Pi.mulSingle x (k x))
I: Type u_1inst✝³: DecidableEq IZ: I → Type u_3inst✝²: (i : I) → CommMonoid (Z i)inst✝¹: Finite IG: Type u_2inst✝: CommMonoid Gg, h: ((i : I) → Z i) →* GH: ∀ (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 = hMonoidHom.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 = hAddMonoidHom.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),
"\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 = hMonoidHom.functions_ext' [Finite: Sort ?u.37310 → PropFinite I: Type ?u.37285I] (M: Type u_2M : Type _: Type (?u.37313+1)Type _) [CommMonoid: Type ?u.37316 → Type ?u.37316CommMonoid M: Type ?u.37313M] (g: ((i : I) → Z i) →* Mg h: ((i : I) → Z i) →* Mh : (∀ i: ?m.37322i, Z: I → Type ?u.37299Z i: ?m.38761i) →* M: Type ?u.37313M)
(H: ∀ (i : I), comp g (single Z i) = comp h (single Z i)H : ∀ i: ?m.38770i, g: ((i : I) → Z i) →* Mg.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 →* Pcomp (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 iMonoidHom.single Z: I → Type ?u.37299Z i: ?m.38770i) = h: ((i : I) → Z i) →* Mh.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 →* Pcomp (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 iMonoidHom.single Z: I → Type ?u.37299Z i: ?m.38770i)) : g: ((i : I) → Z i) →* Mg = h: ((i : I) → Z i) →* Mh :=
g: ((i : I) → Z i) →* Mg.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 = hfunctions_ext M: Type u_2M h: ((i : I) → Z i) →* Mh fun i: ?m.40249i => 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 xFunLike.congr_fun (H: ∀ (i : I), comp g (single Z i) = comp h (single Z i)H i: ?m.40249i)
#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 = hMonoidHom.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),

end MulSingle

section RingHom

open Pi

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

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

@[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 = hRingHom.functions_ext [Finite: Sort ?u.47803 → PropFinite I: Type ?u.47778I] (G: Type ?u.47806G : Type _: Type (?u.47806+1)Type _) [NonAssocSemiring: Type ?u.47809 → Type ?u.47809NonAssocSemiring G: Type ?u.47806G] (g: ((i : I) → f i) →+* Gg h: ((i : I) → f i) →+* Gh : (∀ i: ?m.47871i, f: I → Type ?u.47792f i: ?m.47871i) →+* G: Type ?u.47806G)
(H: ∀ (i : I) (x : f i), ↑g (single i x) = ↑h (single i x)H : ∀ (i: Ii : I: Type ?u.47778I) (x: f ix : f: I → Type ?u.47792f i: Ii), g: ((i : I) → f i) →+* Gg (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 jsingle i: Ii x: f ix) = h: ((i : I) → f i) →+* Gh (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 jsingle i: Ii x: f ix)) : g: ((i : I) → f i) →+* Gg = h: ((i : I) → f i) →+* Gh :=
RingHom.coe_addMonoidHom_injective: ∀ {α : Type ?u.62799} {β : Type ?u.62800} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β},
Function.Injective fun f => ↑fRingHom.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 = hAddMonoidHom.functions_ext I: Type ?u.47778I _ f: I → Type ?u.47792f _ _ G: Type u_2G _ (g: ((i : I) → f i) →+* Gg : (∀ i: ?m.62831i, f: I → Type ?u.47792f i: ?m.62831i) →+ G: Type u_2G) h: ((i : I) → f i) →+* Gh 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 = hRingHom.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.65568CommMonoid α: Type ?u.64455α] [CommMonoid: Type ?u.64467 → Type ?u.64467CommMonoid β: Type ?u.65562β] {s: Finset γs : Finset: Type ?u.64470 → Type ?u.64470Finset γ: 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).fstto_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).fstfst_prod : (∏ c: ?m.64488c in s: Finset γs, f: γ → α × βf c: ?m.64488c).1: {α : Type ?u.64542} → {β : Type ?u.64541} → α × β → α1 = ∏ c: ?m.64552c in s: Finset γs, (f: γ → α × βf c: ?m.64552c).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 →* MMonoidHom.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).fstProd.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).fstProd.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).sndto_additive]
theorem snd_prod: (∏ c in s, f c).snd = ∏ c in s, (f c).sndsnd_prod : (∏ c: ?m.65592c in s: Finset γs, f: γ → α × βf c: ?m.65592c).2: {α : Type ?u.65646} → {β : Type ?u.65645} → α × β → β2 = ∏ c: ?m.65656c in s: Finset γs, (f: γ → α × βf c: ?m.65656c).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 →* NMonoidHom.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).sndProd.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).sndProd.snd_sum

end Prod
```