no goals
ι : Type ?u.206959
α : Type u_2
β : Type u_1
f✝ g : Perm α
p✝ : α → Prop
x y z : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ ↑(extendDomain g f ^ n) ↑(↑f x) = ↑(↑f y) ↔ ↑(g ^ n) x = y
rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]