Theorem: OnCycleFactors.Kf_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 : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ Kf a e (c, i + j) = (g ^ i) (Kf a 1 (e c, j))
Tactic:
rw [← Kf_mul_add, one_mul]
State after:
no goals