ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : 2 ≤ card (support (cycleOf f x))
⊢ ↑f x ≠ x
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ 2 ≤ card (support (cycleOf f x)) ↔ ↑f x ≠ x
refine' ⟨fun h => _, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ↑f x = x
⊢ card (support (cycleOf f x)) < 2
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : 2 ≤ card (support (cycleOf f x))
⊢ ↑f x ≠ x
contrapose! h
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h✝ : ↑f x = x
h : cycleOf f x = 1
⊢ card (support (cycleOf f x)) < 2
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ↑f x = x
⊢ card (support (cycleOf f x)) < 2
rw [← cycleOf_eq_one_iff] at h
no goals
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h✝ : ↑f x = x
h : cycleOf f x = 1
⊢ card (support (cycleOf f x)) < 2
simp [h]
no goals
ι : Type ?u.2441167
α : Type u_1
β : Type ?u.2441173
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ↑f x ≠ x
⊢ 2 ≤ card (support (cycleOf f x))
simpa using (isCycle_cycleOf _ h).two_le_card_support