case H
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
⊢ ↑(cycleOf f x) z = ↑(cycleOf f y) z
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
⊢ cycleOf f x = cycleOf f y
ext z
case H
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
⊢ (if SameCycle f x z then ↑f z else z) = ↑(cycleOf f y) z
case H
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
⊢ ↑(cycleOf f x) z = ↑(cycleOf f y) z
rw [Equiv.Perm.cycleOf_apply]
case H.inl
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
hz : SameCycle f x z
⊢ ↑f z = ↑(cycleOf f y) z

case H.inr
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
hz : ¬SameCycle f x z
⊢ z = ↑(cycleOf f y) z
case H
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
⊢ (if SameCycle f x z then ↑f z else z) = ↑(cycleOf f y) z
split_ifs with hz
no goals
case H.inl
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
hz : SameCycle f x z
⊢ ↑f z = ↑(cycleOf f y) z
exact (h.symm.trans hz).cycleOf_apply.symm
no goals
case H.inr
ι : Type ?u.2244324
α : Type u_1
β : Type ?u.2244330
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
z : α
hz : ¬SameCycle f x z
⊢ z = ↑(cycleOf f y) z
exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm