Theorem: mem_cycleAt_iff_lt (Controlbits/Cycles.lean)

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]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ b < orderOf (π.cycleOf x), (π ^ b) x = y
Tactic:
refine ⟨?_, ?_⟩
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

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
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

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⟩
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

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 _ _)⟩
State after:
no goals

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⟩
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)

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⟩
State after:
no goals