case H
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
⊢ ↑(cycleOf (f * g) x) y = ↑(cycleOf f x) y
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
⊢ cycleOf (f * g) x = cycleOf f x
ext y
case pos
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : SameCycle (f * g) x y
⊢ ↑(cycleOf (f * g) x) y = ↑(cycleOf f x) y

case neg
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : ¬SameCycle (f * g) x y
⊢ ↑(cycleOf (f * g) x) y = ↑(cycleOf f x) y
case H
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
⊢ ↑(cycleOf (f * g) x) y = ↑(cycleOf f x) y
by_cases hxy : (f * g).SameCycle x y
case pos.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ ↑(cycleOf (f * g) x) (↑((f * g) ^ z) x) = ↑(cycleOf f x) (↑((f * g) ^ z) x)
case pos
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : SameCycle (f * g) x y
⊢ ↑(cycleOf (f * g) x) y = ↑(cycleOf f x) y
obtain ⟨z, rfl⟩ := hxy
case pos.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ ↑((f * g) ^ (z + 1)) x = ↑(cycleOf f x) (↑((f * g) ^ z) x)
case pos.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ ↑(cycleOf (f * g) x) (↑((f * g) ^ z) x) = ↑(cycleOf f x) (↑((f * g) ^ z) x)
rw [cycleOf_apply_apply_zpow_self]
no goals
case pos.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ ↑((f * g) ^ (z + 1)) x = ↑(cycleOf f x) (↑((f * g) ^ z) x)
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
case neg
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : ¬SameCycle (f * g) x y
⊢ ¬SameCycle f x y
case neg
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : ¬SameCycle (f * g) x y
⊢ ↑(cycleOf (f * g) x) y = ↑(cycleOf f x) y
rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
case neg
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : SameCycle f x y
⊢ SameCycle (f * g) x y
case neg
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : ¬SameCycle (f * g) x y
⊢ ¬SameCycle f x y
contrapose! hxy
case neg.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ SameCycle (f * g) x (↑(f ^ z) x)
case neg
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y✝ : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
y : α
hxy : SameCycle f x y
⊢ SameCycle (f * g) x y
obtain ⟨z, rfl⟩ := hxy
case neg.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ ↑((f * g) ^ z) x = ↑(f ^ z) x
case neg.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ SameCycle (f * g) x (↑(f ^ z) x)
refine' ⟨z, _⟩
no goals
case neg.intro
ι : Type ?u.2506488
α : Type u_1
β : Type ?u.2506494
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : _root_.Commute f g
x : α
hx : ↑g x = x
z : ℤ
⊢ ↑((f * g) ^ z) x = ↑(f ^ z) x
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]