α : Type u_1
ι : Type ?u.333212
γ : Type ?u.333215
A : Type ?u.333218
B : Type ?u.333221
C : Type ?u.333224
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.336354
M : Type u_2
M' : Type ?u.336360
N : Type u_3
P : Type ?u.336366
G : Type ?u.336369
H : Type ?u.336372
R : Type ?u.336375
S : Type ?u.336378
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 1
h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ ∏ x in f.support ∪ g.support, h x (↑(f + g) x) = ∏ x in f.support ∪ g.support, h x (↑f x) * h x (↑g x)
α : Type u_1
ι : Type ?u.333212
γ : Type ?u.333215
A : Type ?u.333218
B : Type ?u.333221
C : Type ?u.333224
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.336354
M : Type u_2
M' : Type ?u.336360
N : Type u_3
P : Type ?u.336366
G : Type ?u.336369
H : Type ?u.336372
R : Type ?u.336375
S : Type ?u.336378
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 1
h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ prod (f + g) h = prod f h * prod g h
rw [Finsupp.prod_of_support_subset f (subset_union_left _ g.support) h h_zero,
  Finsupp.prod_of_support_subset g (subset_union_right f.support _) h h_zero, ←
  Finset.prod_mul_distrib, Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]
no goals
α : Type u_1
ι : Type ?u.333212
γ : Type ?u.333215
A : Type ?u.333218
B : Type ?u.333221
C : Type ?u.333224
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.336354
M : Type u_2
M' : Type ?u.336360
N : Type u_3
P : Type ?u.336366
G : Type ?u.336369
H : Type ?u.336372
R : Type ?u.336375
S : Type ?u.336378
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 1
h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ ∏ x in f.support ∪ g.support, h x (↑(f + g) x) = ∏ x in f.support ∪ g.support, h x (↑f x) * h x (↑g x)
exact Finset.prod_congr rfl fun x hx => by apply h_add x hx
no goals
α : Type u_1
ι : Type ?u.333212
γ : Type ?u.333215
A : Type ?u.333218
B : Type ?u.333221
C : Type ?u.333224
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x✝ : γ
β : Type ?u.336354
M : Type u_2
M' : Type ?u.336360
N : Type u_3
P : Type ?u.336366
G : Type ?u.336369
H : Type ?u.336372
R : Type ?u.336375
S : Type ?u.336378
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 1
h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
x : α
hx : x ∈ f.support ∪ g.support
⊢ h x (↑(f + g) x) = h x (↑f x) * h x (↑g x)
apply h_add x hx