case intro.zero.intro
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
hi : Nat.zero < orderOf f
h : SameCycle f x (↑(f ^ Nat.zero) x)
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = ↑(f ^ Nat.zero) x

case intro.succ.intro
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
i : ℕ
hi : Nat.succ i < orderOf f
h : SameCycle f x (↑(f ^ Nat.succ i) x)
⊢ ∃ i_1 x_1 x_2, ↑(f ^ i_1) x = ↑(f ^ Nat.succ i) x
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x y z : α
inst✝ : Finite α
h : SameCycle f x y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
case intro.zero.intro
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
hi : Nat.zero < orderOf f
h : SameCycle f x (↑(f ^ Nat.zero) x)
⊢ ↑(f ^ orderOf f) x = ↑(f ^ Nat.zero) x
case intro.zero.intro
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
hi : Nat.zero < orderOf f
h : SameCycle f x (↑(f ^ Nat.zero) x)
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = ↑(f ^ Nat.zero) x
refine' ⟨orderOf f, orderOf_pos f, le_rfl, _⟩
no goals
case intro.zero.intro
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
hi : Nat.zero < orderOf f
h : SameCycle f x (↑(f ^ Nat.zero) x)
⊢ ↑(f ^ orderOf f) x = ↑(f ^ Nat.zero) x
rw [pow_orderOf_eq_one, pow_zero]
no goals
case intro.succ.intro
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
i : ℕ
hi : Nat.succ i < orderOf f
h : SameCycle f x (↑(f ^ Nat.succ i) x)
⊢ ∃ i_1 x_1 x_2, ↑(f ^ i_1) x = ↑(f ^ Nat.succ i) x
exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩
no goals
ι : Type ?u.239854
α : Type u_1
β : Type ?u.239860
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
i : ℕ
hi : Nat.succ i < orderOf f
h : SameCycle f x (↑(f ^ Nat.succ i) x)
⊢ ↑(f ^ Nat.succ i) x = ↑(f ^ Nat.succ i) x
rfl