Theorem: pow_apply_not_mem_cycleAtTo_of_lt_orderOf_cycleOf (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
⊢ (π ^ a) x ∉ CycleAtTo π a x
Tactic:
intro h
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h✝ : a < orderOf (π.cycleOf x)
h : (π ^ a) x ∈ CycleAtTo π a x
⊢ False

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h✝ : a < orderOf (π.cycleOf x)
h : (π ^ a) x ∈ CycleAtTo π a x
⊢ False
Tactic:
rw [mem_cycleAtTo_iff] at h
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h✝ : a < orderOf (π.cycleOf x)
h : ∃ b < a, (π ^ b) x = (π ^ a) x
⊢ False

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h✝ : a < orderOf (π.cycleOf x)
h : ∃ b < a, (π ^ b) x = (π ^ a) x
⊢ False
Tactic:
rcases h with ⟨b, hb, hbx⟩
State after:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
b : ℕ
hb : b < a
hbx : (π ^ b) x = (π ^ a) x
⊢ False

State before:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
b : ℕ
hb : b < a
hbx : (π ^ b) x = (π ^ a) x
⊢ False
Tactic:
exact hb.ne (π.pow_apply_injOn_Iio_orderOf_cycleOf (hb.trans h) h hbx)
State after:
no goals