no goals
ι : Type ?u.206150
α : Type u_1
β : Type ?u.206156
f g : Perm α
p : α → Prop
x✝ y✝ z : α
h : ∀ (x : α), p x ↔ p (↑f x)
x y : { x // p x }
n : ℤ
⊢ ↑(subtypePerm f h ^ n) x = y ↔ ↑(f ^ n) ↑x = ↑y
simp [Subtype.ext_iff]