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

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
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⁻¹)

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
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

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
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

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
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

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
State after:
no goals

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]
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)

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
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⁻¹)

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
State after:
no goals

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
State after:
no goals

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
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⁻¹)

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]
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

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'⟩
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

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
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

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
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

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
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

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]
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)

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'
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

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 ⊢
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

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'
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

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
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

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' ⊢
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

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']
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

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]
State after:
no goals