internlm/Lean-Github huggingface dataset:
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 }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹ = ↑(↑τ c)
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
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c = ↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)
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 }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c = ↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ) * ↑c) x = (↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)) x
Theorem: OnCycleFactors.hφ'_equivariant
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ) * ↑c) x = (↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)) x
Tactic:
exact OnCycleFactors.k_cycle_apply τ.prop c x
Proof state after:
no goals
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ (φ g) ((φ' a) τ) = ↑τ
Tactic:
apply Equiv.Perm.ext
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ ∀ (x : ↑↑(Equiv.Perm.cycleFactorsFinset g)), ((φ g) ((φ' a) τ)) x = ↑τ x
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ ∀ (x : ↑↑(Equiv.Perm.cycleFactorsFinset g)), ((φ g) ((φ' a) τ)) x = ↑τ x
Tactic:
rintro ⟨c, hc⟩
Proof state after:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ((φ g) ((φ' a) τ)) { val := c, property := hc } = ↑τ { val := c, property := hc }
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ((φ g) ((φ' a) τ)) { val := c, property := hc } = ↑τ { val := c, property := hc }
Tactic:
rw [← Subtype.coe_inj]
Proof state after:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(((φ g) ((φ' a) τ)) { val := c, property := hc }) = ↑(↑τ { val := c, property := hc })
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(((φ g) ((φ' a) τ)) { val := c, property := hc }) = ↑(↑τ { val := c, property := hc })
Tactic:
convert φ_eq'2 g ((φ' a τ)) ⟨c, hc⟩
Proof state after:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc } * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc } * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹
Tactic:
rw [eq_mul_inv_iff_mul_eq]
Proof state after:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }
Tactic:
ext x
Proof state after:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ)) x =
    (ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }) x
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ)) x =
    (ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }) x
Tactic:
simp only [Finset.coe_sort_coe, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x) = (ConjAct.ofConjAct ↑((φ' a) τ)) (c x)
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x) = (ConjAct.ofConjAct ↑((φ' a) τ)) (c x)
Tactic:
apply symm
Proof state after:
case h.e'_3.H.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) (c x) = ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x)
Theorem: OnCycleFactors.hφ'_is_rightInverse
Proof state before:
case h.e'_3.H.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) (c x) = ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x)
Tactic:
exact (k_cycle_apply τ.prop ⟨c, hc⟩ x)
Proof state after:
no goals
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Iφ g = MonoidHom.range (φ g)
Tactic:
obtain ⟨a⟩ := g.existsBasis
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
⊢ Iφ g = MonoidHom.range (φ g)
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
⊢ Iφ g = MonoidHom.range (φ g)
Tactic:
ext τ
Proof state after:
case intro.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g ↔ τ ∈ MonoidHom.range (φ g)
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
case intro.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g ↔ τ ∈ MonoidHom.range (φ g)
Tactic:
constructor
Proof state after:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g → τ ∈ MonoidHom.range (φ g)

case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) → τ ∈ Iφ g
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g → τ ∈ MonoidHom.range (φ g)
Tactic:
intro hτ
Proof state after:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ : τ ∈ Iφ g
⊢ τ ∈ MonoidHom.range (φ g)
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ : τ ∈ Iφ g
⊢ τ ∈ MonoidHom.range (φ g)
Tactic:
exact ⟨(φ' a) ⟨τ, hτ⟩, hφ'_is_rightInverse ⟨τ, hτ⟩⟩
Proof state after:
no goals
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) → τ ∈ Iφ g
Tactic:
rw [mem_Iφ_iff]
Proof state after:
case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) →
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Theorem: OnCycleFactors.Iφ_eq_range
Proof state before:
case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) →
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
exact hφ_eq_card_of_mem_range
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_mem_range_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ MonoidHom.range (φ g) ↔
    ∀ (c : ↑↑(Equiv.Perm.cycleFactorsFinset g)), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
simp only [← Iφ_eq_range, mem_Iφ_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card) ↔
    ∀ (c : ↑↑(Equiv.Perm.cycleFactorsFinset g)), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Theorem: OnCycleFactors.hφ_mem_range_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card) ↔
    ∀ (c : ↑↑(Equiv.Perm.cycleFactorsFinset g)), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rfl
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ↑(MonoidHom.range (φ g)) = {τ | fsc ∘ ⇑τ = fsc}
Tactic:
rw [← Iφ_eq_range]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ↑(Iφ g) = {τ | fsc ∘ ⇑τ = fsc}
Theorem: OnCycleFactors.hφ_range'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ↑(Iφ g) = {τ | fsc ∘ ⇑τ = fsc}
Tactic:
ext τ
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ τ ∈ {τ | fsc ∘ ⇑τ = fsc}
Theorem: OnCycleFactors.hφ_range'
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ τ ∈ {τ | fsc ∘ ⇑τ = fsc}
Tactic:
simp only [Finset.coe_sort_coe, Set.mem_setOf_eq, Function.funext_iff, Function.comp_apply]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a
Theorem: OnCycleFactors.hφ_range'
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a
Tactic:
simp only [SetLike.mem_coe, mem_Iφ_iff]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card) ↔
    ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a
Theorem: OnCycleFactors.hφ_range'
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card) ↔
    ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a
Tactic:
apply forall_congr'
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(τ a)).card = (Equiv.Perm.support ↑a).card ↔ fsc (τ a) = fsc a
Theorem: OnCycleFactors.hφ_range'
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(τ a)).card = (Equiv.Perm.support ↑a).card ↔ fsc (τ a) = fsc a
Tactic:
intro c
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card ↔ fsc (τ c) = fsc c
Theorem: OnCycleFactors.hφ_range'
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card ↔ fsc (τ c) = fsc c
Tactic:
simp only [← Function.Injective.eq_iff Fin.val_injective, fsc]
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Nat.card ↥(MonoidHom.range (φ g)) = Fintype.card ↑{k | fsc ∘ ⇑k = fsc}
Tactic:
simp_rw [← hφ_range', Nat.card_eq_fintype_card]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) = Fintype.card ↑↑(MonoidHom.range (φ g))
Theorem: OnCycleFactors.hφ_range_card'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) = Fintype.card ↑↑(MonoidHom.range (φ g))
Tactic:
rfl
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Nat.card ↥(MonoidHom.range (φ g)) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [hφ_range_card', Equiv.Perm.of_partition_card]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | fsc a = i})) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
Tactic:
rintro ⟨i, hi⟩
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi }) (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi }) (Equiv.Perm.cycleType g)
Tactic:
rw [Equiv.Perm.cycleType_def]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi })
      (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi })
      (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
simp only [Fin.val_mk]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count i (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count i (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [← Set.ncard_filter_eq_count (Finset.card ∘ Equiv.Perm.support) g.cycleFactorsFinset i]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
Tactic:
simp only [Set.coe_setOf, Set.mem_setOf_eq, Function.comp_apply]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Tactic:
let u : {x : g.cycleFactorsFinset | fsc x = ⟨i, hi⟩} →
    {x ∈ g.cycleFactorsFinset | (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun ⟨⟨x, hx⟩, hx'⟩ => ⟨x, by
    simp only [fsc, Fin.mk.injEq, Set.mem_setOf_eq] at hx'
    simp only [Function.comp_apply, Set.mem_setOf_eq]
    exact ⟨hx, hx'⟩⟩
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Tactic:
rw [← Set.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Fintype.card ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Fintype.card ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Tactic:
apply Fintype.card_of_bijective this
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
⊢ ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
Tactic:
intro i hi
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i < Fintype.card α + 1