α : Type u_1
ι : Type ?u.64782
γ : Type ?u.64785
A : Type ?u.64788
B : Type ?u.64791
C : Type ?u.64794
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.67924
M : Type ?u.67927
M' : Type ?u.67930
N✝ : Type ?u.67933
P : Type ?u.67936
G : Type ?u.67939
H : Type ?u.67942
R : Type ?u.67945
S : Type ?u.67948
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = 0 → 0 = ↑f a
α : Type u_1
ι : Type ?u.64782
γ : Type ?u.64785
A : Type ?u.64788
B : Type ?u.64791
C : Type ?u.64794
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.67924
M : Type ?u.67927
M' : Type ?u.67930
N✝ : Type ?u.67933
P : Type ?u.67936
G : Type ?u.67939
H : Type ?u.67942
R : Type ?u.67945
S : Type ?u.67948
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (if a ∈ f.support then ↑f a else 0) = ↑f a
simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
no goals
α : Type u_1
ι : Type ?u.64782
γ : Type ?u.64785
A : Type ?u.64788
B : Type ?u.64791
C : Type ?u.64794
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.67924
M : Type ?u.67927
M' : Type ?u.67930
N✝ : Type ?u.67933
P : Type ?u.67936
G : Type ?u.67939
H : Type ?u.67942
R : Type ?u.67945
S : Type ?u.67948
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = 0 → 0 = ↑f a
exact fun h ↦ h.symm