no goals
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : y = x
⊢ ↑f y = ↑(swap x (↑f x)) y
simp [hyx]
no goals
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : y = ↑f x
⊢ ↑f y = ↑(swap x (↑f x)) y
simp [hfyx, hffx]
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
⊢ ↑f y = y
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
⊢ ↑f y = ↑(swap x (↑f x)) y
rw [swap_apply_of_ne_of_ne hyx hfyx]
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
⊢ False
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
⊢ ↑f y = y
refine' by_contradiction fun hy => _
case intro
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ j) z = y
⊢ False
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
⊢ False
cases' hz.2 hy with j hj
case intro
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ (j - i)) x = y
⊢ False
case intro
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ j) z = y
⊢ False
rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj
case intro.inl
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = x
⊢ False

case intro.inr
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = ↑f x
⊢ False
case intro
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ (j - i)) x = y
⊢ False
cases' zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji hji
case intro.inl
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hyx : ¬x = x
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = x
⊢ False
case intro.inl
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = x
⊢ False
rw [← hj, hji] at hyx
no goals
case intro.inl
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hyx : ¬x = x
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = x
⊢ False
tauto
case intro.inr
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hy : ¬↑f y = y
j : ℤ
hfyx : ¬↑f x = ↑f x
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = ↑f x
⊢ False
case intro.inr
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = ↑f x
hy : ¬↑f y = y
j : ℤ
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = ↑f x
⊢ False
rw [← hj, hji] at hfyx
no goals
case intro.inr
ι : Type ?u.816801
α✝ : Type ?u.816804
β : Type ?u.816807
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hfx : ↑f x ≠ x
hffx : ↑f (↑f x) = x
y z : α
hz : ↑f z ≠ z ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f z y
i : ℤ
hi : ↑(f ^ i) z = x
hyx : ¬y = x
hy : ¬↑f y = y
j : ℤ
hfyx : ¬↑f x = ↑f x
hj : ↑(f ^ (j - i)) x = y
hji : ↑(f ^ (j - i)) x = ↑f x
⊢ False
tauto