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

case succ
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
ih : subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
⊢ subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) 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 zero
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
⊢ subtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x))
simp
no goals
case succ
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
ih : subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
⊢ subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))
simp_rw [pow_succ', ih, subtypePerm_mul]