internlm/Lean-Github huggingface dataset:
Theorem: Fin.succAbove_le_succ
Proof state before:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.castSucc
⊢ i.castSucc ≤ i.succ
Tactic:
exact (castSucc_lt_succ _).le
Proof state after:
no goals
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
⊢ (j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rcases lt_or_le (castSucc i) j with (hij | hij)
Proof state after:
case inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k)

case inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_castSucc_lt _ _ hij, predAbove_of_castSucc_lt _ _ hij]
Proof state after:
case inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rcases lt_or_le (castSucc k) i with (hik | hik)
Proof state after:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)

case inl.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
have H := (castSucc_lt_iff_succ_le.mp
(castSucc_lt_castSucc_iff.mpr hik)).trans_lt hij
Proof state after:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
H : k.castSucc.succ < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
H : k.castSucc.succ < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_castSucc_lt _ _ hik, succAbove_of_succ_le _ _ H.le,
succAbove_of_castSucc_lt _ k ((lt_pred_iff _).mpr H), succAbove_castSucc_of_lt _ _ hik]
Proof state after:
no goals
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inl.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_le_castSucc _ _ hik,
succAbove_castSucc_of_le, ← succ_succAbove_succ, succ_pred]
Proof state after:
case inl.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i ≤ (j.pred ⋯).succAbove k
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inl.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i ≤ (j.pred ⋯).succAbove k
Tactic:
exact hik.trans (castSucc_le_succAbove _ _)
Proof state after:
no goals
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_le_castSucc _ _ hij, predAbove_of_le_castSucc _ _ hij]
Proof state after:
case inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rcases lt_or_le i (succ k) with (hik | hik)
Proof state after:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)

