internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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)
Tactic:
rw [← Hz' x, Equiv.Perm.mem_support_cycleOf_iff]
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)
⊢ Equiv.Perm.SameCycle g x x ∧ x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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)
⊢ Equiv.Perm.SameCycle g x x ∧ x ∈ Equiv.Perm.support g
Tactic:
exact ⟨Equiv.Perm.SameCycle.refl _ _, hx⟩
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
Tactic:
intro hzx
Proof state after:
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 : α
hzx : z x ∈ Equiv.Perm.support g
⊢ x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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 : α
hzx : z x ∈ Equiv.Perm.support g
⊢ x ∈ Equiv.Perm.support g
Tactic:
let hzx' := Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
Proof state after:
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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
⊢ x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
⊢ x ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le hzx'
Proof state after:
case mpr.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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mpr.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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
Tactic:
obtain ⟨Hz'⟩ := Hz (g.cycleOf (z x)) hzx'
Proof state after:
case mpr.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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
Hz' :
  ∀ (x_1 : α),
    x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x)) ↔ z x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
h✝ : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z Hz') ∈ Subgroup.zpowers (Equiv.Perm.cycleOf g (z x))
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mpr.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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
Hz' :
  ∀ (x_1 : α),
    x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x)) ↔ z x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
h✝ : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z Hz') ∈ Subgroup.zpowers (Equiv.Perm.cycleOf g (z x))
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
Tactic:
rw [Hz' x, Equiv.Perm.mem_support_cycleOf_iff]
Proof state after:
case mpr.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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
Hz' :
  ∀ (x_1 : α),
    x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x)) ↔ z x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
h✝ : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z Hz') ∈ Subgroup.zpowers (Equiv.Perm.cycleOf g (z x))
⊢ Equiv.Perm.SameCycle g (z x) (z x) ∧ z x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
case mpr.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 : α
hzx : z x ∈ Equiv.Perm.support g
hzx' : Equiv.Perm.cycleOf g (z x) ∈ Equiv.Perm.cycleFactorsFinset g :=
  Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hzx
Hz' :
  ∀ (x_1 : α),
    x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x)) ↔ z x_1 ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g (z x))
h✝ : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z Hz') ∈ Subgroup.zpowers (Equiv.Perm.cycleOf g (z x))
⊢ Equiv.Perm.SameCycle g (z x) (z x) ∧ z x ∈ Equiv.Perm.support g
Tactic:
exact ⟨Equiv.Perm.SameCycle.refl _ _, hzx⟩
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
Tactic:
rw [hθ_1 _ x]
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
⊢ ↑((u, v).1 { val := x, property := ?pos✝ }) = z x

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
⊢ x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
⊢ ↑((u, v).1 { val := x, property := ?pos✝ }) = z x

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
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
simp only [u, v, Equiv.Perm.subtypePerm_apply]
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
⊢ x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
simp only [Equiv.Perm.cycleOf_eq_one_iff] at hx
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 : g x = x
⊢ x ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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 : g x = x
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, (Equiv.Perm.cycleOf_ne_one_iff_mem g).mp hx⟩ rfl]
Proof state after:
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
⊢ ↑((u, v).2 { val := Equiv.Perm.cycleOf g x, property := ⋯ }) x = z x
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
⊢ ↑((u, v).2 { val := Equiv.Perm.cycleOf g x, property := ⋯ }) x = z x
Tactic:
change (v _ : Equiv.Perm α) x = _
Proof state after:
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
⊢ ↑(v { val := Equiv.Perm.cycleOf g x, property := ⋯ }) x = z x
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
⊢ ↑(v { val := Equiv.Perm.cycleOf g x, property := ⋯ }) x = z x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
Proof state after:
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
⊢ ↑((Equiv.Perm.subtypePerm z ⋯) { val := x, property := ?neg.ha✝ }) = z x

case neg.ha
α : 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
⊢ x ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
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
⊢ ↑((Equiv.Perm.subtypePerm z ⋯) { val := x, property := ?neg.ha✝ }) = z x

case neg.ha
α : 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
⊢ x ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }
Tactic:
rfl
Proof state after:
case neg.ha
α : 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
⊢ x ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }