internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
rw [θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ rfl]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Tactic:
obtain ⟨m, hm⟩ := (v _).prop
Proof state after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : (fun x => ↑?m.317682 ^ x) m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : (fun x => ↑?m.317682 ^ x) m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Tactic:
dsimp only at hm
Proof state after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑?m.317682 ^ m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑?m.317682 ^ m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Tactic:
rw [← hm]
Proof state after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m = ↑(v { val := Equiv.Perm.cycleOf g x, property := hx })
⊢ Equiv.Perm.cycleOf g ((↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m) x) = Equiv.Perm.cycleOf g x
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m = ↑(v { val := Equiv.Perm.cycleOf g x, property := hx })
⊢ Equiv.Perm.cycleOf g ((↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m) x) = Equiv.Perm.cycleOf g x
Tactic:
simp only [Equiv.Perm.cycleOf_zpow_apply_self, Equiv.Perm.cycleOf_self_apply_zpow]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
rw [g.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support] at hx
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
rw [g.cycleOf_eq_one_iff.mpr hx, g.cycleOf_eq_one_iff,
  ← Function.mem_fixedPoints_iff]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ θAux g k v x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ θAux g k v x ∈ Function.fixedPoints ⇑g
Tactic:
apply θAux_apply_of_mem_fixedPoints_mem
Proof state after:
case neg.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
case neg.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_one
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
⊢ θAux g 1 1 x = x
Tactic:
unfold θAux
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
⊢ (if hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g then
      ↑(1 { val := Equiv.Perm.cycleOf g x, property := hx }) x
    else (Equiv.Perm.ofSubtype 1) x) =
    x
Theorem: OnCycleFactors.θAux_one
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
⊢ (if hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g then
      ↑(1 { val := Equiv.Perm.cycleOf g x, property := hx }) x
    else (Equiv.Perm.ofSubtype 1) x) =
    x
Tactic:
split_ifs
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(1 { val := Equiv.Perm.cycleOf g x, property := h✝ }) x = x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype 1) x = x
Theorem: OnCycleFactors.θAux_one
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(1 { val := Equiv.Perm.cycleOf g x, property := h✝ }) x = x
Tactic:
simp only [Pi.one_apply, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_one
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype 1) x = x
Tactic:
simp only [map_one, Equiv.Perm.coe_one, id_eq]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_mul
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Theorem: OnCycleFactors.θAux_mul
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
rw [θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ (θAux_apply_of_cycleOf_eq_mem ⟨_, hx⟩ rfl),
  θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ rfl,
  θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ rfl]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(v' { val := Equiv.Perm.cycleOf g x, property := hx }) (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) =
    ↑((v' * v) { val := Equiv.Perm.cycleOf g x, property := hx }) x
Theorem: OnCycleFactors.θAux_mul
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(v' { val := Equiv.Perm.cycleOf g x, property := hx }) (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) =
    ↑((v' * v) { val := Equiv.Perm.cycleOf g x, property := hx }) x
Tactic:
simp only [ne_eq, Pi.mul_apply, Submonoid.coe_mul,
  Subgroup.coe_toSubmonoid, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_mul
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
have hx' : g.cycleOf (θAux g k v x) ∉ g.cycleFactorsFinset := by
  rw [θAux_cycleOf_apply_eq]
  exact hx
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Theorem: OnCycleFactors.θAux_mul
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
nth_rewrite 1 [θAux, dif_neg hx']
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') (θAux g k v x) = θAux g (k' * k) (v' * v) x
Theorem: OnCycleFactors.θAux_mul
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
simp only [θAux, dif_neg hx]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') ((Equiv.Perm.ofSubtype k) x) = (Equiv.Perm.ofSubtype (k' * k)) x
Theorem: OnCycleFactors.θAux_mul
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') ((Equiv.Perm.ofSubtype k) x) = (Equiv.Perm.ofSubtype (k' * k)) x
Tactic:
simp only [map_mul, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_mul
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [θAux_cycleOf_apply_eq]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
Theorem: OnCycleFactors.θAux_mul
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k' : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v' : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_inv
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Function.LeftInverse (θAux g k⁻¹ v⁻¹) (θAux g k v)
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ θAux g k⁻¹ v⁻¹ (θAux g k v x) = x
Theorem: OnCycleFactors.θAux_inv
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ θAux g k⁻¹ v⁻¹ (θAux g k v x) = x
Tactic:
rw [θAux_mul]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ θAux g (k⁻¹ * k) (v⁻¹ * v) x = x
Theorem: OnCycleFactors.θAux_inv
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ θAux g (k⁻¹ * k) (v⁻¹ * v) x = x
Tactic:
simp only [mul_left_inv, θAux_one]
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_1
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ((θ g) uv) x = ↑(uv.1 { val := x, property := hx })
Tactic:
unfold θ
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x =
    ↑(uv.1 { val := x, property := hx })
Theorem: OnCycleFactors.hθ_1
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x =
    ↑(uv.1 { val := x, property := hx })
Tactic:
unfold θFun
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({
          toOneHom :=
            {
              toFun := fun kv =>
                { toFun := θAux g kv.1 kv.2, invFun := θAux g kv.1⁻¹ kv.2⁻¹, left_inv := ⋯, right_inv := ⋯ },
              map_one' := ⋯ },
          map_mul' := ⋯ }
        uv)
      x =
    ↑(uv.1 { val := x, property := hx })
Theorem: OnCycleFactors.hθ_1
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({
          toOneHom :=
            {
              toFun := fun kv =>
                { toFun := θAux g kv.1 kv.2, invFun := θAux g kv.1⁻¹ kv.2⁻¹, left_inv := ⋯, right_inv := ⋯ },
              map_one' := ⋯ },
          map_mul' := ⋯ }
        uv)
      x =
    ↑(uv.1 { val := x, property := hx })
Tactic:
simp only [Equiv.coe_fn_mk, MonoidHom.coe_mk, OneHom.coe_mk, Equiv.coe_fn_mk]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g uv.1 uv.2 x = ↑(uv.1 { val := x, property := hx })
Theorem: OnCycleFactors.hθ_1
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g uv.1 uv.2 x = ↑(uv.1 { val := x, property := hx })
Tactic:
rw [θAux_apply_of_mem_fixedPoints, Equiv.Perm.ofSubtype_apply_of_mem]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.hθ_1
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_2
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ ((θ g) uv) x = ↑(uv.2 c) x
Tactic:
unfold θ
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x = ↑(uv.2 c) x