Theorem: Equiv.Perm.Basis.Kf_apply' (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd : d = e c
⊢ ↑d (Kf a e (c, i)) = Kf a e (c, i + 1)
Tactic:
rw [hd]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd : d = e c
⊢ ↑(e c) (Kf a e (c, i)) = Kf a e (c, i + 1)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd : d = e c
⊢ ↑(e c) (Kf a e (c, i)) = Kf a e (c, i + 1)
Tactic:
rw [Equiv.Perm.Basis.eq_cycleOf', Equiv.Perm.cycleOf_apply_self,
  Equiv.Perm.Basis.Kf_apply]
State after:
no goals