internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0
Tactic:
conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n * g ^ (m - n)) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n * g ^ (m - n)) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0
Tactic:
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq,
  EuclideanDomain.mod_eq_zero]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n
Tactic:
rw [← Equiv.Perm.cycleOf_zpow_apply_self g x]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n
Tactic:
rw [Equiv.Perm.cycle_zpow_mem_support_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(support (cycleOf g x)).card = 0 ↔ ↑(support (cycleOf g x)).card ∣ m - n

case hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ IsCycle (cycleOf g x)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x) x ≠ x
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(support (cycleOf g x)).card = 0 ↔ ↑(support (cycleOf g x)).card ∣ m - n
Tactic:
simp only [EuclideanDomain.mod_eq_zero]
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
case hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ IsCycle (cycleOf g x)
Tactic:
exact Equiv.Perm.isCycle_cycleOf g hx
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x) x ≠ x
Tactic:
simp only [Equiv.Perm.mem_support, Equiv.Perm.cycleOf_apply_self]
Proof state after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x
Tactic:
exact hx
Proof state after:
no goals
Theorem: commute_ofSubtype_disjoint
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
⊢ Commute (Equiv.Perm.ofSubtype x) (Equiv.Perm.ofSubtype y)
Tactic:
apply Equiv.Perm.Disjoint.commute
Proof state after:
case h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
⊢ Equiv.Perm.Disjoint (Equiv.Perm.ofSubtype x) (Equiv.Perm.ofSubtype y)
Theorem: commute_ofSubtype_disjoint
Proof state before:
case h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
⊢ Equiv.Perm.Disjoint (Equiv.Perm.ofSubtype x) (Equiv.Perm.ofSubtype y)
Tactic:
intro a
Proof state after:
case h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Tactic:
by_cases hx : p a
Proof state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ (Equiv.Perm.ofSubtype y) a = a

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : ¬p a
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem y]
Proof state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ a = a

case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ ¬q a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ a = a

case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ ¬q a
Tactic:
apply Or.intro_right
Proof state after:
case pos.h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ a = a

case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ ¬q a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case pos.h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ a = a

case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ ¬q a
Tactic:
rfl
Proof state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ ¬q a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : p a
⊢ ¬q a
Tactic:
exact not_and.mp (hpq a) hx
Proof state after:
no goals
Theorem: commute_ofSubtype_disjoint
Proof state before:
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : ¬p a
⊢ (Equiv.Perm.ofSubtype x) a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem x hx]
Proof state after:
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : ¬p a
⊢ a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : ¬p a
⊢ a = a ∨ (Equiv.Perm.ofSubtype y) a = a
Tactic:
apply Or.intro_left
Proof state after:
case neg.h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : ¬p a
⊢ a = a
Theorem: commute_ofSubtype_disjoint
Proof state before:
case neg.h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hpq : ∀ (a : α), ¬(p a ∧ q a)
x : Equiv.Perm (Subtype p)
y : Equiv.Perm (Subtype q)
a : α
hx : ¬p a
⊢ a = a
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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})
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof 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)
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof state after:
no goals
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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})
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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 })
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof 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 })
Theorem: Equiv.Perm.of_partition_card
Proof 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 _
Proof 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 })
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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
Proof 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
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof state after:
no goals
Theorem: Equiv.Perm.of_partition_card
Proof 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]
Proof state after:
no goals
Theorem: Equiv.Perm.existsBasis
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nonempty (Equiv.Perm.Basis g)
Tactic:
suffices hsupp_ne :
  ∀ c : g.cycleFactorsFinset, (c : Equiv.Perm α).support.Nonempty by
  exact ⟨fun c ↦ (hsupp_ne c).choose, fun c ↦ (hsupp_ne c).choose_spec⟩
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑c).Nonempty
Theorem: Equiv.Perm.existsBasis
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑c).Nonempty
Tactic:
intro c
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑c).Nonempty
Theorem: Equiv.Perm.existsBasis
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑c).Nonempty
Tactic:
exact Equiv.Perm.IsCycle.nonempty_support (Equiv.Perm.mem_cycleFactorsFinset_iff.mp c.prop).1
Proof state after:
no goals