internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Tactic:
rw [← Equiv.Perm.mem_support, ← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e d)) (a.mem_support _) (e d).prop]
Proof state after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ ↑(e d) ∈ Equiv.Perm.cycleFactorsFinset g
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ ↑(e d) ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact (e d).prop
Proof state after:
no goals
Theorem: OnCycleFactors.k_apply
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 1 (c, i)) = Kf a τ (c, i)
Tactic:
simp only [k]
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
⊢ Function.extend (Kf a 1) (Kf a τ) id (Kf a 1 (c, i)) = Kf a τ (c, i)
Theorem: OnCycleFactors.k_apply
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
⊢ Function.extend (Kf a 1) (Kf a τ) id (Kf a 1 (c, i)) = Kf a τ (c, i)
Tactic:
rw [Function.FactorsThrough.extend_apply (Equiv.Perm.Basis.Kf_factorsThrough a _) id ⟨c, i⟩]
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
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(1 c)).card = (Equiv.Perm.support ↑(τ c)).card
Theorem: OnCycleFactors.k_apply
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
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(1 c)).card = (Equiv.Perm.support ↑(τ c)).card
Tactic:
intro c
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
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑(1 c)).card = (Equiv.Perm.support ↑(τ c)).card
Theorem: OnCycleFactors.k_apply
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
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑(1 c)).card = (Equiv.Perm.support ↑(τ c)).card
Tactic:
simp only [← hτ c, Equiv.Perm.coe_one, id.def]
Proof state after:
no goals
Theorem: OnCycleFactors.k_apply_of_not_mem_support
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 }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ x = x
Tactic:
simp only [k]
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 }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ Function.extend (Kf a 1) (Kf a τ) id x = x
Theorem: OnCycleFactors.k_apply_of_not_mem_support
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 }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ Function.extend (Kf a 1) (Kf a τ) id x = x
Tactic:
rw [Function.extend_apply']
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 }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ id x = x

case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x
Theorem: OnCycleFactors.k_apply_of_not_mem_support
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 }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ id x = x

case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x
Tactic:
simp only [id.def]
Proof state after:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x
Theorem: OnCycleFactors.k_apply_of_not_mem_support
Proof state before:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x
Tactic:
intro hyp
Proof state after:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hyp : ∃ a_1, Kf a 1 a_1 = x
⊢ False
Theorem: OnCycleFactors.k_apply_of_not_mem_support
Proof state before:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hyp : ∃ a_1, Kf a 1 a_1 = x
⊢ False
Tactic:
obtain ⟨⟨c, i⟩, rfl⟩ := hyp
Proof state after:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ False
Theorem: OnCycleFactors.k_apply_of_not_mem_support
Proof state before:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ False
Tactic:
apply hx
Proof state after:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.k_apply_of_not_mem_support
Proof state before:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g
Tactic:
rw [Kf_def, Equiv.Perm.zpow_apply_mem_support]
Proof state after:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ a (1 c) ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.k_apply_of_not_mem_support
Proof state before:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ a (1 c) ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.Basis.mem_support'
Proof state after:
no goals
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ x ∈ Equiv.Perm.support g ↔ ∃ c i, x = Kf a 1 (c, i)
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ x ∈ Equiv.Perm.support g → ∃ c i, x = Kf a 1 (c, i)

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ (∃ c i, x = Kf a 1 (c, i)) → x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ x ∈ Equiv.Perm.support g → ∃ c i, x = Kf a 1 (c, i)
Tactic:
intro hx
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∃ c i, x = Kf a 1 (c, i)
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∃ c i, x = Kf a 1 (c, i)
Tactic:
rw [← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff] at hx
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ c i, x = Kf a 1 (c, i)
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ c i, x = Kf a 1 (c, i)
Tactic:
use ⟨g.cycleOf x, hx⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = Kf a 1 ({ val := Equiv.Perm.cycleOf g x, property := hx }, i)
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = Kf a 1 ({ val := Equiv.Perm.cycleOf g x, property := hx }, i)
Tactic:
simp only [Kf_def, Equiv.Perm.coe_one, id.def]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
let ha := a.mem_support ⟨g.cycleOf x, hx⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha : Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx } ∈
  Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := hx } :=
  Equiv.Perm.Basis.mem_support { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha : Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx } ∈
  Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := hx } :=
  Equiv.Perm.Basis.mem_support { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
simp only [Subtype.coe_mk, Equiv.Perm.mem_support_cycleOf_iff] at ha
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
obtain ⟨i, hi⟩ := ha.1.symm
Proof state after:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
i : ℤ
hi : (g ^ i) (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) = x
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
i : ℤ
hi : (g ^ i) (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) = x
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
exact ⟨i, hi.symm⟩
Proof state after:
no goals
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ (∃ c i, x = Kf a 1 (c, i)) → x ∈ Equiv.Perm.support g
Tactic:
rintro ⟨c, i, rfl⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g
Tactic:
simp only [Kf_def, Equiv.Perm.zpow_apply_mem_support, Equiv.Perm.coe_one, id.def]
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop
Proof state after:
case mpr.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.mem_support_iff_exists_Kf
Proof state before:
case mpr.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support ↑c
Tactic:
apply a.mem_support
Proof state after:
no goals
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 : ℤ
⊢ k a τ ∘ ⇑(g ^ j) = ⇑(g ^ j) ∘ 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
j : ℤ
x : α
⊢ (k a τ ∘ ⇑(g ^ j)) x = (⇑(g ^ j) ∘ k a τ) x
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
x : α
⊢ (k a τ ∘ ⇑(g ^ j)) x = (⇑(g ^ j) ∘ 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
j : ℤ
x : α
⊢ k a τ ((g ^ j) x) = (g ^ j) (k a τ x)
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
x : α
⊢ k a τ ((g ^ j) x) = (g ^ j) (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
j : ℤ
x : α
hx : x ∈ Equiv.Perm.support g
⊢ k a τ ((g ^ j) x) = (g ^ j) (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
j : ℤ
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ ((g ^ j) x) = (g ^ j) (k a τ x)
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
x : α
hx : x ∈ Equiv.Perm.support g
⊢ k a τ ((g ^ j) x) = (g ^ j) (k a τ x)
Tactic:
rw [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
j : ℤ
x : α
hx : ∃ c i, x = Kf a 1 (c, i)
⊢ k a τ ((g ^ j) x) = (g ^ j) (k a τ x)
Theorem: OnCycleFactors.k_commute_zpow
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
j : ℤ
x : α
hx : ∃ c i, x = Kf a 1 (c, i)
⊢ k a τ ((g ^ j) x) = (g ^ j) (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
j : ℤ
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ k a τ ((g ^ j) (Kf a 1 (c, 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 : ℤ
⊢ k a τ ((g ^ j) (Kf a 1 (c, i))) = (g ^ j) (k a τ (Kf a 1 (c, i)))
Tactic:
rw [← Kf_add']
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 : ℤ
⊢ k a τ (Kf a 1 (c, j + i)) = (g ^ j) (k a τ (Kf a 1 (c, i)))