internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Tactic:
by_cases hp : p
Proof state after:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1

case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Tactic:
simp only [dif_pos hp]
Proof state after:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = Fintype.card (β hp)
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = Fintype.card (β hp)
Tactic:
rw [Fintype.card_eq]
Proof state after:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Nonempty (((hp : p) → β hp) ≃ β hp)
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Nonempty (((hp : p) → β hp) ≃ β hp)
Tactic:
exact ⟨@Equiv.funUnique p (β hp) (uniqueProp hp)⟩
Proof state after:
no goals
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Tactic:
simp only [dif_neg hp]
Proof state after:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = 1
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = 1
Tactic:
rw [Fintype.card_eq_one_iff]
Proof state after:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∃ x, ∀ (y : (hp : p) → β hp), y = x
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∃ x, ∀ (y : (hp : p) → β hp), y = x
Tactic:
use (fun h => False.elim (hp h))
Proof state after:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∀ (y : (hp : p) → β hp), y = fun h => ⋯.elim
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∀ (y : (hp : p) → β hp), y = fun h => ⋯.elim
Tactic:
intro u
Proof state after:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
⊢ u = fun h => ⋯.elim
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
⊢ u = fun h => ⋯.elim
Tactic:
ext h
Proof state after:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ u h = ⋯.elim
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ u h = ⋯.elim
Tactic:
exfalso
Proof state after:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ False
Theorem: OnCycleFactors.Fintype.card_pfun
Proof state before:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ False
Tactic:
exact hp h
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Set.range ⇑(θ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Set.card_range_of_injective (hθ_injective g)]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card
      (Equiv.Perm ↑(Function.fixedPoints ⇑g) ×
        ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card
      (Equiv.Perm ↑(Function.fixedPoints ⇑g) ×
        ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Fintype.card_prod]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (Equiv.Perm ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (Equiv.Perm ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Fintype.card_perm]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Fintype.card_pi]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) *
      Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g))
Tactic:
apply congr_arg
Proof state after:
case hx.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hx.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Tactic:
exact Equiv.Perm.card_fixedBy g
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) = Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Equiv.Perm.cycleType]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
simp only [Finset.univ_eq_attach, Finset.attach_val, Function.comp_apply]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Finset.attach (Equiv.Perm.cycleFactorsFinset g)) fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Finset.attach (Equiv.Perm.cycleFactorsFinset g)) fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [Finset.prod_attach (s := g.cycleFactorsFinset) (f := fun a ↦ Fintype.card (Subgroup.zpowers (a : Equiv.Perm α)))]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Equiv.Perm.cycleFactorsFinset g) fun x => Fintype.card ↥(Subgroup.zpowers x)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Equiv.Perm.cycleFactorsFinset g) fun x => Fintype.card ↥(Subgroup.zpowers x)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [Finset.prod]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod (Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod (Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
apply congr_arg
Proof state after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val =
    Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val =
    Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val
Tactic:
apply Multiset.map_congr rfl
Proof state after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val, Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val, Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card
Tactic:
intro x hx
Proof state after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card
Tactic:
rw [Fintype.card_zpowers, Equiv.Perm.IsCycle.orderOf]
Proof state after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Equiv.Perm.IsCycle x
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Equiv.Perm.IsCycle x
Tactic:
simp only [Finset.mem_val, Equiv.Perm.mem_cycleFactorsFinset_iff] at hx
Proof state after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : Equiv.Perm.IsCycle x ∧ ∀ a ∈ Equiv.Perm.support x, x a = g a
⊢ Equiv.Perm.IsCycle x
Theorem: OnCycleFactors.hψ_range_card
Proof state before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : Equiv.Perm.IsCycle x ∧ ∀ a ∈ Equiv.Perm.support x, x a = g a
⊢ Equiv.Perm.IsCycle x
Tactic:
exact hx.left
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.conj_stabilizer_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [Subgroup.card_eq_card_quotient_mul_card_subgroup (φ g).ker]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) ⧸ MonoidHom.ker (φ g)) *
      Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Theorem: OnCycleFactors.Equiv.Perm.conj_stabilizer_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) ⧸ MonoidHom.ker (φ g)) *
      Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [Fintype.card_congr (QuotientGroup.quotientKerEquivRange (φ g)).toEquiv]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) * Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Theorem: OnCycleFactors.Equiv.Perm.conj_stabilizer_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) * Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [← Nat.card_eq_fintype_card, hφ_range_card]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g))) *
      Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Theorem: OnCycleFactors.Equiv.Perm.conj_stabilizer_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g))) *
      Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [mul_comm]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g))) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Theorem: OnCycleFactors.Equiv.Perm.conj_stabilizer_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [← hψ_range_card]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) = Fintype.card ↑(Set.range ⇑(θ g))
Theorem: OnCycleFactors.Equiv.Perm.conj_stabilizer_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) = Fintype.card ↑(Set.range ⇑(θ g))
Tactic:
rw [hψ_range_card']
Proof state after:
no goals
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g : G
⊢ {k | IsConj g k} = MulAction.orbit (ConjAct G) g
Tactic:
ext k
Proof state after:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ {k | IsConj g k} ↔ k ∈ MulAction.orbit (ConjAct G) g
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ {k | IsConj g k} ↔ k ∈ MulAction.orbit (ConjAct G) g
Tactic:
simp only [Set.mem_setOf_eq, isConj_iff, MulAction.mem_orbit_iff, ConjAct.smul_def]
Proof state after:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) ↔ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) ↔ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
Tactic:
constructor
Proof state after:
case h.mp
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) → ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h.mp
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) → ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
rintro ⟨c, hc⟩
Proof state after:
case h.mp.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k