ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
⊢ (∀ (x_1 : α), (if SameCycle f x x_1 then ↑f x_1 else x_1) = x_1) ↔ ↑f x = x
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
⊢ cycleOf f x = 1 ↔ ↑f x = x
simp_rw [ext_iff, cycleOf_apply, one_apply]
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
⊢ (if SameCycle f x y then ↑f y else y) = y
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
⊢ (∀ (x_1 : α), (if SameCycle f x x_1 then ↑f x_1 else x_1) = x_1) ↔ ↑f x = x
refine' ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => _⟩
case pos
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
hy : ↑f y = y
⊢ (if SameCycle f x y then ↑f y else y) = y

case neg
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
hy : ¬↑f y = y
⊢ (if SameCycle f x y then ↑f y else y) = y
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
⊢ (if SameCycle f x y then ↑f y else y) = y
by_cases hy : f y = y
no goals
case pos
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
hy : ↑f y = y
⊢ (if SameCycle f x y then ↑f y else y) = y
rw [hy, ite_self]
no goals
case neg
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
hy : ¬↑f y = y
⊢ (if SameCycle f x y then ↑f y else y) = y
exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))
no goals
ι : Type ?u.2371612
α : Type u_1
β : Type ?u.2371618
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y✝ : α
f : Perm α
h : ↑f x = x
y : α
hy : ¬↑f y = y
⊢ ¬(↑f x = x ↔ ↑f y = y)
tauto