Theorem: cycleAtTo_singleton_of_fixedPt (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
ha : 0 < a
h : Function.IsFixedPt (⇑π) x
⊢ CycleAtTo π a x = {x}
Tactic:
simp_rw [Finset.ext_iff, mem_singleton, mem_cycleAtTo_iff,
  π.pow_apply_eq_self_of_apply_eq_self h, eq_comm (a := x)]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
ha : 0 < a
h : Function.IsFixedPt (⇑π) x
⊢ ∀ (a_1 : α), (∃ b < a, a_1 = x) ↔ a_1 = x

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
ha : 0 < a
h : Function.IsFixedPt (⇑π) x
⊢ ∀ (a_1 : α), (∃ b < a, a_1 = x) ↔ a_1 = x
Tactic:
exact fun _ => ⟨fun ⟨_, _, h⟩ => h, fun h => ⟨0, ha, h⟩⟩
State after:
no goals