ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ Disjoint (g * f⁻¹) f
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : f ∈ cycleFactorsFinset g
⊢ Disjoint (g * f⁻¹) f
rw [mem_cycleFactorsFinset_iff] at h
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
⊢ ↑(g * f⁻¹) x = x ∨ ↑f x = x
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ Disjoint (g * f⁻¹) f
intro x
case pos
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ↑f x = x
⊢ ↑(g * f⁻¹) x = x ∨ ↑f x = x

case neg
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ¬↑f x = x
⊢ ↑(g * f⁻¹) x = x ∨ ↑f x = x
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
⊢ ↑(g * f⁻¹) x = x ∨ ↑f x = x
by_cases hx : f x = x
no goals
case pos
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ↑f x = x
⊢ ↑(g * f⁻¹) x = x ∨ ↑f x = x
exact Or.inr hx
case neg
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ¬↑f x = x
⊢ ↑(g * f⁻¹) x = x
case neg
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ¬↑f x = x
⊢ ↑(g * f⁻¹) x = x ∨ ↑f x = x
refine' Or.inl _
case neg.a
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ¬↑f x = x
⊢ ↑f⁻¹ x ∈ support f
case neg
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ¬↑f x = x
⊢ ↑(g * f⁻¹) x = x
rw [mul_apply, ← h.right, apply_inv_self]
no goals
case neg.a
ι : Type ?u.2773969
α : Type u_1
β : Type ?u.2773975
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
x : α
hx : ¬↑f x = x
⊢ ↑f⁻¹ x ∈ support f
rwa [← support_inv, apply_mem_support, support_inv, mem_support]