[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ (i : α), i ∈ s → g i 0 = 1
⊢ prod f g = ∏ x in s, g x (↑f x)
[PROOFSTEP]
refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ (i : α), i ∈ s → g i 0 = 1
x : α
hxs : x ∈ s
hx : ¬x ∈ f.support
⊢ ↑f x = 0
[PROOFSTEP]
exact not_mem_support_iff.1 hx
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
a : α
b : M
h : α → M → N
h_zero : h a 0 = 1
⊢ ∏ x in {a}, h x (↑(single a b) x) = h a b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H✝ : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : ¬x✝¹ ∈ (mapRange f hf g).support
⊢ h x✝¹ (↑(mapRange f hf g) x✝¹) = 1
[PROOFSTEP]
rw [not_mem_support_iff.1 H, h0]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (prod f fun x v => if a = x then b x v else 1) = if a ∈ f.support then b a (↑f a) else 1
[PROOFSTEP]
dsimp [Finsupp.prod]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 in f.support, if a = a_1 then b a_1 (↑f a_1) else 1) = if a ∈ f.support then b a (↑f a) else 1
[PROOFSTEP]
rw [f.support.prod_ite_eq]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (sum f fun x v => if a = x then v else 0) = ↑f a
[PROOFSTEP]
classical
convert f.sum_ite_eq a fun _ => id
simp [ite_eq_right_iff.2 Eq.symm]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (sum f fun x v => if a = x then v else 0) = ↑f a
[PROOFSTEP]
convert f.sum_ite_eq a fun _ => id
[GOAL]
case h.e'_3
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = if a ∈ f.support then id (↑f a) else 0
[PROOFSTEP]
simp [ite_eq_right_iff.2 Eq.symm]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (if a ∈ f.support then ↑f a else 0) = ↑f a
[PROOFSTEP]
simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = 0 → 0 = ↑f a
[PROOFSTEP]
exact fun h ↦ h.symm
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (prod f fun x v => if x = a then b x v else 1) = if a ∈ f.support then b a (↑f a) else 1
[PROOFSTEP]
dsimp [Finsupp.prod]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 in f.support, if a_1 = a then b a_1 (↑f a_1) else 1) = if a ∈ f.support then b a (↑f a) else 1
[PROOFSTEP]
rw [f.support.prod_ite_eq']
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (sum f fun x v => if x = a then v else 0) = ↑f a
[PROOFSTEP]
classical
convert f.sum_ite_eq' a fun _ => id
simp [ite_eq_right_iff.2 Eq.symm]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (sum f fun x v => if x = a then v else 0) = ↑f a
[PROOFSTEP]
convert f.sum_ite_eq' a fun _ => id
[GOAL]
case h.e'_3
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N✝ : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = if a ∈ f.support then id (↑f a) else 0
[PROOFSTEP]
simp [ite_eq_right_iff.2 Eq.symm]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ (x : α), x ∈ s → ¬x ∈ (onFinset s f hf).support → g x (↑(onFinset s f hf) x) = 1
[PROOFSTEP]
simp (config := { contextual := true }) [*]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
[PROOFSTEP]
classical
rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase, Finset.prod_congr rfl]
intro h hx
rw [Finsupp.erase_ne (ne_of_mem_erase hx)]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
[PROOFSTEP]
rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase, Finset.prod_congr rfl]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ (x : α), x ∈ Finset.erase f.support y → g x (↑(erase y f) x) = g x (↑f x)
[PROOFSTEP]
intro h hx
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
hx : h ∈ Finset.erase f.support y
⊢ g h (↑(erase y f) h) = g h (↑f h)
[PROOFSTEP]
rw [Finsupp.erase_ne (ne_of_mem_erase hx)]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
⊢ g y (↑f y) * prod (erase y f) g = prod f g
[PROOFSTEP]
classical
by_cases hyf : y ∈ f.support
· exact Finsupp.mul_prod_erase f y g hyf
· rw [not_mem_support_iff.mp hyf, hg y, erase_of_not_mem_support hyf, one_mul]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
⊢ g y (↑f y) * prod (erase y f) g = prod f g
[PROOFSTEP]
by_cases hyf : y ∈ f.support
[GOAL]
case pos
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
[PROOFSTEP]
exact Finsupp.mul_prod_erase f y g hyf
[GOAL]
case neg
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : ¬y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
[PROOFSTEP]
rw [not_mem_support_iff.mp hyf, hg y, erase_of_not_mem_support hyf, one_mul]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ (Multiset.sum s) = Multiset.sum (Multiset.map (single a✝) s)
⊢ single a✝ (Multiset.sum (a ::ₘ s)) = Multiset.sum (Multiset.map (single a✝) (a ::ₘ s))
[PROOFSTEP]
rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b in s, f b) = ∑ b in s, single a (f b)
[PROOFSTEP]
trans
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b in s, f b) = ?m.275536
[PROOFSTEP]
apply single_multiset_sum
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ Multiset.sum (Multiset.map (single a) (Multiset.map (fun b => f b) s.val)) = ∑ b in s, single a (f b)
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ Multiset.sum (Multiset.map (single a ∘ fun b => f b) s.val) = ∑ b in s, single a (f b)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ (sum f g).support ⊆ Finset.biUnion f.support fun a => (g a (↑f a)).support
[PROOFSTEP]
have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
  let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
  ⟨a, mem_support_iff.mp ha, ne⟩
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
this : ∀ (c : β), (sum f fun a b => ↑(g a b) c) ≠ 0 → ∃ a, ↑f a ≠ 0 ∧ ¬↑(g a (↑f a)) c = 0
⊢ (sum f g).support ⊆ Finset.biUnion f.support fun a => (g a (↑f a)).support
[PROOFSTEP]
simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (Finset.sum s f).support ⊆ Finset.biUnion s fun x => (f x).support
[PROOFSTEP]
rw [← Finset.sup_eq_biUnion]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (Finset.sum s f).support ⊆ sup s fun x => (f x).support
[PROOFSTEP]
induction' s using Finset.cons_induction_on with a s ha ih
[GOAL]
case h₁
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
⊢ (Finset.sum ∅ f).support ⊆ sup ∅ fun x => (f x).support
[PROOFSTEP]
rfl
[GOAL]
case h₂
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a : α
s : Finset α
ha : ¬a ∈ s
ih : (Finset.sum s f).support ⊆ sup s fun x => (f x).support
⊢ (Finset.sum (cons a s ha) f).support ⊆ sup (cons a s ha) fun x => (f x).support
[PROOFSTEP]
rw [Finset.sum_cons, Finset.sup_cons]
[GOAL]
case h₂
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a : α
s : Finset α
ha : ¬a ∈ s
ih : (Finset.sum s f).support ⊆ sup s fun x => (f x).support
⊢ (f a + ∑ x in s, f x).support ⊆ (f a).support ⊔ sup s fun x => (f x).support
[PROOFSTEP]
exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
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)
[PROOFSTEP]
exact Finset.prod_congr rfl fun x hx => by apply h_add x hx
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
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)
[PROOFSTEP]
apply h_add x hx
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ prod (f + g) h = prod f h * prod g h
[PROOFSTEP]
classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ prod (f + g) h = prod f h * prod g h
[PROOFSTEP]
exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
⊢ (fun F x => AddMonoidHom.comp F (singleAddHom x))
      ((fun F =>
          {
            toZeroHom :=
              { toFun := fun f => sum f fun x => ↑(F x), map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
            map_add' :=
              (_ :
                ∀ (x x_1 : α →₀ M),
                  (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
        F) =
    F
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ↑((fun F x => AddMonoidHom.comp F (singleAddHom x))
          ((fun F =>
              {
                toZeroHom :=
                  { toFun := fun f => sum f fun x => ↑(F x),
                    map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                map_add' :=
                  (_ :
                    ∀ (x x_1 : α →₀ M),
                      (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
            F)
          x✝¹)
      x✝ =
    ↑(F x✝¹) x✝
[PROOFSTEP]
simp [singleAddHom]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
⊢ (fun F =>
        {
          toZeroHom :=
            { toFun := fun f => sum f fun x => ↑(F x), map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
          map_add' :=
            (_ :
              ∀ (x x_1 : α →₀ M),
                (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
      ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
    F
[PROOFSTEP]
apply Finsupp.addHom_ext'
[GOAL]
case H
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
⊢ ∀ (x : α),
    AddMonoidHom.comp
        ((fun F =>
            {
              toZeroHom :=
                { toFun := fun f => sum f fun x => ↑(F x),
                  map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
              map_add' :=
                (_ :
                  ∀ (x x_1 : α →₀ M),
                    (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
          ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F))
        (singleAddHom x) =
      AddMonoidHom.comp F (singleAddHom x)
[PROOFSTEP]
simp [singleAddHom, AddMonoidHom.comp, Function.comp]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G✝ : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
⊢ Equiv.toFun
      {
        toFun := fun F =>
          {
            toZeroHom :=
              { toFun := fun f => sum f fun x => ↑(F x), map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
            map_add' :=
              (_ :
                ∀ (x x_1 : α →₀ M),
                  (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) },
        invFun := fun F x => AddMonoidHom.comp F (singleAddHom x),
        left_inv :=
          (_ :
            ∀ (F : α → M →+ N),
              (fun F x => AddMonoidHom.comp F (singleAddHom x))
                  ((fun F =>
                      {
                        toZeroHom :=
                          { toFun := fun f => sum f fun x => ↑(F x),
                            map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                        map_add' :=
                          (_ :
                            ∀ (x x_1 : α →₀ M),
                              (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                    F) =
                F),
        right_inv :=
          (_ :
            ∀ (F : (α →₀ M) →+ N),
              (fun F =>
                    {
                      toZeroHom :=
                        { toFun := fun f => sum f fun x => ↑(F x),
                          map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                      map_add' :=
                        (_ :
                          ∀ (x x_1 : α →₀ M),
                            (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                  ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
                F) }
      (F + G) =
    Equiv.toFun
        {
          toFun := fun F =>
            {
              toZeroHom :=
                { toFun := fun f => sum f fun x => ↑(F x),
                  map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
              map_add' :=
                (_ :
                  ∀ (x x_1 : α →₀ M),
                    (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) },
          invFun := fun F x => AddMonoidHom.comp F (singleAddHom x),
          left_inv :=
            (_ :
              ∀ (F : α → M →+ N),
                (fun F x => AddMonoidHom.comp F (singleAddHom x))
                    ((fun F =>
                        {
                          toZeroHom :=
                            { toFun := fun f => sum f fun x => ↑(F x),
                              map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                          map_add' :=
                            (_ :
                              ∀ (x x_1 : α →₀ M),
                                (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                      F) =
                  F),
          right_inv :=
            (_ :
              ∀ (F : (α →₀ M) →+ N),
                (fun F =>
                      {
                        toZeroHom :=
                          { toFun := fun f => sum f fun x => ↑(F x),
                            map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                        map_add' :=
                          (_ :
                            ∀ (x x_1 : α →₀ M),
                              (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                    ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
                  F) }
        F +
      Equiv.toFun
        {
          toFun := fun F =>
            {
              toZeroHom :=
                { toFun := fun f => sum f fun x => ↑(F x),
                  map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
              map_add' :=
                (_ :
                  ∀ (x x_1 : α →₀ M),
                    (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) },
          invFun := fun F x => AddMonoidHom.comp F (singleAddHom x),
          left_inv :=
            (_ :
              ∀ (F : α → M →+ N),
                (fun F x => AddMonoidHom.comp F (singleAddHom x))
                    ((fun F =>
                        {
                          toZeroHom :=
                            { toFun := fun f => sum f fun x => ↑(F x),
                              map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                          map_add' :=
                            (_ :
                              ∀ (x x_1 : α →₀ M),
                                (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                      F) =
                  F),
          right_inv :=
            (_ :
              ∀ (F : (α →₀ M) →+ N),
                (fun F =>
                      {
                        toZeroHom :=
                          { toFun := fun f => sum f fun x => ↑(F x),
                            map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                        map_add' :=
                          (_ :
                            ∀ (x x_1 : α →₀ M),
                              (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                    ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
                  F) }
        G
[PROOFSTEP]
ext x
[GOAL]
case H.h
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G✝ : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
x : α
x✝ : M
⊢ ↑(AddMonoidHom.comp
          (Equiv.toFun
            {
              toFun := fun F =>
                {
                  toZeroHom :=
                    { toFun := fun f => sum f fun x => ↑(F x),
                      map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                  map_add' :=
                    (_ :
                      ∀ (x x_1 : α →₀ M),
                        (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) },
              invFun := fun F x => AddMonoidHom.comp F (singleAddHom x),
              left_inv :=
                (_ :
                  ∀ (F : α → M →+ N),
                    (fun F x => AddMonoidHom.comp F (singleAddHom x))
                        ((fun F =>
                            {
                              toZeroHom :=
                                { toFun := fun f => sum f fun x => ↑(F x),
                                  map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                              map_add' :=
                                (_ :
                                  ∀ (x x_1 : α →₀ M),
                                    (sum (x + x_1) fun a => ↑(F a)) =
                                      (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                          F) =
                      F),
              right_inv :=
                (_ :
                  ∀ (F : (α →₀ M) →+ N),
                    (fun F =>
                          {
                            toZeroHom :=
                              { toFun := fun f => sum f fun x => ↑(F x),
                                map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                            map_add' :=
                              (_ :
                                ∀ (x x_1 : α →₀ M),
                                  (sum (x + x_1) fun a => ↑(F a)) =
                                    (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                        ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
                      F) }
            (F + G))
          (singleAddHom x))
      x✝ =
    ↑(AddMonoidHom.comp
          (Equiv.toFun
              {
                toFun := fun F =>
                  {
                    toZeroHom :=
                      { toFun := fun f => sum f fun x => ↑(F x),
                        map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : α →₀ M),
                          (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) },
                invFun := fun F x => AddMonoidHom.comp F (singleAddHom x),
                left_inv :=
                  (_ :
                    ∀ (F : α → M →+ N),
                      (fun F x => AddMonoidHom.comp F (singleAddHom x))
                          ((fun F =>
                              {
                                toZeroHom :=
                                  { toFun := fun f => sum f fun x => ↑(F x),
                                    map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                                map_add' :=
                                  (_ :
                                    ∀ (x x_1 : α →₀ M),
                                      (sum (x + x_1) fun a => ↑(F a)) =
                                        (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                            F) =
                        F),
                right_inv :=
                  (_ :
                    ∀ (F : (α →₀ M) →+ N),
                      (fun F =>
                            {
                              toZeroHom :=
                                { toFun := fun f => sum f fun x => ↑(F x),
                                  map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                              map_add' :=
                                (_ :
                                  ∀ (x x_1 : α →₀ M),
                                    (sum (x + x_1) fun a => ↑(F a)) =
                                      (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                          ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
                        F) }
              F +
            Equiv.toFun
              {
                toFun := fun F =>
                  {
                    toZeroHom :=
                      { toFun := fun f => sum f fun x => ↑(F x),
                        map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : α →₀ M),
                          (sum (x + x_1) fun a => ↑(F a)) = (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) },
                invFun := fun F x => AddMonoidHom.comp F (singleAddHom x),
                left_inv :=
                  (_ :
                    ∀ (F : α → M →+ N),
                      (fun F x => AddMonoidHom.comp F (singleAddHom x))
                          ((fun F =>
                              {
                                toZeroHom :=
                                  { toFun := fun f => sum f fun x => ↑(F x),
                                    map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                                map_add' :=
                                  (_ :
                                    ∀ (x x_1 : α →₀ M),
                                      (sum (x + x_1) fun a => ↑(F a)) =
                                        (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                            F) =
                        F),
                right_inv :=
                  (_ :
                    ∀ (F : (α →₀ M) →+ N),
                      (fun F =>
                            {
                              toZeroHom :=
                                { toFun := fun f => sum f fun x => ↑(F x),
                                  map_zero' := (_ : ∑ x in ∅, (fun x => ↑(F x)) x (↑0 x) = 0) },
                              map_add' :=
                                (_ :
                                  ∀ (x x_1 : α →₀ M),
                                    (sum (x + x_1) fun a => ↑(F a)) =
                                      (sum x fun a => ↑(F a)) + sum x_1 fun a => ↑(F a)) })
                          ((fun F x => AddMonoidHom.comp F (singleAddHom x)) F) =
                        F) }
              G)
          (singleAddHom x))
      x✝
[PROOFSTEP]
exact sum_add
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, ↑(single i m) j = m
[PROOFSTEP]
classical rw [single, coe_mk, Finset.sum_pi_single']
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, ↑(single i m) j = m
[PROOFSTEP]
rw [single, coe_mk, Finset.sum_pi_single']
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, ↑(single j m) i = m
[PROOFSTEP]
simp_rw [single, coe_mk]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m
[PROOFSTEP]
classical rw [Finset.sum_pi_single]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m
[PROOFSTEP]
rw [Finset.sum_pi_single]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ ↑(AddEquiv.symm liftAddHom) (AddMonoidHom.comp g (↑liftAddHom f)) a = AddMonoidHom.comp g (f a)
[PROOFSTEP]
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ prod (embDomain f v) g = prod v fun a b => g (↑f a) b
[PROOFSTEP]
rw [prod, prod, support_embDomain, Finset.prod_map]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x in v.support, g (↑f x) (↑(embDomain f v) (↑f x)) = ∏ a in v.support, g (↑f a) (↑v a)
[PROOFSTEP]
simp_rw [embDomain_apply]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : ¬a ∈ s
ih : ∏ i in s, prod (g i) h = prod (∑ i in s, g i) h
⊢ ∏ i in cons a s has, prod (g i) h = prod (∑ i in cons a s has, g i) h
[PROOFSTEP]
rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : sum (Multiset.sum s) h = Multiset.sum (Multiset.map (fun g => sum g h) s)
⊢ sum (Multiset.sum (a ::ₘ s)) h = Multiset.sum (Multiset.map (fun g => sum g h) (a ::ₘ s))
[PROOFSTEP]
rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]
[GOAL]
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support
[PROOFSTEP]
classical
  -- Porting note: apply Finset.induction_on s was not working; refine does.
refine Finset.induction_on s ?_ ?_
· simp
· intro i s hi
  simp only [hi, sum_insert, not_false_iff, biUnion_insert]
  intro hs
  rw [Finsupp.support_add_eq, hs]
  rw [hs, Finset.disjoint_biUnion_right]
  intro j hj
  refine' h _ _ (ne_of_mem_of_not_mem hj hi).symm
[GOAL]
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support
[PROOFSTEP]
refine Finset.induction_on s ?_ ?_
[GOAL]
case refine_1
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i in ∅, g i).support = Finset.biUnion ∅ fun i => (g i).support
[PROOFSTEP]
simp
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support) →
        (∑ i in insert a s, g i).support = Finset.biUnion (insert a s) fun i => (g i).support
[PROOFSTEP]
intro i s hi
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : ¬i ∈ s
⊢ ((∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support) →
    (∑ i in insert i s, g i).support = Finset.biUnion (insert i s) fun i => (g i).support
[PROOFSTEP]
simp only [hi, sum_insert, not_false_iff, biUnion_insert]
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : ¬i ∈ s
⊢ ((∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support) →
    (g i + ∑ i in s, g i).support = (g i).support ∪ Finset.biUnion s fun i => (g i).support
[PROOFSTEP]
intro hs
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : ¬i ∈ s
hs : (∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support
⊢ (g i + ∑ i in s, g i).support = (g i).support ∪ Finset.biUnion s fun i => (g i).support
[PROOFSTEP]
rw [Finsupp.support_add_eq, hs]
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : ¬i ∈ s
hs : (∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support
⊢ Disjoint (g i).support (∑ i in s, g i).support
[PROOFSTEP]
rw [hs, Finset.disjoint_biUnion_right]
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : ¬i ∈ s
hs : (∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support
⊢ ∀ (i_1 : ι), i_1 ∈ s → Disjoint (g i).support (g i_1).support
[PROOFSTEP]
intro j hj
[GOAL]
case refine_2
α✝ : Type u_1
ι✝ : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M✝ : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : ¬i ∈ s
hs : (∑ i in s, g i).support = Finset.biUnion s fun i => (g i).support
j : ι
hj : j ∈ s
⊢ Disjoint (g i).support (g j).support
[PROOFSTEP]
refine' h _ _ (ne_of_mem_of_not_mem hj hi).symm
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
⊢ prod (f1 + f2) g = prod f1 g * prod f2 g
[PROOFSTEP]
have : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → (∏ x in f1.support, g x (f1 x + f2 x)) = f1.prod g :=
  fun hd => Finset.prod_congr rfl fun x hx => by simp only [not_mem_support_iff.mp (disjoint_left.mp hd hx), add_zero]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd✝ : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
f1✝ f2✝ : α →₀ M
hd : Disjoint f1✝.support f2✝.support
x : α
hx : x ∈ f1✝.support
⊢ g x (↑f1✝ x + ↑f2✝ x) = g x (↑f1✝ x)
[PROOFSTEP]
simp only [not_mem_support_iff.mp (disjoint_left.mp hd hx), add_zero]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x in f1.support, g x (↑f1 x + ↑f2 x) = prod f1 g
⊢ prod (f1 + f2) g = prod f1 g * prod f2 g
[PROOFSTEP]
classical simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd, prod_union hd,
  add_apply]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x in f1.support, g x (↑f1 x + ↑f2 x) = prod f1 g
⊢ prod (f1 + f2) g = prod f1 g * prod f2 g
[PROOFSTEP]
simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd, prod_union hd, add_apply]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
⊢ prod f1 g1 ∣ prod f2 g2
[PROOFSTEP]
classical
simp only [Finsupp.prod, Finsupp.prod_mul]
rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
apply dvd_mul_of_dvd_right
apply prod_dvd_prod_of_dvd
exact h2
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
⊢ prod f1 g1 ∣ prod f2 g2
[PROOFSTEP]
simp only [Finsupp.prod, Finsupp.prod_mul]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
⊢ ∏ x in f1.support, g1 x (↑f1 x) ∣ ∏ x in f2.support, g2 x (↑f2 x)
[PROOFSTEP]
rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
⊢ ∏ x in f1.support, g1 x (↑f1 x) ∣ (∏ x in f2.support \ f1.support, g2 x (↑f2 x)) * ∏ x in f1.support, g2 x (↑f2 x)
[PROOFSTEP]
apply dvd_mul_of_dvd_right
[GOAL]
case h
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
⊢ ∏ x in f1.support, g1 x (↑f1 x) ∣ ∏ x in f1.support, g2 x (↑f2 x)
[PROOFSTEP]
apply prod_dvd_prod_of_dvd
[GOAL]
case h.h
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
⊢ ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)
[PROOFSTEP]
exact h2
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ indicator s f = ∑ x in attach s, single (↑x) (f ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∑ x in attach s, single (↑x) (↑(indicator s f) ↑x) = ∑ x in attach s, single (↑x) (f ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
refine' Finset.sum_congr rfl (fun _ _ => _)
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ attach s
⊢ single (↑x✝¹) (↑(indicator s f) ↑x✝¹) = single (↑x✝¹) (f ↑x✝¹ (_ : ↑x✝¹ ∈ s))
[PROOFSTEP]
rw [indicator_of_mem]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ (x : α), x ∈ s → ¬x ∈ (indicator s f).support → single x (↑(indicator s f) x) = 0
[PROOFSTEP]
intro i _ hi
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : ¬i ∈ (indicator s f).support
⊢ single i (↑(indicator s f) i) = 0
[PROOFSTEP]
rw [not_mem_support_iff.mp hi, single_zero]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ (a : α), a ∈ s → h a 0 = 1
⊢ prod (indicator s f) h = ∏ x in attach s, h (↑x) (f ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ (a : α), a ∈ s → h a 0 = 1
⊢ ∏ x in attach s, h (↑x) (↑(indicator s f) ↑x) = ∏ x in attach s, h (↑x) (f ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
refine' Finset.prod_congr rfl (fun _ _ => _)
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ (a : α), a ∈ s → h a 0 = 1
x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ attach s
⊢ h (↑x✝¹) (↑(indicator s f) ↑x✝¹) = h (↑x✝¹) (f ↑x✝¹ (_ : ↑x✝¹ ∈ s))
[PROOFSTEP]
rw [indicator_of_mem]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
a : α
s : Finset α
has : ¬a ∈ s
ih : sum (∑ x in s, f x) t = ∑ x in s, sum (f x) t
⊢ sum (∑ x in insert a s, f x) t = ∑ x in insert a s, sum (f x) t
[PROOFSTEP]
simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ sum s f * b = sum s fun a c => f a c * b
[PROOFSTEP]
simp only [Finsupp.sum, Finset.sum_mul]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ b * sum s f = sum s fun a c => b * f a c
[PROOFSTEP]
simp only [Finsupp.sum, Finset.mul_sum]
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H✝ : Type u_13
R : Type u_14
S : Type u_15
f : ℕ →₀ ℕ
hf : ¬0 ∈ f.support
a : ℕ
ha : a ∈ f.support
H : a = 0
⊢ False
[PROOFSTEP]
subst H
[GOAL]
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
f : ℕ →₀ ℕ
hf : ¬0 ∈ f.support
ha : 0 ∈ f.support
⊢ False
[PROOFSTEP]
exact hf ha