Theorem: cycleAtTo_subset_cycleAt (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ CycleAtTo π a x ⊆ CycleAt π x
Tactic:
rintro y hy
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
⊢ y ∈ CycleAt π x

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
⊢ y ∈ CycleAt π x
Tactic:
rcases (mem_cycleAtTo_iff.mp hy) with ⟨b, _, hb⟩
State after:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
b : ℕ
left✝ : b < a
hb : (π ^ b) x = y
⊢ y ∈ CycleAt π x

State before:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
b : ℕ
left✝ : b < a
hb : (π ^ b) x = y
⊢ y ∈ CycleAt π x
Tactic:
exact mem_cycleAt_iff.mpr ⟨b, hb⟩
State after:
no goals