internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
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
⊢ ¬g x = x
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
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 : ¬g x = x
⊢ ¬g x = x
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
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 α
⊢ 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⟩
Proof 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))
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof 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)
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof 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)
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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 θ
Proof 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)
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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)
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof 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)
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
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'
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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 })
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
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 α
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]
Proof 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
Theorem: OnCycleFactors.hφ_ker_eq_θ_range
Proof 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
Proof 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