-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem mem_cycleFactorsFinset_conj (g k c : Perm α) :
    k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
refine ⟨fun h ↦ ?_, imp_lemma⟩

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ c ∈ g.cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
aux : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ k⁻¹ * (k * c * k⁻¹) * k ∈ (k⁻¹ * (k * g * k⁻¹) * k).cycleFactorsFinset

Tactic:
exact imp_lemma h

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
suffices imp_lemma : ∀ {g k c : Perm α},
    c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset by
  refine ⟨fun h ↦ ?_, imp_lemma⟩
  have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
  rw [aux g, aux c]
  exact imp_lemma h

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Proof state:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : c • k⁻¹ • a = k⁻¹ • a
⊢ k • k⁻¹ • a = a

Tactic:
simp only [Perm.smul_def, apply_inv_self]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Tactic:
intro g k c

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (∀ a ∈ c.support, c a = g a) → ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a

Tactic:
intro hc a ha

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ (k * c * k⁻¹) a = (k * g * k⁻¹) a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
x✝ : Perm α
⊢ x✝ = k⁻¹ * (k * x✝ * k⁻¹) * k

Tactic:
group

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Tactic:
simp only [mem_cycleFactorsFinset_iff]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (c.IsCycle ∧ ∀ a ∈ c.support, c a = g a) →
    (k * c * k⁻¹).IsCycle ∧ ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a

Proof state:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : c (k⁻¹ a) = k⁻¹ a
⊢ (k * c * k⁻¹) a = a

Tactic:
simp only [mul_smul, ← Perm.smul_def] at ha ⊢

Result:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : c • k⁻¹ • a = k⁻¹ • a
⊢ k • c • k⁻¹ • a = a

Proof state:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ k⁻¹ a ∈ c.support

Tactic:
rw [mem_support] at ha ⊢

Result:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
⊢ c (k⁻¹ a) ≠ k⁻¹ a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ c ∈ g.cycleFactorsFinset

Tactic:
have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
aux : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ c ∈ g.cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
aux : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ c ∈ g.cycleFactorsFinset

Tactic:
rw [aux g, aux c]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
aux : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ k⁻¹ * (k * c * k⁻¹) * k ∈ (k⁻¹ * (k * g * k⁻¹) * k).cycleFactorsFinset

Proof state:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : c • k⁻¹ • a = k⁻¹ • a
⊢ k • c • k⁻¹ • a = a

Tactic:
rw [ha]

Result:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : c • k⁻¹ • a = k⁻¹ • a
⊢ k • k⁻¹ • a = a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ c (k⁻¹ a) = g (k⁻¹ a)

Tactic:
apply hc

Result:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ k⁻¹ a ∈ c.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (c.IsCycle ∧ ∀ a ∈ c.support, c a = g a) →
    (k * c * k⁻¹).IsCycle ∧ ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a

Tactic:
apply And.imp IsCycle.conj

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (∀ a ∈ c.support, c a = g a) → ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a

Proof state:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : (k * c * k⁻¹) a ≠ a
⊢ c (k⁻¹ a) ≠ k⁻¹ a

Tactic:
contrapose! ha

Result:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : c (k⁻¹ a) = k⁻¹ a
⊢ (k * c * k⁻¹) a = a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ (k * c * k⁻¹) a = (k * g * k⁻¹) a

Tactic:
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ c (k⁻¹ a) = g (k⁻¹ a)