Theorem: cycleAtTo_strict_mono_lt_of_lt_lt_orderOf (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
b : ℕ
ha : a < orderOf (π.cycleOf x)
hab : a < b
⊢ CycleAtTo π a x ⊂ CycleAtTo π b x
Tactic:
rw [Finset.ssubset_iff]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
b : ℕ
ha : a < orderOf (π.cycleOf x)
hab : a < b
⊢ ∃ a_1 ∉ CycleAtTo π a x, insert a_1 (CycleAtTo π a x) ⊆ CycleAtTo π b x

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
b : ℕ
ha : a < orderOf (π.cycleOf x)
hab : a < b
⊢ ∃ a_1 ∉ CycleAtTo π a x, insert a_1 (CycleAtTo π a x) ⊆ CycleAtTo π b x
Tactic:
exact ⟨_, pow_apply_not_mem_cycleAtTo_of_lt_orderOf_cycleOf ha, insert_cycleAtTo (le_refl _) hab⟩
State after:
no goals