Theorem: OnCycleFactors.k_mul
Proof state before:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
σ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hσ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a (σ * τ) (c, i) = Kf a (σ * τ * 1) (c, i)

case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
σ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hσ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑((σ * τ) c)).card = (Equiv.Perm.support ↑c).card

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
σ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hσ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
simp only [mul_one]
Proof state after:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
σ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hσ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑((σ * τ) c)).card = (Equiv.Perm.support ↑c).card

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
σ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hσ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(σ c)).card = (Equiv.Perm.support ↑c).card