internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ d = 1 d
Tactic:
simp only [Equiv.Perm.coe_one, id.def]
Proof state after:
no goals
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))
Tactic:
rw [Equiv.Perm.Basis.Kf_apply'' a,
  k_apply a _ _ hτ, Equiv.Perm.Basis.Kf_apply'' a]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ τ c ≠ τ d

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ τ c ≠ τ d

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d
Tactic:
exact (Equiv.injective τ).ne_iff.mpr hcd
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d
Tactic:
exact hcd
Proof state after:
no goals
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
suffices ∀ (c : g.cycleFactorsFinset), (c : Equiv.Perm α) x = x by
  simp only [this, k_apply_of_not_mem_support x hx]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ↑c x = x
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ↑c x = x
Tactic:
intro c
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ↑c x = x
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ↑c x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ x ∉ Equiv.Perm.support ↑c
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
apply Finset.not_mem_mono _ hx
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ Equiv.Perm.support ↑c ⊆ Equiv.Perm.support g
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ Equiv.Perm.support ↑c ⊆ Equiv.Perm.support g
Tactic:
exact Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop
Proof state after:
no goals
Theorem: OnCycleFactors.k_cycle_apply
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
this : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ↑c x = x
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
simp only [this, k_apply_of_not_mem_support x hx]
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_eq_card_of_mem_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hτ : τ ∈ MonoidHom.range (φ g)
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
obtain ⟨⟨k, hk⟩, rfl⟩ := hτ
Proof state after:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Equiv.Perm.support ↑(((φ g) { val := k, property := hk }) c)).card = (Equiv.Perm.support ↑c).card
Theorem: OnCycleFactors.hφ_eq_card_of_mem_range
Proof state before:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Equiv.Perm.support ↑(((φ g) { val := k, property := hk }) c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rw [φ_eq, ConjAct.smul_def, Equiv.Perm.support_conj]
Proof state after:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Finset.map (Equiv.toEmbedding (ConjAct.ofConjAct k)) (Equiv.Perm.support ↑c)).card = (Equiv.Perm.support ↑c).card
Theorem: OnCycleFactors.hφ_eq_card_of_mem_range
Proof state before:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Finset.map (Equiv.toEmbedding (ConjAct.ofConjAct k)) (Equiv.Perm.support ↑c)).card = (Equiv.Perm.support ↑c).card
Tactic:
apply Finset.card_map
Proof state after:
no goals
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ ConjAct.toConjAct (φ'Fun a hτ) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
rw [MulAction.mem_stabilizer_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ ConjAct.toConjAct (φ'Fun a hτ) • g = g
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ ConjAct.toConjAct (φ'Fun a hτ) • g = g
Tactic:
rw [ConjAct.smul_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ ConjAct.ofConjAct (ConjAct.toConjAct (φ'Fun a hτ)) * g * (ConjAct.ofConjAct (ConjAct.toConjAct (φ'Fun a hτ)))⁻¹ = g
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ ConjAct.ofConjAct (ConjAct.toConjAct (φ'Fun a hτ)) * g * (ConjAct.ofConjAct (ConjAct.toConjAct (φ'Fun a hτ)))⁻¹ = g
Tactic:
rw [ConjAct.ofConjAct_toConjAct]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ φ'Fun a hτ * g * (φ'Fun a hτ)⁻¹ = g
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ φ'Fun a hτ * g * (φ'Fun a hτ)⁻¹ = g
Tactic:
rw [mul_inv_eq_iff_eq_mul]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ φ'Fun a hτ * g = g * φ'Fun a hτ
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
⊢ φ'Fun a hτ * g = g * φ'Fun a hτ
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (φ'Fun a hτ * g) x = (g * φ'Fun a hτ) x
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (φ'Fun a hτ * g) x = (g * φ'Fun a hτ) x
Tactic:
simp only [Equiv.Perm.coe_mul]
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (⇑(φ'Fun a hτ) ∘ ⇑g) x = (⇑g ∘ ⇑(φ'Fun a hτ)) x
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (⇑(φ'Fun a hτ) ∘ ⇑g) x = (⇑g ∘ ⇑(φ'Fun a hτ)) x
Tactic:
simp only [φ'Fun]
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (⇑(Equiv.ofBijective (k a τ) ⋯) ∘ ⇑g) x = (⇑g ∘ ⇑(Equiv.ofBijective (k a τ) ⋯)) x
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (⇑(Equiv.ofBijective (k a τ) ⋯) ∘ ⇑g) x = (⇑g ∘ ⇑(Equiv.ofBijective (k a τ) ⋯)) x
Tactic:
simp only [Function.comp_apply, Equiv.ofBijective_apply]
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ k a τ (g x) = g (k a τ x)
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ k a τ (g x) = g (k a τ x)
Tactic:
rw [← Function.comp_apply (f := k a τ)]
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (k a τ ∘ ⇑g) x = g (k a τ x)
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (k a τ ∘ ⇑g) x = g (k a τ x)
Tactic:
rw [k_commute hτ]
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (⇑g ∘ k a τ) x = g (k a τ x)
Theorem: OnCycleFactors.φ'_mem_stabilizer
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
x : α
⊢ (⇑g ∘ k a τ) x = g (k a τ x)
Tactic:
rfl
Proof state after:
no goals
Theorem: OnCycleFactors.mem_Iφ_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g ↔
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
simp only [Iφ]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈
      {
        toSubmonoid :=
          {
            toSubsemigroup :=
              {
                carrier :=
                  {τ |
                    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
                      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card},
                mul_mem' := ⋯ },
            one_mem' := ⋯ },
        inv_mem' := ⋯ } ↔
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Theorem: OnCycleFactors.mem_Iφ_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈
      {
        toSubmonoid :=
          {
            toSubsemigroup :=
              {
                carrier :=
                  {τ |
                    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
                      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card},
                mul_mem' := ⋯ },
            one_mem' := ⋯ },
        inv_mem' := ⋯ } ↔
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rfl
Proof state after:
no goals
Theorem: OnCycleFactors.φ'_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ Equiv.Perm.support (ConjAct.ofConjAct ↑((φ' a) τ)) ≤ Equiv.Perm.support g
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ x ∈ Equiv.Perm.support (ConjAct.ofConjAct ↑((φ' a) τ)) → x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.φ'_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ x ∈ Equiv.Perm.support (ConjAct.ofConjAct ↑((φ' a) τ)) → x ∈ Equiv.Perm.support g
Tactic:
simp only [Equiv.Perm.mem_support]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x → g x ≠ x
Theorem: OnCycleFactors.φ'_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x → g x ≠ x
Tactic:
intro hx' hx
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ False
Theorem: OnCycleFactors.φ'_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ False
Tactic:
apply hx'
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x
Theorem: OnCycleFactors.φ'_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x
Tactic:
rw [← Equiv.Perm.not_mem_support] at hx
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : x ∉ Equiv.Perm.support g
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x
Theorem: OnCycleFactors.φ'_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : x ∉ Equiv.Perm.support g
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x
Tactic:
exact OnCycleFactors.k_apply_of_not_mem_support x hx
Proof state after:
no goals
Theorem: OnCycleFactors.hφ'_equivariant
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ↑((φ' a) τ) • ↑c = ↑(↑τ c)
Tactic:
rw [ConjAct.smul_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹ = ↑(↑τ c)