Theorem: insert_cycleAtTo (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
⊢ insert ((π ^ k) x) (CycleAtTo π a x) ⊆ CycleAtTo π b x
Tactic:
intros y hy
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
y : α
hy : y ∈ insert ((π ^ k) x) (CycleAtTo π a x)
⊢ y ∈ CycleAtTo π b x

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
y : α
hy : y ∈ insert ((π ^ k) x) (CycleAtTo π a x)
⊢ y ∈ CycleAtTo π b x
Tactic:
rw [mem_insert] at hy
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
y : α
hy : y = (π ^ k) x ∨ y ∈ CycleAtTo π a x
⊢ y ∈ CycleAtTo π b x

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
y : α
hy : y = (π ^ k) x ∨ y ∈ CycleAtTo π a x
⊢ y ∈ CycleAtTo π b x
Tactic:
rcases hy with (rfl | hy)
State after:
case inl
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
⊢ (π ^ k) x ∈ CycleAtTo π b x

case inr
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
y : α
hy : y ∈ CycleAtTo π a x
⊢ y ∈ CycleAtTo π b x

State before:
case inl
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
⊢ (π ^ k) x ∈ CycleAtTo π b x
Tactic:
rw [mem_cycleAtTo_iff]
State after:
case inl
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
⊢ ∃ b_1 < b, (π ^ b_1) x = (π ^ k) x

State before:
case inl
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
⊢ ∃ b_1 < b, (π ^ b_1) x = (π ^ k) x
Tactic:
exact ⟨k, hkb, rfl⟩
State after:
no goals

State before:
case inr
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
k b : ℕ
x : α
a : ℕ
hak : a ≤ k
hkb : k < b
y : α
hy : y ∈ CycleAtTo π a x
⊢ y ∈ CycleAtTo π b x
Tactic:
exact cycleAtTo_of_mono (lt_of_le_of_lt hak hkb).le hy
State after:
no goals