case inl
ι : Type ?u.2510500
α : Type u_1
β : Type ?u.2510506
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : Disjoint f g
x : α
hfx : ↑f x = x
⊢ cycleOf (f * g) x = cycleOf f x * cycleOf g x

case inr
ι : Type ?u.2510500
α : Type u_1
β : Type ?u.2510506
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : Disjoint f g
x : α
hgx : ↑g x = x
⊢ cycleOf (f * g) x = cycleOf f x * cycleOf g x
ι : Type ?u.2510500
α : Type u_1
β : Type ?u.2510506
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : Disjoint f g
x : α
⊢ cycleOf (f * g) x = cycleOf f x * cycleOf g x
cases' (disjoint_iff_eq_or_eq.mp h) x with hfx hgx
no goals
case inl
ι : Type ?u.2510500
α : Type u_1
β : Type ?u.2510506
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : Disjoint f g
x : α
hfx : ↑f x = x
⊢ cycleOf (f * g) x = cycleOf f x * cycleOf g x
simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
no goals
case inr
ι : Type ?u.2510500
α : Type u_1
β : Type ?u.2510506
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x✝ y : α
h : Disjoint f g
x : α
hgx : ↑g x = x
⊢ cycleOf (f * g) x = cycleOf f x * cycleOf g x
simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]