case inr.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
have H := ((hij.trans_lt (castSucc_lt_castSucc_iff.mpr hik)))
Proof state after:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
H : j < k.succ.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
H : j < k.succ.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_lt_succ _ _ hik, succAbove_of_le_castSucc _ _ H.le,
succAbove_of_lt_succ _ k ((castPred_lt_iff _).mpr H), succAbove_succ_of_lt _ _ hik]
Proof state after:
no goals
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inr.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_succ_le _ _ hik, succAbove_succ_of_le,
← castSucc_succAbove_castSucc, castSucc_castPred]
Proof state after:
case inr.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ (j.castPred ⋯).succAbove k ≤ i
Theorem: Fin.succAbove_succAbove_predAbove_succAbove
Proof state before:
case inr.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ (j.castPred ⋯).succAbove k ≤ i
Tactic:
exact (succAbove_le_succ _ _).trans hik
Proof state after:
no goals
Theorem: Equiv.Perm.cycleOf_pow_apply
Proof state before:
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x y : β
a : ℕ
⊢ (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
Tactic:
induction' a with a IH generalizing y
Proof state after:
case zero
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x y : β
⊢ (f.cycleOf x ^ 0) y = if f.SameCycle x y then (f ^ 0) y else y

case succ
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
⊢ (f.cycleOf x ^ (a + 1)) y = if f.SameCycle x y then (f ^ (a + 1)) y else y
Theorem: Equiv.Perm.cycleOf_pow_apply
Proof state before:
case zero
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x y : β
⊢ (f.cycleOf x ^ 0) y = if f.SameCycle x y then (f ^ 0) y else y
Tactic:
simp_rw [pow_zero, one_apply, ite_self]
Proof state after:
no goals
Theorem: Equiv.Perm.cycleOf_pow_apply
Proof state before:
case succ
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
⊢ (f.cycleOf x ^ (a + 1)) y = if f.SameCycle x y then (f ^ (a + 1)) y else y
Tactic:
simp_rw [pow_succ', mul_apply, IH, cycleOf_apply]
Proof state after:
case succ
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
⊢ (if f.SameCycle x (if f.SameCycle x y then (f ^ a) y else y) then f (if f.SameCycle x y then (f ^ a) y else y)
    else if f.SameCycle x y then (f ^ a) y else y) =
    if f.SameCycle x y then f ((f ^ a) y) else y
Theorem: Equiv.Perm.cycleOf_pow_apply
Proof state before:
case succ
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
⊢ (if f.SameCycle x (if f.SameCycle x y then (f ^ a) y else y) then f (if f.SameCycle x y then (f ^ a) y else y)
    else if f.SameCycle x y then (f ^ a) y else y) =
    if f.SameCycle x y then f ((f ^ a) y) else y
Tactic:
by_cases h : f.SameCycle x y
Proof state after:
case pos
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
h : f.SameCycle x y
⊢ (if f.SameCycle x (if f.SameCycle x y then (f ^ a) y else y) then f (if f.SameCycle x y then (f ^ a) y else y)
    else if f.SameCycle x y then (f ^ a) y else y) =
    if f.SameCycle x y then f ((f ^ a) y) else y

case neg
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
h : ¬f.SameCycle x y
⊢ (if f.SameCycle x (if f.SameCycle x y then (f ^ a) y else y) then f (if f.SameCycle x y then (f ^ a) y else y)
    else if f.SameCycle x y then (f ^ a) y else y) =
    if f.SameCycle x y then f ((f ^ a) y) else y
Theorem: Equiv.Perm.cycleOf_pow_apply
Proof state before:
case pos
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
h : f.SameCycle x y
⊢ (if f.SameCycle x (if f.SameCycle x y then (f ^ a) y else y) then f (if f.SameCycle x y then (f ^ a) y else y)
    else if f.SameCycle x y then (f ^ a) y else y) =
    if f.SameCycle x y then f ((f ^ a) y) else y
Tactic:
simp only [h, ↓reduceIte, sameCycle_pow_right]
Proof state after:
no goals
Theorem: Equiv.Perm.cycleOf_pow_apply
Proof state before:
case neg
α : Type ?u.39
π : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
β : Type v
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm β
x : β
a : ℕ
IH : ∀ (y : β), (f.cycleOf x ^ a) y = if f.SameCycle x y then (f ^ a) y else y
y : β
h : ¬f.SameCycle x y
⊢ (if f.SameCycle x (if f.SameCycle x y then (f ^ a) y else y) then f (if f.SameCycle x y then (f ^ a) y else y)
    else if f.SameCycle x y then (f ^ a) y else y) =
    if f.SameCycle x y then f ((f ^ a) y) else y
Tactic:
simp only [h, ↓reduceIte]
Proof state after:
no goals
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
⊢ Set.InjOn (fun t => (π ^ t) x) (Set.Iio (orderOf (π.cycleOf x)))
Tactic:
rintro a ha b hb hab
Proof state after:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
⊢ a = b
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
⊢ a = b
Tactic:
refine' pow_injOn_Iio_orderOf ha hb (ext (fun y => _))
Proof state after:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ ((fun x_1 => π.cycleOf x ^ x_1) a) y = ((fun x_1 => π.cycleOf x ^ x_1) b) y
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ ((fun x_1 => π.cycleOf x ^ x_1) a) y = ((fun x_1 => π.cycleOf x ^ x_1) b) y
Tactic:
simp_rw [cycleOf_pow_apply]
Proof state after:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Tactic:
by_cases h : SameCycle π x y
Proof state after:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y

case neg
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : ¬π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Tactic:
simp_rw [h, ite_true]
Proof state after:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (π ^ a) y = (π ^ b) y
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (π ^ a) y = (π ^ b) y
Tactic:
rcases h with ⟨c, rfl⟩
Proof state after:
case pos.intro
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
c : ℤ
⊢ (π ^ a) ((π ^ c) x) = (π ^ b) ((π ^ c) x)
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
case pos.intro
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
c : ℤ
⊢ (π ^ a) ((π ^ c) x) = (π ^ b) ((π ^ c) x)
Tactic:
simp_rw [← zpow_natCast, zpow_apply_comm, zpow_natCast, hab]
Proof state after:
no goals
Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf
Proof state before:
case neg
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : ¬π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Tactic:
simp_rw [h, ite_false]
Proof state after:
no goals
Theorem: mem_cycleAt_iff
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ π.SameCycle x y
Tactic:
simp_rw [CycleAt, mem_filter, mem_univ, true_and]
Proof state after:
no goals
Theorem: mem_cycleAt_iff_zpow
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ ∃ k, (π ^ k) x = y
Tactic:
simp_rw [mem_cycleAt_iff]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ k, (π ^ k) x = y
Theorem: mem_cycleAt_iff_zpow
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ k, (π ^ k) x = y
Tactic:
rfl
Proof state after:
no goals
Theorem: cycleAt_of_fixed
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
h : Function.IsFixedPt (⇑π) x
⊢ CycleAt π x = {x}
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAt_iff_zpow, mem_singleton, (fun k => (h.perm_zpow k).eq),
exists_const, eq_comm, implies_true]
Proof state after:
no goals
Theorem: card_cycleAt_eq_one_iff_fixedPt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ Function.IsFixedPt (⇑π) x ↔ (CycleAt π x).card = 1
Tactic:
rw [Finset.card_eq_one, fixedPt_iff_cycleAt_singleton]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π x = {x} ↔ ∃ a, CycleAt π x = {a}
Theorem: card_cycleAt_eq_one_iff_fixedPt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π x = {x} ↔ ∃ a, CycleAt π x = {a}
Tactic:
refine ⟨fun hx => ⟨_, hx⟩, ?_⟩
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ (∃ a, CycleAt π x = {a}) → CycleAt π x = {x}
Theorem: card_cycleAt_eq_one_iff_fixedPt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ (∃ a, CycleAt π x = {a}) → CycleAt π x = {x}
Tactic:
rintro ⟨_, hx⟩
Proof state after:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ CycleAt π x = {x}
Theorem: card_cycleAt_eq_one_iff_fixedPt
Proof state before:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ CycleAt π x = {x}
Tactic:
rw [hx, singleton_inj, eq_comm, ← mem_singleton, ← hx]
Proof state after:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ x ∈ CycleAt π x
Theorem: card_cycleAt_eq_one_iff_fixedPt
Proof state before:
case intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x w✝ : α
hx : CycleAt π x = {w✝}
⊢ x ∈ CycleAt π x
Tactic:
exact self_mem_cycleAt
Proof state after:
no goals
Theorem: cycleAt_apply_eq_cycleAt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π (π x) = CycleAt π x
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAt_iff, Perm.sameCycle_apply_left, implies_true]
Proof state after:
no goals
Theorem: mem_cycleAt_iff_lt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Tactic:
rw [mem_cycleAt_iff]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Theorem: mem_cycleAt_iff_lt
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y → ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y

