internlm/Lean-Github huggingface dataset:
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ Perm.Disjoint (List.formPerm a) (List.formPerm b)
Tactic:
rw [List.formPerm_disjoint_iff (hp_nodup a ha) (hp_nodup b hb) (hp2 a ha) (hp2 b hb)]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ List.Disjoint a b
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ List.Disjoint a b
Tactic:
exact hab
Proof state after:
no goals
Theorem: Equiv.Perm.conj_support_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ a ∈ support (k • g) ↔ (ConjAct.ofConjAct k⁻¹) a ∈ support g
Tactic:
simp only [Equiv.Perm.mem_support, ConjAct.smul_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a ≠ a ↔ g ((ConjAct.ofConjAct k⁻¹) a) ≠ (ConjAct.ofConjAct k⁻¹) a
Theorem: Equiv.Perm.conj_support_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a ≠ a ↔ g ((ConjAct.ofConjAct k⁻¹) a) ≠ (ConjAct.ofConjAct k⁻¹) a
Tactic:
rw [not_iff_not]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a = a ↔ g ((ConjAct.ofConjAct k⁻¹) a) = (ConjAct.ofConjAct k⁻¹) a
Theorem: Equiv.Perm.conj_support_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a = a ↔ g ((ConjAct.ofConjAct k⁻¹) a) = (ConjAct.ofConjAct k⁻¹) a
Tactic:
simp only [Equiv.Perm.coe_mul, Function.comp_apply, ConjAct.ofConjAct_inv]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k) (g ((ConjAct.ofConjAct k)⁻¹ a)) = a ↔ g ((ConjAct.ofConjAct k)⁻¹ a) = (ConjAct.ofConjAct k)⁻¹ a
Theorem: Equiv.Perm.conj_support_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k) (g ((ConjAct.ofConjAct k)⁻¹ a)) = a ↔ g ((ConjAct.ofConjAct k)⁻¹ a) = (ConjAct.ofConjAct k)⁻¹ a
Tactic:
apply Equiv.apply_eq_iff_eq_symm_apply
Proof state after:
no goals
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ c ∈ cycleFactorsFinset g
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹) → c ∈ cycleFactorsFinset g

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹) → c ∈ cycleFactorsFinset g
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ c ∈ cycleFactorsFinset g
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ c ∈ cycleFactorsFinset g
Tactic:
suffices ∀ h : Equiv.Perm α, h = k⁻¹ * (k * h * k⁻¹) * k by
  rw [this g, this c]
  apply imp_lemma
  exact h
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h✝ : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : Perm α
⊢ h = k⁻¹ * (k * h * k⁻¹) * k
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h✝ : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : Perm α
⊢ h = k⁻¹ * (k * h * k⁻¹) * k
Tactic:
group
Proof state after:
no goals
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
this : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ c ∈ cycleFactorsFinset g
Tactic:
rw [this g, this c]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
this : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ k⁻¹ * (k * c * k⁻¹) * k ∈ cycleFactorsFinset (k⁻¹ * (k * g * k⁻¹) * k)
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
this : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ k⁻¹ * (k * c * k⁻¹) * k ∈ cycleFactorsFinset (k⁻¹ * (k * g * k⁻¹) * k)
Tactic:
apply imp_lemma
Proof state after:
case x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
this : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
h : k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
this : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Tactic:
exact h
Proof state after:
no goals
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
⊢ c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Tactic:
apply imp_lemma g k c
Proof state after:
no goals
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ ∀ (g k c : Perm α), c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Tactic:
intro g k c
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ c ∈ cycleFactorsFinset g → k * c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Tactic:
simp only [Equiv.Perm.mem_cycleFactorsFinset_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (IsCycle c ∧ ∀ a ∈ support c, c a = g a) →
    IsCycle (k * c * k⁻¹) ∧ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (IsCycle c ∧ ∀ a ∈ support c, c a = g a) →
    IsCycle (k * c * k⁻¹) ∧ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Tactic:
rintro ⟨hc, hc'⟩
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ IsCycle (k * c * k⁻¹) ∧ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ IsCycle (k * c * k⁻¹) ∧ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Tactic:
constructor
Proof state after:
case intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ IsCycle (k * c * k⁻¹)

case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ IsCycle (k * c * k⁻¹)

case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Tactic:
exact Equiv.Perm.IsCycle.conj hc
Proof state after:
case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
⊢ ∀ a ∈ support (k * c * k⁻¹), (k * c * k⁻¹) a = (k * g * k⁻¹) a
Tactic:
intro a ha
Proof state after:
case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : a ∈ support (k * c * k⁻¹)
⊢ (k * c * k⁻¹) a = (k * g * k⁻¹) a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : a ∈ support (k * c * k⁻¹)
⊢ (k * c * k⁻¹) a = (k * g * k⁻¹) a
Tactic:
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
Proof state after:
case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : a ∈ support (k * c * k⁻¹)
⊢ c (k⁻¹ a) = g (k⁻¹ a)
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : a ∈ support (k * c * k⁻¹)
⊢ c (k⁻¹ a) = g (k⁻¹ a)
Tactic:
apply hc'
Proof state after:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : a ∈ support (k * c * k⁻¹)
⊢ k⁻¹ a ∈ support c
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : a ∈ support (k * c * k⁻¹)
⊢ k⁻¹ a ∈ support c
Tactic:
rw [Equiv.Perm.mem_support] at ha ⊢
Proof state after:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
⊢ c (k⁻¹ a) ≠ k⁻¹ a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
⊢ c (k⁻¹ a) ≠ k⁻¹ a
Tactic:
intro ha'
Proof state after:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c (k⁻¹ a) = k⁻¹ a
⊢ False
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c (k⁻¹ a) = k⁻¹ a
⊢ False
Tactic:
apply ha
Proof state after:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c (k⁻¹ a) = k⁻¹ a
⊢ (k * c * k⁻¹) a = a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c (k⁻¹ a) = k⁻¹ a
⊢ (k * c * k⁻¹) a = a
Tactic:
simp only [mul_smul, ← Equiv.Perm.smul_def] at ha' ⊢
Proof state after:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c • k⁻¹ • a = k⁻¹ • a
⊢ k • c • k⁻¹ • a = a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c • k⁻¹ • a = k⁻¹ • a
⊢ k • c • k⁻¹ • a = a
Tactic:
rw [ha']
Proof state after:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c • k⁻¹ • a = k⁻¹ • a
⊢ k • k⁻¹ • a = a
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state before:
case intro.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : IsCycle c
hc' : ∀ a ∈ support c, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
ha' : c • k⁻¹ • a = k⁻¹ • a
⊢ k • k⁻¹ • a = a
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.apply_inv_self]
Proof state after:
no goals
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k : Perm α
⊢ cycleFactorsFinset (k * g * k⁻¹) = Finset.map (Equiv.toEmbedding (MulAut.conj k).toEquiv) (cycleFactorsFinset g)
Tactic:
ext c
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔
    c ∈ Finset.map (Equiv.toEmbedding (MulAut.conj k).toEquiv) (cycleFactorsFinset g)
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔
    c ∈ Finset.map (Equiv.toEmbedding (MulAut.conj k).toEquiv) (cycleFactorsFinset g)
Tactic:
rw [Finset.mem_map_equiv]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ (MulAut.conj k).symm c ∈ cycleFactorsFinset g
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ (MulAut.conj k).symm c ∈ cycleFactorsFinset g
Tactic:
rw [← Equiv.Perm.mem_cycleFactorsFinset_conj g k]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Tactic:
apply iff_of_eq
Proof state after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ (c ∈ cycleFactorsFinset (k * g * k⁻¹)) = (k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹))
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ (c ∈ cycleFactorsFinset (k * g * k⁻¹)) = (k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹))
Tactic:
apply congr_arg₂ _ _
Proof state after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ cycleFactorsFinset (k * g * k⁻¹) = cycleFactorsFinset (k * g * k⁻¹)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ cycleFactorsFinset (k * g * k⁻¹) = cycleFactorsFinset (k * g * k⁻¹)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹
Tactic:
rfl
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹
Tactic:
simp only [MulEquiv.toEquiv_eq_coe, MulEquiv.coe_toEquiv_symm, MulAut.conj_symm_apply]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (k⁻¹ * c * k) * k⁻¹
Theorem: Equiv.Perm.cycleFactorsFinset_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (k⁻¹ * c * k) * k⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k • c ∈ cycleFactorsFinset (k • g) ↔ c ∈ cycleFactorsFinset g
Tactic:
simp only [ConjAct.smul_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      cycleFactorsFinset (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) ↔
    c ∈ cycleFactorsFinset g
Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      cycleFactorsFinset (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) ↔
    c ∈ cycleFactorsFinset g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_conj
Proof state after:
no goals
Theorem: Equiv.Perm.cycleFactorsFinset_conj_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ cycleFactorsFinset (k • g) = k • cycleFactorsFinset g
Tactic:
ext c
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ cycleFactorsFinset (k • g) ↔ c ∈ k • cycleFactorsFinset g
Theorem: Equiv.Perm.cycleFactorsFinset_conj_eq
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ cycleFactorsFinset (k • g) ↔ c ∈ k • cycleFactorsFinset g
Tactic:
rw [← Equiv.Perm.mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ cycleFactorsFinset (k⁻¹ • k • g) ↔ c ∈ k • cycleFactorsFinset g
Theorem: Equiv.Perm.cycleFactorsFinset_conj_eq
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ cycleFactorsFinset (k⁻¹ • k • g) ↔ c ∈ k • cycleFactorsFinset g
Tactic:
simp only [inv_smul_smul]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ cycleFactorsFinset g ↔ c ∈ k • cycleFactorsFinset g
Theorem: Equiv.Perm.cycleFactorsFinset_conj_eq
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ cycleFactorsFinset g ↔ c ∈ k • cycleFactorsFinset g
Tactic:
exact Finset.inv_smul_mem_iff
Proof state after:
no goals
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ Commute k g
Tactic:
rw [← Equiv.Perm.cycleFactorsFinset_noncommProd g (Equiv.Perm.cycleFactorsFinset_mem_commute g)]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ Commute k (Finset.noncommProd (cycleFactorsFinset g) id ⋯)
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ Commute k (Finset.noncommProd (cycleFactorsFinset g) id ⋯)
Tactic:
apply Finset.noncommProd_commute
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k (id x)
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k (id x)
Tactic:
simp only [id.def]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k x