no goals
α : Type u_1
β : Type u_2
γ : Type ?u.227043
ι : Type ?u.227046
M : Type u_3
M' : Type ?u.227052
N : Type ?u.227055
P : Type ?u.227058
G : Type ?u.227061
H : Type ?u.227064
R : Type ?u.227067
S : Type ?u.227070
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ ↑l₁ a = ↑l₂ a
simpa only [embDomain_apply] using FunLike.ext_iff.1 h (f a)