internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ x ∉ Equiv.Perm.support (↑c ^ m)
Tactic:
intro hx'
Proof state after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False
Tactic:
suffices ¬ x ∈ Equiv.Perm.support c by
  apply this
  apply Equiv.Perm.support_zpow_le _ _ hx'
Proof state after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∉ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro h
Proof state after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
h : x ∈ Equiv.Perm.support ↑c
⊢ False
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
h : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
exact hc (Equiv.Perm.cycle_is_cycleOf h c.prop).symm
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_injective
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply this
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.hθ_injective
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support ↑c
Tactic:
apply Equiv.Perm.support_zpow_le _ _ hx'
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g)) ↔
    z ∈ Set.range ⇑(θ g)
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g)) →
    z ∈ Set.range ⇑(θ g)

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ z ∈ Set.range ⇑(θ g) →
    ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g)) →
    z ∈ Set.range ⇑(θ g)
Tactic:
rw [hφ_mem_ker_iff, Equiv.Perm.IsCycle.forall_commute_iff, Set.mem_range]
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ (∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
      ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
        Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c) →
    ∃ y, (θ g) y = z
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ (∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
      ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
        Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c) →
    ∃ y, (θ g) y = z
Tactic:
intro Hz
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
⊢ ∃ y, (θ g) y = z
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
⊢ ∃ y, (θ g) y = z
Tactic:
let u := Equiv.Perm.subtypePerm z hu
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
⊢ ∃ y, (θ g) y = z
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
⊢ ∃ y, (θ g) y = z
Tactic:
let v : (c : g.cycleFactorsFinset) → (Subgroup.zpowers (c : Equiv.Perm α)) :=
  fun c => ⟨Equiv.Perm.ofSubtype
      (z.subtypePerm (Classical.choose (Hz c.val c.prop))),
        Classical.choose_spec (Hz c.val c.prop)⟩
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
⊢ ∃ y, (θ g) y = z
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
⊢ ∃ y, (θ g) y = z
Tactic:
use ⟨u, v⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
⊢ (θ g) (u, v) = z
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
⊢ (θ g) (u, v) = z
Tactic:
ext x
Proof state after:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
x : α
⊢ ((θ g) (u, v)) x = z x
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
x : α
⊢ ((θ g) (u, v)) x = z x
Tactic:
by_cases hx : g.cycleOf x = 1
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
x : α
hx : Equiv.Perm.cycleOf g x = 1
⊢ ((θ g) (u, v)) x = z x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
hu : ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
u : Equiv.Perm { x // x ∈ Function.fixedPoints ⇑g } := Equiv.Perm.subtypePerm z hu
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c) :=
  fun c => { val := Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z ⋯), property := ⋯ }
x : α
hx : ¬Equiv.Perm.cycleOf g x = 1
⊢ ((θ g) (u, v)) x = z x
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
⊢ ∀ (x : α), x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ Function.fixedPoints ⇑g ↔ z x ∈ Function.fixedPoints ⇑g
Tactic:
simp only [Function.fixedPoints, Equiv.Perm.smul_def, Function.IsFixedPt]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ {x | g x = x} ↔ z x ∈ {x | g x = x}
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ {x | g x = x} ↔ z x ∈ {x | g x = x}
Tactic:
simp only [← Equiv.Perm.not_mem_support]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ {x | x ∉ Equiv.Perm.support g} ↔ z x ∈ {x | x ∉ Equiv.Perm.support g}
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ {x | x ∉ Equiv.Perm.support g} ↔ z x ∈ {x | x ∉ Equiv.Perm.support g}
Tactic:
simp only [Set.mem_setOf_eq, not_iff_not]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ Equiv.Perm.support g ↔ z x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ Equiv.Perm.support g ↔ z x ∈ Equiv.Perm.support g
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ Equiv.Perm.support g → z x ∈ Equiv.Perm.support g

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ z x ∈ Equiv.Perm.support g → x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
⊢ x ∈ Equiv.Perm.support g → z x ∈ Equiv.Perm.support g
Tactic:
intro hx
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
⊢ z x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
⊢ z x ∈ Equiv.Perm.support g
Tactic:
let hx' := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx
⊢ z x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx
⊢ z x ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le hx'
Proof state after:
case mp.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx
⊢ z x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g x)
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mp.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx
⊢ z x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g x)
Tactic:
obtain ⟨Hz'⟩ := Hz (g.cycleOf x)
  (Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx)
Proof state after:
case mp.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
Hz :
  ∀ c ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
      Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
x : α
hx : x ∈ Equiv.Perm.support g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx
Hz' :
  ∀ (x_1 : α), x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g x) ↔ z x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g x)
h✝ : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z Hz') ∈ Subgroup.zpowers (Equiv.Perm.cycleOf g x)
⊢ z x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g x)