α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ ↑(extendDomain e (Function.Embedding.toEquivRange f)) (↑f a) = ↑f (↑e a)
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ ↑(viaFintypeEmbedding e f) (↑f a) = ↑f (↑e a)
rw [Equiv.Perm.viaFintypeEmbedding]
no goals
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ ↑(extendDomain e (Function.Embedding.toEquivRange f)) (↑f a) = ↑f (↑e a)
convert Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a