no goals
α : Type u_1
β : Type ?u.486127
γ : Type ?u.486130
ι : Type ?u.486133
M : Type u_2
M' : Type ?u.486139
N : Type ?u.486142
P : Type ?u.486145
G : Type ?u.486148
H : Type ?u.486151
R : Type ?u.486154
S : Type ?u.486157
inst✝ : Zero M
p : α → Prop
f : α →₀ M
⊢ subtypeDomain p f = 0 ↔ ∀ (x : α), p x → ↑f x = 0
classical simp_rw [← support_eq_empty, support_subtypeDomain, subtype_eq_empty,
    not_mem_support_iff]
no goals
α : Type u_1
β : Type ?u.486127
γ : Type ?u.486130
ι : Type ?u.486133
M : Type u_2
M' : Type ?u.486139
N : Type ?u.486142
P : Type ?u.486145
G : Type ?u.486148
H : Type ?u.486151
R : Type ?u.486154
S : Type ?u.486157
inst✝ : Zero M
p : α → Prop
f : α →₀ M
⊢ subtypeDomain p f = 0 ↔ ∀ (x : α), p x → ↑f x = 0
simp_rw [← support_eq_empty, support_subtypeDomain, subtype_eq_empty,
not_mem_support_iff]