case pos
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y

case neg
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
by_cases hx : x ∈ f.support
case pos.intro.intro
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
hk : k < card (support (cycleOf f x))
hk' : ↑(f ^ k) x = y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
case pos
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
case pos.intro.intro.zero
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y

case pos.intro.intro.succ
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
hk : Nat.succ k < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.succ k) x = y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
case pos.intro.intro
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
hk : k < card (support (cycleOf f x))
hk' : ↑(f ^ k) x = y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
cases' k with k
case pos.intro.intro.zero.refine'_1
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ 0 < card (support (cycleOf f x))

case pos.intro.intro.zero.refine'_2
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ ↑(f ^ card (support (cycleOf f x))) x = y
case pos.intro.intro.zero
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
refine' ⟨(f.cycleOf x).support.card, _, self_le_add_right _ _, _⟩
case pos.intro.intro.zero.refine'_1
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ cycleOf f x ≠ 1
case pos.intro.intro.zero.refine'_1
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ 0 < card (support (cycleOf f x))
refine' zero_lt_one.trans (one_lt_card_support_of_ne_one _)
no goals
case pos.intro.intro.zero.refine'_1
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ cycleOf f x ≠ 1
simpa using hx
case pos.intro.intro.zero.refine'_2
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : x = y
⊢ ↑(f ^ card (support (cycleOf f x))) x = y
case pos.intro.intro.zero.refine'_2
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.zero) x = y
⊢ ↑(f ^ card (support (cycleOf f x))) x = y
simp only [Nat.zero_eq, pow_zero, coe_one, id_eq] at hk'
case pos.intro.intro.zero.refine'_2
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x : α
f : Perm α
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
h : SameCycle f x x
⊢ ↑(f ^ card (support (cycleOf f x))) x = x
case pos.intro.intro.zero.refine'_2
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
hk' : x = y
⊢ ↑(f ^ card (support (cycleOf f x))) x = y
subst hk'
no goals
case pos.intro.intro.zero.refine'_2
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x : α
f : Perm α
hx : x ∈ support f
hk : Nat.zero < card (support (cycleOf f x))
h : SameCycle f x x
⊢ ↑(f ^ card (support (cycleOf f x))) x = x
rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
  pow_orderOf_eq_one, one_apply]
no goals
case pos.intro.intro.succ
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
hk : Nat.succ k < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.succ k) x = y
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
no goals
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
hk : Nat.succ k < card (support (cycleOf f x))
hk' : ↑(f ^ Nat.succ k) x = y
⊢ 0 < k + 1
simp
case neg
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ ↑(f ^ 1) x = y
case neg
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ ∃ i x_1 x_2, ↑(f ^ i) x = y
refine' ⟨1, zero_lt_one, by simp, _⟩
case neg.intro
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x : α
f : Perm α
hx : ¬x ∈ support f
k : ℤ
⊢ ↑(f ^ 1) x = ↑(f ^ k) x
case neg
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ ↑(f ^ 1) x = y
obtain ⟨k, rfl⟩ := h
case neg.intro
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x : α
f : Perm α
hx : ↑f x = x
k : ℤ
⊢ ↑(f ^ 1) x = ↑(f ^ k) x
case neg.intro
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x : α
f : Perm α
hx : ¬x ∈ support f
k : ℤ
⊢ ↑(f ^ 1) x = ↑(f ^ k) x
rw [not_mem_support] at hx
no goals
case neg.intro
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x : α
f : Perm α
hx : ↑f x = x
k : ℤ
⊢ ↑(f ^ 1) x = ↑(f ^ k) x
rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
no goals
ι : Type ?u.2618181
α : Type u_1
β : Type ?u.2618187
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ 1 ≤ card (support (cycleOf f x)) + 1
simp