case intro
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
⊢ f ^ a = f ^ b ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
cases nonempty_fintype β
case intro.mp
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b → ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x

case intro.mpr
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
⊢ (∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x) → f ^ a = f ^ b
case intro
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
constructor
case intro.mp
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
case intro.mp
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b → ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
intro h
case intro.mp.intro.intro
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : ↑f x ≠ x
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
case intro.mp
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
obtain ⟨x, hx, -⟩ := id hf
no goals
case intro.mp.intro.intro
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : ↑f x ≠ x
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x
exact ⟨x, hx, by simp [h]⟩
no goals
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : ↑f x ≠ x
⊢ ↑(f ^ a) x = ↑(f ^ b) x
simp [h]
case intro.mpr.intro.intro
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ a) x = ↑(f ^ b) x
⊢ f ^ a = f ^ b
case intro.mpr
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
⊢ (∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x) → f ^ a = f ^ b
rintro ⟨x, hx, hx'⟩
case intro.mpr.intro.intro.inr
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ a) x = ↑(f ^ b) x
this : ∀ {a b : ℕ}, ↑(f ^ a) x = ↑(f ^ b) x → a ≤ b → f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
⊢ f ^ a = f ^ b
case intro.mpr.intro.intro
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ a) x = ↑(f ^ b) x
⊢ f ^ a = f ^ b
wlog hab : a ≤ b generalizing a b
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
⊢ f ^ (b - a) = 1
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
⊢ f ^ a = f ^ b
suffices f ^ (b - a) = 1 by
  rw [pow_sub _ hab, mul_inv_eq_one] at this
  rw [this]
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
⊢ f ^ (b - a) = 1
rw [hf.pow_eq_one_iff]
case pos
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ↑(f ^ a) x ∈ support f
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x

case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ¬↑(f ^ a) x ∈ support f
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
by_cases hfa : (f ^ a) x ∈ f.support
no goals
case intro.mpr.intro.intro.inr
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
a b : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ a) x = ↑(f ^ b) x
this : ∀ {a b : ℕ}, ↑(f ^ a) x = ↑(f ^ b) x → a ≤ b → f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b
exact (this hx'.symm (le_of_not_le hab)).symm
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
this : f ^ (b - a) = 1
⊢ f ^ a = f ^ b
rw [pow_sub _ hab, mul_inv_eq_one] at this
no goals
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b
rw [this]
case pos
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ↑(f ^ a) x ∈ support f
⊢ ↑(f ^ (b - a)) (↑(f ^ a) x) = ↑(f ^ a) x
case pos
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ↑(f ^ a) x ∈ support f
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
refine' ⟨(f ^ a) x, mem_support.mp hfa, _⟩
no goals
case pos
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ↑(f ^ a) x ∈ support f
⊢ ↑(f ^ (b - a)) (↑(f ^ a) x) = ↑(f ^ a) x
simp only [pow_sub _ hab, Equiv.Perm.coe_mul, Function.comp_apply, inv_apply_self, ← hx']
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ¬↑(f ^ a) x ∈ support f
h : ↑(f ^ 1) (↑(f ^ ↑a) x) = ↑(f ^ ↑a) (↑(f ^ 1) x)
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ¬↑(f ^ a) x ∈ support f
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ¬↑(f ^ a) x ∈ support f
h : ↑f (↑(f ^ a) x) = ↑(f ^ a) (↑f x)
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ¬↑(f ^ a) x ∈ support f
h : ↑(f ^ 1) (↑(f ^ ↑a) x) = ↑(f ^ ↑a) (↑(f ^ 1) x)
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
simp only [zpow_one, zpow_ofNat] at h
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ↑f x = x
h : ↑f (↑(f ^ a) x) = ↑(f ^ a) (↑f x)
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ¬↑(f ^ a) x ∈ support f
h : ↑f (↑(f ^ a) x) = ↑(f ^ a) (↑f x)
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
rw [not_mem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
no goals
case neg
ι : Type ?u.1415307
α : Type ?u.1415310
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
a b : ℕ
hx' : ↑(f ^ a) x = ↑(f ^ b) x
hab : a ≤ b
hfa : ↑f x = x
h : ↑f (↑(f ^ a) x) = ↑(f ^ a) (↑f x)
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ (b - a)) x = x
contradiction