case ofNat
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ subtypePerm f hf ^ Int.ofNat n = subtypePerm (f ^ Int.ofNat n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Int.ofNat n) x))

case negSucc
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
ih : ℕ
⊢ subtypePerm f hf ^ Int.negSucc ih =
    subtypePerm (f ^ Int.negSucc ih) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Int.negSucc ih) x))
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
n : ℤ
hf : ∀ (x : α), p x ↔ p (↑f x)
⊢ subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
induction' n with n ih
no goals
case ofNat
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ subtypePerm f hf ^ Int.ofNat n = subtypePerm (f ^ Int.ofNat n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Int.ofNat n) x))
exact subtypePerm_pow _ _ _
no goals
case negSucc
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
ih : ℕ
⊢ subtypePerm f hf ^ Int.negSucc ih =
    subtypePerm (f ^ Int.negSucc ih) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Int.negSucc ih) x))
simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]