Theorem: insert_cycleAtTo_eq_succ (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ insert ((π ^ a) x) (CycleAtTo π a x) = CycleAtTo π (a + 1) x
Tactic:
ext y
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
⊢ y ∈ insert ((π ^ a) x) (CycleAtTo π a x) ↔ y ∈ CycleAtTo π (a + 1) x

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
⊢ y ∈ insert ((π ^ a) x) (CycleAtTo π a x) ↔ y ∈ CycleAtTo π (a + 1) x
Tactic:
simp_rw [mem_insert, mem_cycleAtTo_iff, Nat.lt_succ_iff_lt_or_eq, or_and_right, exists_or,
  exists_eq_left, or_comm (a := y = (π ^ a) x), eq_comm (b := (π^a) x)]
State after:
no goals