no goals
α' : Type u_1
β' : Type u_2
e✝ : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
e e' : Perm α'
⊢ (extendDomain e f).trans (extendDomain e' f) = extendDomain (e.trans e') f
simp [Perm.extendDomain, permCongr_trans]