ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
⊢ ∃ i x_1, ↑(f ^ i) x = y
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : x ∈ support f
⊢ ∃ i x_1, ↑(f ^ i) x = y
rw [mem_support] at hx
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
this : ∃ n, n < card (support (cycleOf f x)) ∧ ↑(f ^ n) x = y
⊢ ∃ i x_1, ↑(f ^ i) x = y
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
⊢ ∃ i x_1, ↑(f ^ i) x = y
have := Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf x)
  (by rw [mem_support_cycleOf_iff' hx]) (by rwa [mem_support_cycleOf_iff' hx])
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
this : ∃ n _h, ↑(f ^ n) x = y
⊢ ∃ i x_1, ↑(f ^ i) x = y
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
this : ∃ n, n < card (support (cycleOf f x)) ∧ ↑(f ^ n) x = y
⊢ ∃ i x_1, ↑(f ^ i) x = y
simp_rw [← exists_prop] at this
no goals
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
this : ∃ n _h, ↑(f ^ n) x = y
⊢ ∃ i x_1, ↑(f ^ i) x = y
exact this
no goals
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
⊢ ?m.2617372 ∈ support (cycleOf f x)
rw [mem_support_cycleOf_iff' hx]
no goals
ι : Type ?u.2586211
α : Type u_1
β : Type ?u.2586217
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : SameCycle f x y
hx : ↑f x ≠ x
⊢ y ∈ support (cycleOf f x)
rwa [mem_support_cycleOf_iff' hx]