case pos
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ↑f x = x
⊢ y ∈ support (cycleOf f x) ↔ SameCycle f x y ∧ x ∈ support f

case neg
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
⊢ y ∈ support (cycleOf f x) ↔ SameCycle f x y ∧ x ∈ support f
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ y ∈ support (cycleOf f x) ↔ SameCycle f x y ∧ x ∈ support f
by_cases hx : f x = x
case pos
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ↑f x = x
⊢ y ∈ support 1 ↔ SameCycle f x y ∧ x ∈ support f
case pos
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ↑f x = x
⊢ y ∈ support (cycleOf f x) ↔ SameCycle f x y ∧ x ∈ support f
rw [(cycleOf_eq_one_iff _).mpr hx]
no goals
case pos
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ↑f x = x
⊢ y ∈ support 1 ↔ SameCycle f x y ∧ x ∈ support f
simp [hx]
case neg
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
⊢ (if SameCycle f x y then ↑f y else y) ≠ y ↔ SameCycle f x y ∧ x ∈ support f
case neg
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
⊢ y ∈ support (cycleOf f x) ↔ SameCycle f x y ∧ x ∈ support f
rw [mem_support, cycleOf_apply]
case neg.inl
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
hy : SameCycle f x y
⊢ ↑f y ≠ y ↔ SameCycle f x y ∧ x ∈ support f

case neg.inr
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
hy : ¬SameCycle f x y
⊢ y ≠ y ↔ SameCycle f x y ∧ x ∈ support f
case neg
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
⊢ (if SameCycle f x y then ↑f y else y) ≠ y ↔ SameCycle f x y ∧ x ∈ support f
split_ifs with hy
case neg.inl
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
hy : SameCycle f x y
⊢ ¬↑f y = y
case neg.inl
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
hy : SameCycle f x y
⊢ ↑f y ≠ y ↔ SameCycle f x y ∧ x ∈ support f
simp only [hx, hy, iff_true_iff, Ne.def, not_false_iff, and_self_iff, mem_support]
case neg.inl.intro
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hx : ¬↑f x = x
k : ℤ
⊢ ¬↑f (↑(f ^ k) x) = ↑(f ^ k) x
case neg.inl
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
hy : SameCycle f x y
⊢ ¬↑f y = y
rcases hy with ⟨k, rfl⟩
case neg.inl.intro
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hx : ¬↑f x = x
k : ℤ
⊢ ¬¬↑(f ^ k) x ∈ support f
case neg.inl.intro
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hx : ¬↑f x = x
k : ℤ
⊢ ¬↑f (↑(f ^ k) x) = ↑(f ^ k) x
rw [← not_mem_support]
no goals
case neg.inl.intro
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hx : ¬↑f x = x
k : ℤ
⊢ ¬¬↑(f ^ k) x ∈ support f
simpa using hx
no goals
case neg.inr
ι : Type ?u.2515226
α : Type u_1
β : Type ?u.2515232
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ¬↑f x = x
hy : ¬SameCycle f x y
⊢ y ≠ y ↔ SameCycle f x y ∧ x ∈ support f
simpa [hx] using hy