internlm/Lean-Github huggingface dataset:
Theorem: apply_pow_mem_cycleAtTo_apply_pow_of_ge_of_lt
Proof 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]
Proof 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)
Theorem: apply_pow_mem_cycleAtTo_apply_pow_of_ge_of_lt
Proof 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)
Proof state after:
no goals
Theorem: cycleAtTo_zero
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAtTo π 0 x = ∅
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAtTo_iff, not_lt_zero', false_and, exists_false,
  not_mem_empty, implies_true]
Proof state after:
no goals
Theorem: cycleAtTo_one
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAtTo π 1 x = {x}
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAtTo_iff, Nat.lt_one_iff, exists_eq_left, pow_zero,
  Perm.one_apply, mem_singleton, eq_comm, implies_true]
Proof state after:
no goals
Theorem: cycleAtTo_singleton_of_fixedPt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
ha : 0 < a
h : Function.IsFixedPt (⇑π) x
⊢ CycleAtTo π a x = {x}
Tactic:
simp_rw [Finset.ext_iff, mem_singleton, mem_cycleAtTo_iff,
  π.pow_apply_eq_self_of_apply_eq_self h, eq_comm (a := x)]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
ha : 0 < a
h : Function.IsFixedPt (⇑π) x
⊢ ∀ (a_1 : α), (∃ b < a, a_1 = x) ↔ a_1 = x
Theorem: cycleAtTo_singleton_of_fixedPt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
ha : 0 < a
h : Function.IsFixedPt (⇑π) x
⊢ ∀ (a_1 : α), (∃ b < a, a_1 = x) ↔ a_1 = x
Tactic:
exact fun _ => ⟨fun ⟨_, _, h⟩ => h, fun h => ⟨0, ha, h⟩⟩
Proof state after:
no goals
Theorem: cycleAtTo_mono
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
⊢ Monotone fun x => CycleAtTo π x
Tactic:
intros a b hab x y h
Proof 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
Theorem: cycleAtTo_mono
Proof 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 ⊢
Proof 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
Theorem: cycleAtTo_mono
Proof 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⟩
Proof 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
Theorem: cycleAtTo_mono
Proof 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⟩
Proof state after:
no goals
Theorem: card_cycleAtTo_le
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ (CycleAtTo π a x).card ≤ a
Tactic:
convert Finset.card_image_le
Proof state after:
case h.e'_4
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ a = (Iio a).card
Theorem: card_cycleAtTo_le
Proof state before:
case h.e'_4
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ a = (Iio a).card
Tactic:
exact (Nat.card_Iio _).symm
Proof state after:
no goals
Theorem: cycleAtTo_card_eq_of_le_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ (CycleAtTo π a x).card = a
Tactic:
nth_rewrite 2 [← Nat.card_Iio a]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ (CycleAtTo π a x).card = (Iio a).card
Theorem: cycleAtTo_card_eq_of_le_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ (CycleAtTo π a x).card = (Iio a).card
Tactic:
apply Finset.card_image_iff.mpr
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ Set.InjOn (fun k => (π ^ k) x) ↑(Iio a)
Theorem: cycleAtTo_card_eq_of_le_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ Set.InjOn (fun k => (π ^ k) x) ↑(Iio a)
Tactic:
intros b hb c hc hbc
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b : ℕ
hb : b ∈ ↑(Iio a)
c : ℕ
hc : c ∈ ↑(Iio a)
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
⊢ b = c
Theorem: cycleAtTo_card_eq_of_le_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b : ℕ
hb : b ∈ ↑(Iio a)
c : ℕ
hc : c ∈ ↑(Iio a)
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
⊢ b = c
Tactic:
simp_rw [coe_Iio, Set.mem_Iio] at hb hc
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b c : ℕ
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
hb : b < a
hc : c < a
⊢ b = c
Theorem: cycleAtTo_card_eq_of_le_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b c : ℕ
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
hb : b < a
hc : c < a
⊢ b = c
Tactic:
exact π.pow_apply_injOn_Iio_orderOf_cycleOf (lt_of_lt_of_le hb h) (lt_of_lt_of_le hc h) hbc
Proof state after:
no goals
Theorem: cycleAtTo_subset_cycleAt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ CycleAtTo π a x ⊆ CycleAt π x
Tactic:
rintro y hy
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
⊢ y ∈ CycleAt π x
Theorem: cycleAtTo_subset_cycleAt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
⊢ y ∈ CycleAt π x
Tactic:
rcases (mem_cycleAtTo_iff.mp hy) with ⟨b, _, hb⟩
Proof state after:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
b : ℕ
left✝ : b < a
hb : (π ^ b) x = y
⊢ y ∈ CycleAt π x
Theorem: cycleAtTo_subset_cycleAt
Proof state before:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
hy : y ∈ CycleAtTo π a x
b : ℕ
left✝ : b < a
hb : (π ^ b) x = y
⊢ y ∈ CycleAt π x
Tactic:
exact mem_cycleAt_iff.mpr ⟨b, hb⟩
Proof state after:
no goals
Theorem: cycleAt_eq_cycleAtTo_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π x = CycleAtTo π (orderOf (π.cycleOf x)) x
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAtTo_iff, mem_cycleAt_iff_lt, implies_true]
Proof state after:
no goals
Theorem: cycleAt_card_eq_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ orderOf (π.cycleOf x) = (CycleAt π x).card
Tactic:
simp_rw [cycleAt_eq_cycleAtTo_orderOf_cycleOf, cycleAtTo_card_eq_of_le_orderOf_cycleOf (le_refl _)]
Proof state after:
no goals
Theorem: cycleAt_eq_cycleAtTo_ge_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAt π x = CycleAtTo π a x
Tactic:
refine le_antisymm ?_ ?_
Proof state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAt π x ≤ CycleAtTo π a x

