no goals
α : Type u_1
β : Type ?u.487267
γ : Type ?u.487270
ι : Type ?u.487273
M : Type u_2
M' : Type ?u.487279
N : Type ?u.487282
P : Type ?u.487285
G : Type ?u.487288
H✝ : Type ?u.487291
R : Type ?u.487294
S : Type ?u.487297
inst✝ : Zero M
p : α → Prop
f : α →₀ M
hf : ∀ (x : α), x ∈ f.support → p x
H : ∀ (x : α), p x → ↑f x = 0
x : α
⊢ ↑f x = ↑0 x
classical exact if hx : p x then H x hx else not_mem_support_iff.1 <| mt (hf x) hx
no goals
α : Type u_1
β : Type ?u.487267
γ : Type ?u.487270
ι : Type ?u.487273
M : Type u_2
M' : Type ?u.487279
N : Type ?u.487282
P : Type ?u.487285
G : Type ?u.487288
H✝ : Type ?u.487291
R : Type ?u.487294
S : Type ?u.487297
inst✝ : Zero M
p : α → Prop
f : α →₀ M
hf : ∀ (x : α), x ∈ f.support → p x
H : ∀ (x : α), p x → ↑f x = 0
x : α
⊢ ↑f x = ↑0 x
exact if hx : p x then H x hx else not_mem_support_iff.1 <| mt (hf x) hx
no goals
α : Type u_1
β : Type ?u.487267
γ : Type ?u.487270
ι : Type ?u.487273
M : Type u_2
M' : Type ?u.487279
N : Type ?u.487282
P : Type ?u.487285
G : Type ?u.487288
H✝ : Type ?u.487291
R : Type ?u.487294
S : Type ?u.487297
inst✝ : Zero M
p : α → Prop
f : α →₀ M
hf : ∀ (x : α), x ∈ f.support → p x
H : f = 0
x : α
x✝ : p x
⊢ ↑f x = 0
simp [H]