Theorem: Equiv.Perm.cycleOf_pow_apply (Controlbits/Cycles.lean)

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

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

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

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

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

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