internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hθ_2
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x = ↑(uv.2 c) x
Tactic:
unfold θFun
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ ({
          toOneHom :=
            {
              toFun := fun kv =>
                { toFun := θAux g kv.1 kv.2, invFun := θAux g kv.1⁻¹ kv.2⁻¹, left_inv := ⋯, right_inv := ⋯ },
              map_one' := ⋯ },
          map_mul' := ⋯ }
        uv)
      x =
    ↑(uv.2 c) x
Theorem: OnCycleFactors.hθ_2
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ ({
          toOneHom :=
            {
              toFun := fun kv =>
                { toFun := θAux g kv.1 kv.2, invFun := θAux g kv.1⁻¹ kv.2⁻¹, left_inv := ⋯, right_inv := ⋯ },
              map_one' := ⋯ },
          map_mul' := ⋯ }
        uv)
      x =
    ↑(uv.2 c) x
Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, Equiv.coe_fn_mk]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ θAux g uv.1 uv.2 x = ↑(uv.2 c) x
Theorem: OnCycleFactors.hθ_2
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ θAux g uv.1 uv.2 x = ↑(uv.2 c) x
Tactic:
exact θAux_apply_of_cycleOf_eq c hx
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ }) = ↑c
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Tactic:
by_cases hx : x ∈ Function.fixedPoints g
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [← Equiv.Perm.cycleOf_ne_one_iff_mem, ne_eq, Equiv.Perm.cycleOf_eq_one_iff]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ¬g x = x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ¬g x = x
Tactic:
simpa [Function.mem_fixedPoints_iff] using hx
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Tactic:
simp only [hθ_1 _ x hx, Equiv.Perm.coe_one, id_eq]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x = ↑c x
Tactic:
apply symm
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑c x = x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑c x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∉ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
simp only [Function.mem_fixedPoints, Function.IsFixedPt, ← Equiv.Perm.not_mem_support] at hx
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro hx'
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ False
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply hx
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop hx'
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, hx'⟩ rfl]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c { val := ↑c, property := ⋯ }).2 { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c { val := ↑c, property := ⋯ }).2 { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
dsimp only
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
by_cases hc : c = ⟨Equiv.Perm.cycleOf g x, hx'⟩
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
rw [hc, Pi.mulSingle_eq_same, Equiv.Perm.cycleOf_apply_self]
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
rw [Pi.mulSingle_eq_of_ne' hc]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑1 x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑1 x = ↑c x
Tactic:
simp only [OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x = ↑c x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x = ↑c x
Tactic:
apply symm
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑c x = x
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑c x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x ∉ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro hxc
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ False
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply hc
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx' }
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx' }
Tactic:
rw [← Subtype.coe_inj]
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ ↑c = ↑{ val := Equiv.Perm.cycleOf g x, property := hx' }
Theorem: OnCycleFactors.hθ_single
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ ↑c = ↑{ val := Equiv.Perm.cycleOf g x, property := hx' }
Tactic:
exact Equiv.Perm.cycle_is_cycleOf hxc c.prop
Proof state after:
no goals
Theorem: OnCycleFactors.hθ_injective
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Function.Injective ⇑(θ g)
Tactic:
rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ MonoidHom.ker (θ g) ≤ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ MonoidHom.ker (θ g) ≤ ⊥
Tactic:
rintro ⟨u, v⟩
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker (θ g) → (u, v) ∈ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker (θ g) → (u, v) ∈ ⊥
Tactic:
unfold θ
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker { toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } →
    (u, v) ∈ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker { toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } →
    (u, v) ∈ ⊥
Tactic:
unfold θFun
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈
      MonoidHom.ker
        {
          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) ∈ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈
      MonoidHom.ker
        {
          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) ∈ ⊥
Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, MonoidHom.mem_ker, Equiv.Perm.ext_iff]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), { toFun := θAux g u v, invFun := θAux g u⁻¹ v⁻¹, left_inv := ⋯, right_inv := ⋯ } x = 1 x) → (u, v) ∈ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), { toFun := θAux g u v, invFun := θAux g u⁻¹ v⁻¹, left_inv := ⋯, right_inv := ⋯ } x = 1 x) → (u, v) ∈ ⊥
Tactic:
simp only [Equiv.coe_fn_mk, Equiv.Perm.coe_one, id_eq]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), θAux g u v x = x) → (u, v) ∈ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), θAux g u v x = x) → (u, v) ∈ ⊥
Tactic:
intro huv
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ (u, v) ∈ ⊥
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ (u, v) ∈ ⊥
Tactic:
simp only [Subgroup.mem_bot, Prod.mk_eq_one, MonoidHom.mem_ker]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1 ∧ v = 1
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1 ∧ v = 1
Tactic:
constructor
Proof state after:
case mk.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1

case mk.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ v = 1
Theorem: OnCycleFactors.hθ_injective
Proof state before:
case mk.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1
Tactic:
ext ⟨x, hx⟩
Proof state after:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = ↑(1 { val := x, property := hx })