case refine_2
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ (∃ b < orderOf (π.cycleOf x), (π ^ b) x = y) → π.SameCycle x y
Theorem: mem_cycleAt_iff_lt
Proof state before:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y → ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Tactic:
rintro hb
Proof state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
hb : π.SameCycle x y
⊢ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Theorem: mem_cycleAt_iff_lt
Proof state before:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
hb : π.SameCycle x y
⊢ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Tactic:
rcases (hb.exists_pow_eq π) with ⟨b, _, _, rfl⟩
Proof state after:
case refine_1.intro.intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
b : ℕ
left✝¹ : 0 < b
left✝ : b ≤ (π.cycleOf x).support.card + 1
hb : π.SameCycle x ((π ^ b) x)
⊢ ∃ b_1 < orderOf (π.cycleOf x), (π ^ b_1) x = (π ^ b) x
Theorem: mem_cycleAt_iff_lt
Proof state before:
case refine_1.intro.intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
b : ℕ
left✝¹ : 0 < b
left✝ : b ≤ (π.cycleOf x).support.card + 1
hb : π.SameCycle x ((π ^ b) x)
⊢ ∃ b_1 < orderOf (π.cycleOf x), (π ^ b_1) x = (π ^ b) x
Tactic:
refine ⟨b % orderOf (π.cycleOf x), Nat.mod_lt _ (orderOf_pos _),
  (π.pow_mod_orderOf_cycleOf_apply _ _)⟩
Proof state after:
no goals
Theorem: mem_cycleAt_iff_lt
Proof state before:
case refine_2
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ (∃ b < orderOf (π.cycleOf x), (π ^ b) x = y) → π.SameCycle x y
Tactic:
rintro ⟨b, _, rfl⟩
Proof state after:
case refine_2.intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
b : ℕ
left✝ : b < orderOf (π.cycleOf x)
⊢ π.SameCycle x ((π ^ b) x)
Theorem: mem_cycleAt_iff_lt
Proof state before:
case refine_2.intro.intro
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
b : ℕ
left✝ : b < orderOf (π.cycleOf x)
⊢ π.SameCycle x ((π ^ b) x)
Tactic:
exact ⟨b, rfl⟩
Proof state after:
no goals
Theorem: mem_cycleAt_iff_le
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ ∃ b ≤ orderOf (π.cycleOf x) - 1, (π ^ b) x = y
Tactic:
simp_rw [mem_cycleAt_iff_lt, Nat.lt_iff_le_pred (orderOf_pos _)]
Proof state after:
no goals
Theorem: mem_cycleAtTo_iff
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y : α
a : ℕ
x : α
⊢ y ∈ CycleAtTo π a x ↔ ∃ b < a, (π ^ b) x = y
Tactic:
simp_rw [CycleAtTo, Finset.mem_image, Finset.mem_Iio]
Proof state after:
no goals