no goals
α : Type u_1
β : Type ?u.485392
γ : Type ?u.485395
ι : Type ?u.485398
M : Type u_2
M' : Type ?u.485404
N : Type ?u.485407
P : Type ?u.485410
G : Type ?u.485413
H : Type ?u.485416
R : Type ?u.485419
S : Type ?u.485422
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support
rw [Subsingleton.elim D] <;> rfl