Theorem: OnCycleFactors.hφ_ker_eq_θ_range (Jordan/ConjClassCount.lean)

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
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))

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]
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

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
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

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
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

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)⟩
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

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⟩
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

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
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

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
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

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
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

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]
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}

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]
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}

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]
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

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
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

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
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

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
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

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'
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)

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)
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)

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]
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

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⟩
State after:
no goals

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
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

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
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

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'
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))

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'
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))

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]
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

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⟩
State after:
no goals

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]
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

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]
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

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
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

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
State after:
no goals

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]
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

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 = _
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

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]
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 := ⋯ }

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
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 := ⋯ }

State before:
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:
simp only [Equiv.Perm.mem_support, Equiv.Perm.cycleOf_apply_self, ne_eq]
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
⊢ ¬g x = x

State before:
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
⊢ ¬g x = x
Tactic:
simp only [Equiv.Perm.cycleOf_eq_one_iff] at hx
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 : ¬g x = x
⊢ ¬g x = x

State before:
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 : ¬g x = x
⊢ ¬g x = x
Tactic:
exact hx
State after:
no goals

State before:
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))
Tactic:
rintro ⟨⟨u, v⟩, h⟩
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
⊢ ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
⊢ ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
Tactic:
rw [hφ_mem_ker_iff]
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
rw [Equiv.Perm.IsCycle.forall_commute_iff]
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
⊢ ∀ 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

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
⊢ ∀ 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
Tactic:
intro c hc
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : 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

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
Tactic:
intro x
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
Tactic:
simp only [← Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff g c hc]
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔ c = Equiv.Perm.cycleOf g (z x)

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔ c = Equiv.Perm.cycleOf g (z x)
Tactic:
rw [← h]
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔ c = Equiv.Perm.cycleOf g (((θ g) (u, v)) x)

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔ c = Equiv.Perm.cycleOf g (((θ g) (u, v)) x)
Tactic:
unfold θ
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔
    c =
      Equiv.Perm.cycleOf g
        (({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } (u, v)) x)

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔
    c =
      Equiv.Perm.cycleOf g
        (({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } (u, v)) x)
Tactic:
unfold θFun
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔
    c =
      Equiv.Perm.cycleOf 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' := ⋯ }
            (u, v))
          x)

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔
    c =
      Equiv.Perm.cycleOf 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' := ⋯ }
            (u, v))
          x)
Tactic:
dsimp only [MonoidHom.coe_mk, OneHom.coe_mk, Equiv.coe_fn_mk]
State after:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔ c = Equiv.Perm.cycleOf g (θAux g u v x)

State before:
case mpr.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
x : α
⊢ c = Equiv.Perm.cycleOf g x ↔ c = Equiv.Perm.cycleOf g (θAux g u v x)
Tactic:
rw [θAux_cycleOf_apply_eq]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ?m.373134
⊢ ∃ (hc : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c),
    Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
use hc'
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : 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

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : 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
Tactic:
suffices Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc') = v ⟨c, hc⟩ by
  rw [this]
  exact (v _).prop
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : 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') = ↑(v { val := c, property := hc })

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : 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') = ↑(v { val := c, property := hc })
Tactic:
ext x
State after:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x

State before:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x
Tactic:
by_cases hx : x ∈ c.support
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
this : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc') = ↑(v { val := c, property := hc })
⊢ Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc') ∈ Subgroup.zpowers c
Tactic:
rw [this]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
this : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc') = ↑(v { val := c, property := hc })
⊢ ↑(v { val := c, property := hc }) ∈ Subgroup.zpowers c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
this : Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc') = ↑(v { val := c, property := hc })
⊢ ↑(v { val := c, property := hc }) ∈ Subgroup.zpowers c
Tactic:
exact (v _).prop
State after:
no goals

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem, Equiv.Perm.subtypePerm_apply]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ ↑{ val := z ↑{ val := x, property := ?pos.ha✝ }, property := ⋯ } = ↑(v { val := c, property := hc }) x

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ ↑{ val := z ↑{ val := x, property := ?pos.ha✝ }, property := ⋯ } = ↑(v { val := c, property := hc }) x

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
dsimp
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ z x = ↑(v { val := c, property := hc }) x

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ z x = ↑(v { val := c, property := hc }) x

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
rw [← h, hθ_2 _ x ⟨c, hc⟩]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ Equiv.Perm.cycleOf g x = ↑{ val := c, property := hc }

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ Equiv.Perm.cycleOf g x = ↑{ val := c, property := hc }

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
exact (Equiv.Perm.cycle_is_cycleOf hx hc).symm
State after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

State before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∈ Equiv.Perm.support c
⊢ x ∈ Equiv.Perm.support c
Tactic:
exact hx
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ (Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm z hc')) x = ↑(v { val := c, property := hc }) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
obtain ⟨m, hm⟩ := (v ⟨c, hc⟩).prop
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : (fun x => ↑{ val := c, property := hc } ^ x) m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : (fun x => ↑{ val := c, property := hc } ^ x) m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
dsimp only at hm
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = ↑(v { val := c, property := hc }) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
rw [← hm]
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = (c ^ m) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x = (c ^ m) x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
apply symm
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ (c ^ m) x = x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ (c ^ m) x = x

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x ∉ Equiv.Perm.support (c ^ m)

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
⊢ x ∉ Equiv.Perm.support (c ^ m)

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
intro hx'
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ False

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ False

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
apply hx
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ x ∈ Equiv.Perm.support c

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
m : ℤ
hm : c ^ m = ↑(v { val := c, property := hc })
hx' : x ∈ Equiv.Perm.support (c ^ m)
⊢ x ∈ Equiv.Perm.support c

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
exact (Equiv.Perm.support_zpow_le c m) hx'
State after:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c

State before:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
h : (θ g) (u, v) = z
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ Equiv.Perm.support c ↔ z x ∈ Equiv.Perm.support c
x : α
hx : x ∉ Equiv.Perm.support c
⊢ x ∉ Equiv.Perm.support c
Tactic:
exact hx
State after:
no goals