internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (MulAut.conj (ConjAct.ofConjAct (ConjAct.toConjAct z))) g = g
Tactic:
rw [MulAut.conj_apply]
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g * (ConjAct.ofConjAct (ConjAct.toConjAct z))⁻¹ = g
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g * (ConjAct.ofConjAct (ConjAct.toConjAct z))⁻¹ = g
Tactic:
rw [mul_inv_eq_iff_eq_mul]
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g = g * ConjAct.ofConjAct (ConjAct.toConjAct z)
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g = g * ConjAct.ofConjAct (ConjAct.toConjAct z)
Tactic:
rw [ConjAct.ofConjAct_toConjAct]
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ z * g = g * z
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ z * g = g * z
Tactic:
exact Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute z g H
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case h.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (φ g) { val := ConjAct.toConjAct z, property := ⋯ } = 1
Tactic:
ext ⟨c, hc⟩
Proof state after:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ ↑(((φ g) { val := ConjAct.toConjAct z, property := ⋯ }) { val := c, property := hc }) x✝ =
    ↑(1 { val := c, property := hc }) x✝
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ ↑(((φ g) { val := ConjAct.toConjAct z, property := ⋯ }) { val := c, property := hc }) x✝ =
    ↑(1 { val := c, property := hc }) x✝
Tactic:
rw [φ_eq']
Proof state after:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (z * c * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (z * c * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝
Tactic:
rw [H c hc]
Proof state after:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (c * z * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (c * z * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝
Tactic:
simp only [mul_inv_cancel_right, Equiv.Perm.coe_one, id.def, Subtype.coe_mk]
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof state before:
case h.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := ConjAct.toConjAct z, property := ⋯ } =
    ConjAct.toConjAct z
Tactic:
simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
Proof state after:
no goals
Theorem: Finset.noncommProd_eq_one
Proof state before:
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hf : ∀ a ∈ s, f a = 1
⊢ Finset.noncommProd s f comm = 1
Tactic:
induction s using Finset.induction_on with
| empty => simp only [Finset.noncommProd_empty]
| insert ha hs =>
    rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha]
    rw [hf _ (Finset.mem_insert_self _ _), one_mul]
    apply hs
    intro a ha
    exact hf _ (Finset.mem_insert_of_mem ha)
Proof state after:
no goals
Theorem: Finset.noncommProd_eq_one
Proof state before:
case empty
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
comm : Set.Pairwise ↑∅ fun a b => Commute (f a) (f b)
hf : ∀ a ∈ ∅, f a = 1
⊢ Finset.noncommProd ∅ f comm = 1
Tactic:
simp only [Finset.noncommProd_empty]
Proof state after:
no goals
Theorem: Finset.noncommProd_eq_one
Proof state before:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ Finset.noncommProd (insert a✝ s✝) f comm = 1
Tactic:
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha]
Proof state after:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ f a✝ * Finset.noncommProd s✝ f ⋯ = 1
Theorem: Finset.noncommProd_eq_one
Proof state before:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ f a✝ * Finset.noncommProd s✝ f ⋯ = 1
Tactic:
rw [hf _ (Finset.mem_insert_self _ _), one_mul]
Proof state after:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ Finset.noncommProd s✝ f ⋯ = 1
Theorem: Finset.noncommProd_eq_one
Proof state before:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ Finset.noncommProd s✝ f ⋯ = 1
Tactic:
apply hs
Proof state after:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ ∀ a ∈ s✝, f a = 1
Theorem: Finset.noncommProd_eq_one
Proof state before:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ ∀ a ∈ s✝, f a = 1
Tactic:
intro a ha
Proof state after:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha✝ : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
a : α
ha : a ∈ s✝
⊢ f a = 1
Theorem: Finset.noncommProd_eq_one
Proof state before:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha✝ : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
a : α
ha : a ∈ s✝
⊢ f a = 1
Tactic:
exact hf _ (Finset.mem_insert_of_mem ha)
Proof state after:
no goals
Theorem: Equiv.Perm.cycleOf_ne_one_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x : α
⊢ Equiv.Perm.cycleOf g x ≠ 1 ↔ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.mem_support,
      ne_eq, Equiv.Perm.cycleOf_eq_one_iff]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_apply_of_not_mem_cycleFactorsFinset
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k v x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [θAux, dif_neg hx]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_apply_of_mem_fixedPoints
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g k v x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [θAux, dif_neg]
Proof state after:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
Theorem: OnCycleFactors.θAux_apply_of_mem_fixedPoints
Proof state before:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support]
Proof state after:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g x = x
Theorem: OnCycleFactors.θAux_apply_of_mem_fixedPoints
Proof state before:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g x = x
Tactic:
exact hx
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_apply_of_mem_fixedPoints_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g k v x ∈ Function.fixedPoints ⇑g
Tactic:
rw [θAux_apply_of_mem_fixedPoints hx, Equiv.Perm.ofSubtype_apply_of_mem k hx]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(k { val := x, property := hx }) ∈ Function.fixedPoints ⇑g
Theorem: OnCycleFactors.θAux_apply_of_mem_fixedPoints_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(k { val := x, property := hx }) ∈ Function.fixedPoints ⇑g
Tactic:
exact (k _).prop
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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 k v x = ↑(v c) x
Tactic:
suffices c = ⟨g.cycleOf x, ?_⟩ by
  rw [this, θAux, dif_pos]
  rw [hx]; exact c.prop
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ c = { val := Equiv.Perm.cycleOf g x, property := ⋯ }
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ c = { val := Equiv.Perm.cycleOf g x, property := ⋯ }
Tactic:
simp only [← Subtype.coe_inj, hx]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
this : c = { val := Equiv.Perm.cycleOf g x, property := ?m.315200 }
⊢ θAux g k v x = ↑(v c) x
Tactic:
rw [this, θAux, dif_pos]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [hx]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ ↑c ∈ Equiv.Perm.cycleFactorsFinset g
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ ↑c ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact c.prop
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = ↑c
Tactic:
rw [θAux_apply_of_cycleOf_eq c hx]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq_mem
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Tactic:
obtain ⟨m, hm⟩ := (v c).prop
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq_mem
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Tactic:
dsimp only at hm
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq_mem
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Tactic:
rw [← hm, ← hx]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g ((Equiv.Perm.cycleOf g x ^ m) x) = Equiv.Perm.cycleOf g x
Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq_mem
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (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
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g ((Equiv.Perm.cycleOf g x ^ m) x) = Equiv.Perm.cycleOf g x
Tactic:
simp only [Equiv.Perm.cycleOf_zpow_apply_self, Equiv.Perm.cycleOf_self_apply_zpow]
Proof state after:
no goals
Theorem: OnCycleFactors.θAux_cycleOf_apply_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x