internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ k a τ (Kf a 1 (c, j + i)) = (g ^ j) (k a τ (Kf a 1 (c, i)))
Tactic:
rw [k_apply a c (j + i) hτ]
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
j : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a τ (c, j + i) = (g ^ j) (k a τ (Kf a 1 (c, i)))
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a τ (c, j + i) = (g ^ j) (k a τ (Kf a 1 (c, i)))
Tactic:
rw [k_apply a c i hτ]
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
j : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a τ (c, j + i) = (g ^ j) (Kf a τ (c, i))
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a τ (c, j + i) = (g ^ j) (Kf a τ (c, i))
Tactic:
rw [Kf_add']
Proof state after:
no goals
Theorem: OnCycleFactors.k_commute_zpow
Proof state before:
case neg
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ ((g ^ j) x) = (g ^ j) (k a τ x)
Tactic:
rw [k_apply_of_not_mem_support x hx]
Proof state after:
case neg
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ ((g ^ j) x) = (g ^ j) x
Theorem: OnCycleFactors.k_commute_zpow
Proof state before:
case neg
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ ((g ^ j) x) = (g ^ j) x
Tactic:
rw [k_apply_of_not_mem_support ((g ^ j : Equiv.Perm α) x) _]
Proof state after:
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ (g ^ j) x ∉ Equiv.Perm.support g
Theorem: OnCycleFactors.k_commute_zpow
Proof state before:
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ (g ^ j) x ∉ Equiv.Perm.support g
Tactic:
rw [Equiv.Perm.zpow_apply_mem_support]
Proof state after:
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support g
Theorem: OnCycleFactors.k_commute_zpow
Proof state before:
α : 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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support g
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.k_commute
Proof state before:
α : 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
⊢ k a τ ∘ ⇑g = ⇑g ∘ k a τ
Tactic:
simpa only [zpow_one] using k_commute_zpow hτ 1
Proof state after:
no goals
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ (Kf a σ (c, i)) = Kf a (τ * σ) (c, i)
Tactic:
simp only [Kf_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ ((g ^ i) (a (σ c))) = (g ^ i) (a ((τ * σ) c))
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ ((g ^ i) (a (σ c))) = (g ^ i) (a ((τ * σ) c))
Tactic:
rw [← Function.comp_apply (f := k a τ), k_commute_zpow hτ, Function.comp_apply]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ (g ^ i) (k a τ (a (σ c))) = (g ^ i) (a ((τ * σ) c))
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ (g ^ i) (k a τ (a (σ c))) = (g ^ i) (a ((τ * σ) c))
Tactic:
apply congr_arg
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ (a (σ c)) = a ((τ * σ) c)
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ (a (σ c)) = a ((τ * σ) c)
Tactic:
dsimp
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ (a (σ c)) = a (τ (σ c))
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
⊢ k a τ (a (σ c)) = a (τ (σ c))
Tactic:
have : ∀ (d) (τ : Equiv.Perm g.cycleFactorsFinset),
  a (τ d) = Kf a 1 (τ d, 0) :=
  fun d τ ↦ rfl
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
this :
  ∀ (d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    a (τ d) = Kf a 1 (τ d, 0)
⊢ k a τ (a (σ c)) = a (τ (σ c))
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
this :
  ∀ (d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    a (τ d) = Kf a 1 (τ d, 0)
⊢ k a τ (a (σ c)) = a (τ (σ c))
Tactic:
rw [this _ σ,
  k_apply a (σ c) 0 hτ, ← Function.comp_apply (f := τ), ← Equiv.Perm.coe_mul,
  this _ (τ * σ)]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
this :
  ∀ (d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    a (τ d) = Kf a 1 (τ d, 0)
⊢ Kf a τ (σ c, 0) = Kf a 1 ((τ * σ) c, 0)
Theorem: OnCycleFactors.k_apply_gen
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
σ τ : 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
this :
  ∀ (d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    a (τ d) = Kf a 1 (τ d, 0)
⊢ Kf a τ (σ c, 0) = Kf a 1 ((τ * σ) c, 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: OnCycleFactors.k_mul
Proof state before:
α : 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
⊢ k a σ ∘ k a τ = k a (σ * τ)
Tactic:
ext x
Proof state after:
case h
α : 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
x : α
⊢ (k a σ ∘ k a τ) x = k a (σ * τ) x
Theorem: OnCycleFactors.k_mul
Proof state before:
case h
α : 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
x : α
⊢ (k a σ ∘ k a τ) x = k a (σ * τ) x
Tactic:
simp only [Function.comp_apply]
Proof state after:
case h
α : 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
x : α
⊢ k a σ (k a τ x) = k a (σ * τ) x
Theorem: OnCycleFactors.k_mul
Proof state before:
case h
α : 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
x : α
⊢ k a σ (k a τ x) = k a (σ * τ) x
Tactic:
by_cases hx : x ∈ g.support
Proof state after:
case pos
α : 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
x : α
hx : x ∈ Equiv.Perm.support g
⊢ k a σ (k a τ x) = k a (σ * τ) x

case neg
α : 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
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a σ (k a τ x) = k a (σ * τ) x
Theorem: OnCycleFactors.k_mul
Proof state before:
case pos
α : 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
x : α
hx : x ∈ Equiv.Perm.support g
⊢ k a σ (k a τ x) = k a (σ * τ) x
Tactic:
simp only [mem_support_iff_exists_Kf a] at hx
Proof state after:
case pos
α : 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
x : α
hx : ∃ c i, x = Kf a 1 (c, i)
⊢ k a σ (k a τ x) = k a (σ * τ) x
Theorem: OnCycleFactors.k_mul
Proof state before:
case pos
α : 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
x : α
hx : ∃ c i, x = Kf a 1 (c, i)
⊢ k a σ (k a τ x) = k a (σ * τ) x
Tactic:
obtain ⟨c, i, rfl⟩ := hx
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 : ℤ
⊢ k a σ (k a τ (Kf a 1 (c, i))) = k a (σ * τ) (Kf a 1 (c, i))
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 : ℤ
⊢ k a σ (k a τ (Kf a 1 (c, i))) = k a (σ * τ) (Kf a 1 (c, i))
Tactic:
rw [k_apply a c i hτ, k_apply_gen _]
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 : ℤ
⊢ Kf a (σ * τ) (c, i) = k a (σ * τ) (Kf a 1 (c, i))

α : 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
Theorem: OnCycleFactors.k_mul
Proof state before:
α : 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:
exact hσ
Proof state after:
no goals
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 : ℤ
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑((σ * τ) c)).card = (Equiv.Perm.support ↑c).card
Tactic:
intro c
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
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 : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑((σ * τ) c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rw [Equiv.Perm.coe_mul, Function.comp_apply, hσ, hτ]
Proof state after:
no goals
Theorem: OnCycleFactors.k_mul
Proof state before:
case neg
α : 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
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a σ (k a τ x) = k a (σ * τ) x
Tactic:
simp only [k_apply_of_not_mem_support x hx]
Proof state after:
no goals