Theorem: apply_pow_mem_cycleAtTo_apply_pow_of_ge_of_lt (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
b a c : ℕ
x : α
hba : b < a + c
hcb : c ≤ b
⊢ (π ^ b) x ∈ CycleAtTo π a ((π ^ c) x)
Tactic:
rw [← tsub_add_cancel_of_le hcb, pow_add, Perm.mul_apply]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
b a c : ℕ
x : α
hba : b < a + c
hcb : c ≤ b
⊢ (π ^ (b - c)) ((π ^ c) x) ∈ CycleAtTo π a ((π ^ c) x)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
b a c : ℕ
x : α
hba : b < a + c
hcb : c ≤ b
⊢ (π ^ (b - c)) ((π ^ c) x) ∈ CycleAtTo π a ((π ^ c) x)
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt (Nat.sub_lt_right_of_lt_add hcb hba)
State after:
no goals