Theorem: Equiv.Perm.of_partition_card (Jordan/ConjClassCount.lean)

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
⊢ Fintype.card ↑{f | p ∘ ⇑f = p} = Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})
Tactic:
suffices ∀ x : Equiv.Perm α, (x ∈ MulAction.stabilizer (Equiv.Perm α) p ↔ p ∘ x = p) by
  simp_rw [← this]
  suffices Fintype.card {f | f ∈ MulAction.stabilizer (Equiv.Perm α) p} = Fintype.card (MulAction.stabilizer (Equiv.Perm α) p) by
    rw [this, Fintype.card_congr (Φ p).toEquiv]
    simp only [Set.coe_setOf, Set.mem_setOf_eq, Fintype.card_pi]
    apply Finset.prod_congr rfl
    intro i _
    exact Fintype.card_perm
  rw [Fintype.card_ofFinset, ← Fintype.subtype_card]
  intro x
  simp only [MulAction.mem_stabilizer_iff, Set.mem_setOf_eq, Finset.mem_univ, forall_true_left, ne_eq,
    Finset.mem_filter, true_and]
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
⊢ ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ Fintype.card ↑{f | p ∘ ⇑f = p} = Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})
Tactic:
simp_rw [← this]
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} =
    Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} =
    Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})
Tactic:
suffices Fintype.card {f | f ∈ MulAction.stabilizer (Equiv.Perm α) p} = Fintype.card (MulAction.stabilizer (Equiv.Perm α) p) by
  rw [this, Fintype.card_congr (Φ p).toEquiv]
  simp only [Set.coe_setOf, Set.mem_setOf_eq, Fintype.card_pi]
  apply Finset.prod_congr rfl
  intro i _
  exact Fintype.card_perm
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
Tactic:
rw [Fintype.card_ofFinset, ← Fintype.subtype_card]
State after:
case H
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ ∀ (x : Perm α),
    x ∈ Finset.filter (fun x => x ∈ {f | f ∈ MulAction.stabilizer (Perm α) p}) Finset.univ ↔
      x ∈ MulAction.stabilizer (Perm α) p

State before:
case H
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
⊢ ∀ (x : Perm α),
    x ∈ Finset.filter (fun x => x ∈ {f | f ∈ MulAction.stabilizer (Perm α) p}) Finset.univ ↔
      x ∈ MulAction.stabilizer (Perm α) p
Tactic:
intro x
State after:
case H
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
x : Perm α
⊢ x ∈ Finset.filter (fun x => x ∈ {f | f ∈ MulAction.stabilizer (Perm α) p}) Finset.univ ↔
    x ∈ MulAction.stabilizer (Perm α) p

State before:
case H
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
x : Perm α
⊢ x ∈ Finset.filter (fun x => x ∈ {f | f ∈ MulAction.stabilizer (Perm α) p}) Finset.univ ↔
    x ∈ MulAction.stabilizer (Perm α) p
Tactic:
simp only [MulAction.mem_stabilizer_iff, Set.mem_setOf_eq, Finset.mem_univ, forall_true_left, ne_eq,
  Finset.mem_filter, true_and]
State after:
no goals

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} =
    Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})
Tactic:
rw [this, Fintype.card_congr (Φ p).toEquiv]
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ Fintype.card ((i : ι) → Perm ↑{a | p a = i}) =
    Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ Fintype.card ((i : ι) → Perm ↑{a | p a = i}) =
    Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | p a = i})
Tactic:
simp only [Set.coe_setOf, Set.mem_setOf_eq, Fintype.card_pi]
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ (Finset.prod Finset.univ fun a => Fintype.card (Perm { x // p x = a })) =
    Finset.prod Finset.univ fun x => Nat.factorial (Fintype.card { x_1 // p x_1 = x })

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ (Finset.prod Finset.univ fun a => Fintype.card (Perm { x // p x = a })) =
    Finset.prod Finset.univ fun x => Nat.factorial (Fintype.card { x_1 // p x_1 = x })
Tactic:
apply Finset.prod_congr rfl
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ ∀ x ∈ Finset.univ, Fintype.card (Perm { x_1 // p x_1 = x }) = Nat.factorial (Fintype.card { x_1 // p x_1 = x })

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
⊢ ∀ x ∈ Finset.univ, Fintype.card (Perm { x_1 // p x_1 = x }) = Nat.factorial (Fintype.card { x_1 // p x_1 = x })
Tactic:
intro i _
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
i : ι
a✝ : i ∈ Finset.univ
⊢ Fintype.card (Perm { x // p x = i }) = Nat.factorial (Fintype.card { x // p x = i })

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
this✝ : ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
this : Fintype.card ↑{f | f ∈ MulAction.stabilizer (Perm α) p} = Fintype.card ↥(MulAction.stabilizer (Perm α) p)
i : ι
a✝ : i ∈ Finset.univ
⊢ Fintype.card (Perm { x // p x = i }) = Nat.factorial (Fintype.card { x // p x = i })
Tactic:
exact Fintype.card_perm
State after:
no goals

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
⊢ ∀ (x : Perm α), x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
Tactic:
intro x
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
⊢ x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
⊢ x ∈ MulAction.stabilizer (Perm α) p ↔ p ∘ ⇑x = p
Tactic:
simp only [MulAction.mem_stabilizer_iff]
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
⊢ x • p = p ↔ p ∘ ⇑x = p

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
⊢ x • p = p ↔ p ∘ ⇑x = p
Tactic:
suffices ∀ x : Equiv.Perm α, (x • p = p ↔ p ∘ x = p) by
  simp_rw [this]
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
⊢ ∀ (x : Perm α), x • p = p ↔ p ∘ ⇑x = p

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
⊢ ∀ (x : Perm α), x • p = p ↔ p ∘ ⇑x = p
Tactic:
intro x
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x✝ x : Perm α
⊢ x • p = p ↔ p ∘ ⇑x = p

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x✝ x : Perm α
⊢ x • p = p ↔ p ∘ ⇑x = p
Tactic:
change p ∘ (x⁻¹ : Equiv.Perm α) = p ↔ p ∘ x = p
State after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x✝ x : Perm α
⊢ p ∘ ⇑x⁻¹ = p ↔ p ∘ ⇑x = p

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x✝ x : Perm α
⊢ p ∘ ⇑x⁻¹ = p ↔ p ∘ ⇑x = p
Tactic:
rw [Equiv.Perm.inv_def, Equiv.comp_symm_eq, eq_comm]
State after:
no goals

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : α → ι
x : Perm α
this : ∀ (x : Perm α), x • p = p ↔ p ∘ ⇑x = p
⊢ x • p = p ↔ p ∘ ⇑x = p
Tactic:
simp_rw [this]
State after:
no goals