case refine_2
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π a x ≤ CycleAt π x
Theorem: cycleAt_eq_cycleAtTo_ge_orderOf_cycleOf
Proof state before:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAt π x ≤ CycleAtTo π a x
Tactic:
rw [cycleAt_eq_cycleAtTo_orderOf_cycleOf]
Proof state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π (orderOf (π.cycleOf x)) x ≤ CycleAtTo π a x
Theorem: cycleAt_eq_cycleAtTo_ge_orderOf_cycleOf
Proof state before:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π (orderOf (π.cycleOf x)) x ≤ CycleAtTo π a x
Tactic:
exact cycleAtTo_of_mono ha
Proof state after:
no goals
Theorem: cycleAt_eq_cycleAtTo_ge_orderOf_cycleOf
Proof state before:
case refine_2
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π a x ≤ CycleAt π x
Tactic:
exact cycleAtTo_subset_cycleAt
Proof state after:
no goals
Theorem: insert_cycleAtTo_eq_succ
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ insert ((π ^ a) x) (CycleAtTo π a x) = CycleAtTo π (a + 1) x
Tactic:
ext y
Proof state after:
case a
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
⊢ y ∈ insert ((π ^ a) x) (CycleAtTo π a x) ↔ y ∈ CycleAtTo π (a + 1) x
Theorem: insert_cycleAtTo_eq_succ
Proof state before:
case a
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x y : α
⊢ y ∈ insert ((π ^ a) x) (CycleAtTo π a x) ↔ y ∈ CycleAtTo π (a + 1) x
Tactic:
simp_rw [mem_insert, mem_cycleAtTo_iff, Nat.lt_succ_iff_lt_or_eq, or_and_right, exists_or,
  exists_eq_left, or_comm (a := y = (π ^ a) x), eq_comm (b := (π^a) x)]
