no goals
α' : Type u_2
β' : Type u_1
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
b : β'
h : p b
⊢ ↑(extendDomain e f) b = ↑(↑f (↑e (↑f.symm { val := b, property := h })))
simp [Perm.extendDomain, h]