no goals
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : ¬b ∈ Set.range ↑f
⊢ ↑(viaFintypeEmbedding e f) b = b
rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]