Theorem: cycleAtTo_mono (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
⊢ Monotone fun x => CycleAtTo π x
Tactic:
intros a b hab x y h
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a b : ℕ
hab : a ≤ b
x y : α
h : y ∈ (fun x => CycleAtTo π x) a x
⊢ y ∈ (fun x => CycleAtTo π x) b x

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a b : ℕ
hab : a ≤ b
x y : α
h : y ∈ (fun x => CycleAtTo π x) a x
⊢ y ∈ (fun x => CycleAtTo π x) b x
Tactic:
rw [mem_cycleAtTo_iff] at h ⊢
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a b : ℕ
hab : a ≤ b
x y : α
h : ∃ b < a, (π ^ b) x = y
⊢ ∃ b_1 < b, (π ^ b_1) x = y

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a b : ℕ
hab : a ≤ b
x y : α
h : ∃ b < a, (π ^ b) x = y
⊢ ∃ b_1 < b, (π ^ b_1) x = y
Tactic:
rcases h with ⟨c, hca, hc⟩
State after:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a b : ℕ
hab : a ≤ b
x y : α
c : ℕ
hca : c < a
hc : (π ^ c) x = y
⊢ ∃ b_1 < b, (π ^ b_1) x = y

State before:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a b : ℕ
hab : a ≤ b
x y : α
c : ℕ
hca : c < a
hc : (π ^ c) x = y
⊢ ∃ b_1 < b, (π ^ b_1) x = y
Tactic:
exact ⟨c, lt_of_lt_of_le hca hab, hc⟩
State after:
no goals