Proof state after:
no goals
Theorem: insert_cycleAtTo
Proof 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
Proof 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
Theorem: insert_cycleAtTo
Proof 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
Proof 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
Theorem: insert_cycleAtTo
Proof 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)
Proof 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
Theorem: insert_cycleAtTo
Proof 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]
Proof 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
Theorem: insert_cycleAtTo
Proof 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⟩
Proof state after:
no goals
Theorem: insert_cycleAtTo
Proof 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
Proof state after:
no goals
Theorem: pow_apply_not_mem_cycleAtTo_of_lt_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
⊢ (π ^ a) x ∉ CycleAtTo π a x
Tactic:
intro h
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h✝ : a < orderOf (π.cycleOf x)
h : (π ^ a) x ∈ CycleAtTo π a x
⊢ False
Theorem: pow_apply_not_mem_cycleAtTo_of_lt_orderOf_cycleOf
Proof 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
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h✝ : a < orderOf (π.cycleOf x)
h : ∃ b < a, (π ^ b) x = (π ^ a) x
⊢ False
Theorem: pow_apply_not_mem_cycleAtTo_of_lt_orderOf_cycleOf
Proof 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⟩
Proof 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
Theorem: pow_apply_not_mem_cycleAtTo_of_lt_orderOf_cycleOf
Proof 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)
Proof state after:
no goals
Theorem: cycleAtTo_strict_mono_lt_of_lt_lt_orderOf
Proof 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]
Proof 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
Theorem: cycleAtTo_strict_mono_lt_of_lt_lt_orderOf
Proof 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⟩
Proof state after:
no goals
Theorem: cycleAt_gt_cycleAtTo_lt_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
⊢ CycleAtTo π a x ⊂ CycleAt π x
Tactic:
rw [cycleAt_eq_cycleAtTo_orderOf_cycleOf]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
⊢ CycleAtTo π a x ⊂ CycleAtTo π (orderOf (π.cycleOf x)) x
Theorem: cycleAt_gt_cycleAtTo_lt_orderOf_cycleOf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
⊢ CycleAtTo π a x ⊂ CycleAtTo π (orderOf (π.cycleOf x)) x
Tactic:
exact cycleAtTo_strict_mono_lt_of_lt_lt_orderOf h h
Proof state after:
no goals
Theorem: cycleMin_eq_min_cycleAtTo
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ CycleMin π x = (CycleAtTo π (orderOf (π.cycleOf x)) x).min' ⋯
Tactic:
simp_rw [cycleMin_def, cycleAt_eq_cycleAtTo_orderOf_cycleOf]
Proof state after:
no goals
Theorem: cycleMin_of_fixed
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
h : Function.IsFixedPt (⇑π) x
⊢ CycleMin π x = x
Tactic:
simp_rw [cycleMin_eq_min_cycleAtTo, π.cycleOf_eq_one_iff.mpr h, orderOf_one,
  cycleAtTo_one, min'_singleton]
Proof state after:
no goals
Theorem: cycleMin_eq_min_cycleAtTo_ge
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
a : ℕ
cycleAtTo_nonempty : (CycleAtTo π a x).Nonempty
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleMin π x = (CycleAtTo π a x).min' cycleAtTo_nonempty
Tactic:
simp_rw [cycleMin_def, cycleAt_eq_cycleAtTo_ge_orderOf_cycleOf ha]
Proof state after:
no goals
Theorem: cycleMin_le
Proof state before:
α : Type u
inst✝² : DecidableEq α
π✝ : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
y : α
π : Perm α
x : α
h : π.SameCycle x y
⊢ CycleMin π x ≤ y
Tactic:
rw [cycleMin_def]
Proof state after:
α : Type u
inst✝² : DecidableEq α
π✝ : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
y : α
π : Perm α
x : α
h : π.SameCycle x y
⊢ (CycleAt π x).min' ⋯ ≤ y
Theorem: cycleMin_le
Proof state before:
α : Type u
inst✝² : DecidableEq α
π✝ : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
y : α
π : Perm α
x : α
h : π.SameCycle x y
⊢ (CycleAt π x).min' ⋯ ≤ y
Tactic:
exact Finset.min'_le _ y (mem_cycleAt_iff.mpr h)
Proof state after:
no goals
Theorem: le_cycleMin
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x z : α
h : ∀ (y : α), π.SameCycle x y → z ≤ y
⊢ z ≤ CycleMin π x
Tactic:
simp_rw [cycleMin_def, Finset.le_min'_iff, mem_cycleAt_iff]
Proof state after:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x z : α
h : ∀ (y : α), π.SameCycle x y → z ≤ y
⊢ ∀ (y : α), π.SameCycle x y → z ≤ y
Theorem: le_cycleMin
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x z : α
h : ∀ (y : α), π.SameCycle x y → z ≤ y
⊢ ∀ (y : α), π.SameCycle x y → z ≤ y
Tactic:
exact h
Proof state after:
no goals
Theorem: le_cycleMin_iff
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
z x : α
⊢ z ≤ CycleMin π x ↔ ∀ (y : α), π.SameCycle x y → z ≤ y
Tactic:
simp_rw [cycleMin_def, Finset.le_min'_iff, mem_cycleAt_iff]
Proof state after:
no goals
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
x : α
⊢ FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
Tactic:
induction' i with i hi generalizing x
Proof state after:
case zero
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ FastCycleMin 0 π x = (CycleAtTo π (2 ^ 0) x).min' ⋯

case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ FastCycleMin (i + 1) π x = (CycleAtTo π (2 ^ (i + 1)) x).min' ⋯
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case zero
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ FastCycleMin 0 π x = (CycleAtTo π (2 ^ 0) x).min' ⋯
Tactic:
simp_rw [fastCycleMin_zero_eq, pow_zero, cycleAtTo_one, min'_singleton]
Proof state after:
no goals
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ FastCycleMin (i + 1) π x = (CycleAtTo π (2 ^ (i + 1)) x).min' ⋯
Tactic:
simp_rw [fastCycleMin_succ_eq, hi, le_antisymm_iff, le_min_iff, Finset.le_min'_iff, min_le_iff,
  mem_cycleAtTo_iff, Nat.pow_succ', Nat.two_mul, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, ← forall_and, ← Equiv.Perm.mul_apply, ← pow_add, imp_and]
Proof state after:
case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ ∀ (x_1 : ℕ),
    (x_1 < 2 ^ i + 2 ^ i →
        (CycleAtTo π (2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x ∨ (CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)).min' ⋯ ≤ (π ^ x_1) x) ∧
      (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x) ∧
        (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ (x_1 + 2 ^ i)) x)
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ ∀ (x_1 : ℕ),
    (x_1 < 2 ^ i + 2 ^ i →
        (CycleAtTo π (2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x ∨ (CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)).min' ⋯ ≤ (π ^ x_1) x) ∧
      (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x) ∧
        (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ (x_1 + 2 ^ i)) x)
Tactic:
refine' fun b => And.intro (fun h => (lt_or_le b (2^i)).imp _ _) (And.intro _ _) <;>
refine' fun hb => min'_le _ _ _
Proof state after:
case succ.refine'_1
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) x

case succ.refine'_2
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : 2 ^ i ≤ b
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)

case succ.refine'_3
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x

case succ.refine'_4
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ (b + 2 ^ i)) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case succ.refine'_1
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) x
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt hb
Proof state after:
no goals
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case succ.refine'_2
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : 2 ^ i ≤ b
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)
Tactic:
exact apply_pow_mem_cycleAtTo_apply_pow_of_ge_of_lt h hb
Proof state after:
no goals
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case succ.refine'_3
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt (lt_of_lt_of_le hb le_self_add)
Proof state after:
no goals