ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
n : ℕ
⊢ ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ ∀ (n : ℕ), ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
intro n
case zero
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ ↑(cycleOf f x ^ Nat.zero) x = ↑(f ^ Nat.zero) x

case succ
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
n : ℕ
hn : ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
⊢ ↑(cycleOf f x ^ Nat.succ n) x = ↑(f ^ Nat.succ n) x
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
n : ℕ
⊢ ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
induction' n with n hn
no goals
case zero
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ ↑(cycleOf f x ^ Nat.zero) x = ↑(f ^ Nat.zero) x
rfl
case succ.hc
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
n : ℕ
hn : ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
⊢ SameCycle f x (↑(f ^ n) x)
case succ
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
n : ℕ
hn : ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
⊢ ↑(cycleOf f x ^ Nat.succ n) x = ↑(f ^ Nat.succ n) x
rw [pow_succ, mul_apply, cycleOf_apply, hn, if_pos, pow_succ, mul_apply]
no goals
case succ.hc
ι : Type ?u.2116608
α : Type u_1
β : Type ?u.2116614
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
n : ℕ
hn : ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
⊢ SameCycle f x (↑(f ^ n) x)
simpa [SameCycle] using ⟨n,rfl⟩