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 e (c, j))
Tactic:
rw [← mul_one e, Kf_mul_add, mul_one]
State after:
α : 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 : ℤ
⊢ (g ^ i) (Kf a e (1 c, j)) = (g ^ i) (Kf a e (c, j))

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 : ℤ
⊢ (g ^ i) (Kf a e (1 c, j)) = (g ^ i) (Kf a e (c, j))
Tactic:
rfl
State after:
no goals