Theorem: card_cycleAt_eq_one_iff_fixedPt (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ Function.IsFixedPt (⇑π) x ↔ (CycleAt π x).card = 1
Tactic:
rw [Finset.card_eq_one, fixedPt_iff_cycleAt_singleton]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π x = {x} ↔ ∃ a, CycleAt π x = {a}

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π x = {x} ↔ ∃ a, CycleAt π x = {a}
Tactic:
refine ⟨fun hx => ⟨_, hx⟩, ?_⟩
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ (∃ a, CycleAt π x = {a}) → CycleAt π x = {x}

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ (∃ a, CycleAt π x = {a}) → CycleAt π x = {x}
Tactic:
rintro ⟨_, hx⟩
State after:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ CycleAt π x = {x}

State before:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ CycleAt π x = {x}
Tactic:
rw [hx, singleton_inj, eq_comm, ← mem_singleton, ← hx]
State after:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ x ∈ CycleAt π x

State before:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ x ∈ CycleAt π x
Tactic:
exact self_mem_cycleAt
State after:
no goals