Theorem: OnCycleFactors.Kf_mul_add (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ Kf a (e' * e) (c, i + j) = (g ^ i) (Kf a e' (e c, j))
Tactic:
simp only [Kf_def, zpow_add, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
no goals