awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
refine_3 : f * g.cycleFactorsFinset.noncommProd id ⋯ = f * g
refine_3₁ refine_3₂ : f * g = f * g
⊢ f.cycleFactorsFinset.noncommProd id ⋯ * g.cycleFactorsFinset.noncommProd id ⋯ = f * g

Tactic:
rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]

Premises used: Equiv.Perm.cycleFactorsFinset_noncommProd, Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f ∈ g.cycleFactorsFinset
⊢ f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
rw [mem_cycleFactorsFinset_iff] at h

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
pos : ∀ (hx : (f : (a : α) → α) x = x), (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
neg : ∀ (hx : ¬(f : (a : α) → α) x = x), (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : (f : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x

Tactic:
Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : (f : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x

Tactic:
exact Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : ¬(f : (a : α) → α) x = x
neg : (g * f⁻¹ : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x

Tactic:
left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ Membership.mem (α := α) f.support ((f⁻¹ : (a : α) → α) x : α)

Tactic:
simpa [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : ¬(f : (a : α) → α) x = x
neg : (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
⊢ (g * f⁻¹ : (a : α) → α) x = x

Tactic:
rw [mul_apply, ← h.right _ (by simpa [eq_symm_apply])]

Premises used: And.right, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
rw : c = c.cycleOf a
⊢ c = f.cycleOf a

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
a₁ : c.cycleOf a = c
⊢ c = c.cycleOf a

Tactic:
apply symm

Premises used: symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c.cycleOf a = c

Tactic:
Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)

Premises used: Equiv.Perm.mem_support, Equiv.Perm.IsCycle.cycleOf_eq, And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c.cycleOf a = c

Tactic:
exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)

Premises used: Equiv.Perm.mem_support, Equiv.Perm.IsCycle.cycleOf_eq, And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
suffices : f.cycleOf a = c.cycleOf a
⊢ c = f.cycleOf a

Tactic:
suffices f.cycleOf a = c.cycleOf a by
    rw [this]
    apply symm
    exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := ⋯
hfc2 : Commute c (f * c⁻¹) := ⋯
rw : f.cycleOf a = (c * (f * c⁻¹)).cycleOf a
hx : (f * c⁻¹ : (a : α) → α) a = a
⊢ f.cycleOf a = c.cycleOf a

Tactic:
rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]

Premises used: Equiv.Perm.cycleOf_mul_of_apply_right_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := ⋯
hfc2 : Commute c (f * c⁻¹) := ⋯
⊢ f.cycleOf a = (c * (f * c⁻¹)).cycleOf a

Tactic:
simp only [hfc2.eq, inv_mul_cancel_right]

Premises used: inv_mul_cancel_right, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := ⋯
hfc2 : Commute c (f * c⁻¹) := ⋯
⊢ (f * c⁻¹ : (a : α) → α) a = a

Tactic:
Equiv.Perm.notMem_support.mp
      (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.Disjoint.disjoint_support, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := ⋯
hfc2 : Commute c (f * c⁻¹) := ⋯
⊢ (f * c⁻¹ : (a : α) → α) a = a

Tactic:
exact
    Equiv.Perm.notMem_support.mp
      (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.Disjoint.disjoint_support, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
obtain : ∀ (x : α) (hx : x ∈ c.support), g.IsCycleOn (↑c.support : Set α)
⊢ g.IsCycleOn (↑c.support : Set α)

Tactic:
obtain ⟨x, hx⟩ := IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp hc).1

Premises used: Equiv.Perm.IsCycle.nonempty_support, And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
rw : g.IsCycleOn (↑(g.cycleOf x).support : Set α)
⊢ g.IsCycleOn (↑c.support : Set α)

Tactic:
rw [cycle_is_cycleOf hx hc]

Premises used: Equiv.Perm.cycle_is_cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn (↑(g.cycleOf x).support : Set α)

Tactic:
isCycleOn_support_cycleOf g x

Premises used: Equiv.Perm.isCycleOn_support_cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn (↑(g.cycleOf x).support : Set α)

Tactic:
exact isCycleOn_support_cycleOf g x

Premises used: Equiv.Perm.isCycleOn_support_cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
⊢ c = g.cycleOf x ↔ x ∈ c.support

Tactic:
⟨?_, (cycle_is_cycleOf · hc)⟩

Premises used: Equiv.Perm.cycle_is_cycleOf, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
refine : c = g.cycleOf x → x ∈ c.support
⊢ c = g.cycleOf x ↔ x ∈ c.support

Tactic:
refine ⟨?_, (cycle_is_cycleOf · hc)⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
rw : ¬g.cycleOf x = 1
⊢ x ∈ (g.cycleOf x).support

Tactic:
rw [mem_support, cycleOf_apply_self, ne_eq, ← cycleOf_eq_one_iff]

Premises used: Equiv.Perm.cycleOf_eq_one_iff, Equiv.Perm.mem_support, ne_eq, Equiv.Perm.cycleOf_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g.cycleOf x = 1

Tactic:
(mem_cycleFactorsFinset_iff.mp hc).left.ne_one

Premises used: Equiv.Perm.IsCycle.ne_one, And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g.cycleOf x = 1

Tactic:
exact (mem_cycleFactorsFinset_iff.mp hc).left.ne_one

Premises used: Equiv.Perm.IsCycle.ne_one, And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
rw : (↑c : Perm α) = g.cycleOf ((g ^ m : (a : α) → α) x) ↔ x ∈ (↑c : Perm α).support
rw₁ : (↑c : Perm α) = g.cycleOf x ↔ x ∈ (↑c : Perm α).support
rw₂ rw₃ : x ∈ (↑c : Perm α).support ↔ x ∈ (↑c : Perm α).support
⊢ Membership.mem (α := α) (↑c : Perm α).support ((g ^ m : (a : α) → α) x : α) ↔ x ∈ (↑c : Perm α).support

Tactic:
rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
    eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]

Premises used: Equiv.Perm.cycleOf_self_apply_zpow, Subtype.prop, Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : 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:
⟨fun h ↦ ?_, imp_lemma⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
refine : ∀ (h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset), c ∈ g.cycleFactorsFinset
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
refine ⟨fun h ↦ ?_, imp_lemma⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : 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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : 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
⊢ ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k

Tactic:
have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : 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
rw : k⁻¹ * (k * c * k⁻¹) * k ∈ (k⁻¹ * (k * g * k⁻¹) * k).cycleFactorsFinset
⊢ c ∈ g.cycleFactorsFinset

Tactic:
rw [aux g, aux c]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : 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:
imp_lemma h

Premises used: Set.Mem, setOf, Equiv.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : 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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
suffices : ∀ {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:
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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
simp :
  (c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
    (k * c * k⁻¹).IsCycle ∧
      ∀ a ∈ (k * c * k⁻¹).support, Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)
⊢ c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Tactic:
simp only [mem_cycleFactorsFinset_iff]

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
apply :
  (∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
    ∀ a ∈ (k * c * k⁻¹).support, Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)
⊢ (c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
    (k * c * k⁻¹).IsCycle ∧
      ∀ a ∈ (k * c * k⁻¹).support, Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)

Tactic:
apply And.imp IsCycle.conj

Premises used: And.imp, Equiv.Perm.IsCycle.conj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
hc : ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
a : α
ha : a ∈ (k * c * k⁻¹).support
simp :
  Eq (α := α) ((c : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α)
⊢ Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)

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

Premises used: Equiv.Perm.coe_mul, EmbeddingLike.apply_eq_iff_eq, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
hc : ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
a : α
ha : a ∈ (k * c * k⁻¹).support
a₁ : Membership.mem (α := α) c.support ((k⁻¹ : (a : α) → α) a : α)
⊢ Eq (α := α) ((c : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α)

Tactic:
apply hc
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
hc : ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ Membership.mem (α := α) c.support ((k⁻¹ : (a : α) → α) a : α)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
rw : Commute k (g.cycleFactorsFinset.noncommProd id ⋯)
⊢ Commute k g

Tactic:
rw [← cycleFactorsFinset_noncommProd g (cycleFactorsFinset_mem_commute g)]

Premises used: Equiv.Perm.cycleFactorsFinset_noncommProd, Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
h : ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)
⊢ Commute k (g.cycleFactorsFinset.noncommProd id ⋯)

Tactic:
apply Finset.noncommProd_commute

Premises used: Finset.noncommProd_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)

Tactic:
simpa only [id_eq] using hk

Premises used: id_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
hk : ∀ c_1 ∈ g.cycleFactorsFinset, Commute c c_1
⊢ Commute c g

Tactic:
apply commute_of_mem_cycleFactorsFinset_commute

Premises used: Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
pos : ∀ (hcc' : c = c'), Commute c c'
neg : ∀ (hcc' : ¬c = c'), Commute c c'
⊢ Commute c c'

Tactic:
by_cases hcc' : c = c'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : c = c'
pos pos₁ : Commute c' c'
⊢ Commute c c'

Tactic:
rw [hcc']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
neg : c ≠ c'
⊢ Commute c c'

Tactic:
apply g.cycleFactorsFinset_mem_commute hc hc'

Premises used: Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ c ≠ c'

Tactic:
hcc'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ c ≠ c'

Tactic:
exact hcc'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
simp : Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Membership.mem (α := α) c.support ((d : (a : α) → α) x : α) ↔ x ∈ c.support

Tactic:
simp only [mem_support, not_iff_not]

Premises used: not_iff_not, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
pos :
  ∀ (h : c = d),
    Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg :
  ∀ (h : ¬c = d),
    Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x

Tactic:
by_cases h : c = d
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
pos : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
pos₁ pos₂ : (c : (a : α) → α) x = x ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x

Tactic:
rw [← h, EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
neg : Eq (α := α) ((c * d : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg₁ : Eq (α := α) ((d * c : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg₂ : Eq (α := α) ((d : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg₃ neg₄ : (c : (a : α) → α) x = x ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x

Tactic:
rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq, Equiv.Perm.cycleFactorsFinset_mem_commute, Equiv.Perm.mul_apply, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
a : α
⊢ Membership.mem (α := α) c.support ((g : (a : α) → α) a : α) ↔ a ∈ c.support

Tactic:
mem_support_iff_of_commute (self_mem_cycle_factors_commute hc).symm a

Premises used: Equiv.Perm.mem_support_iff_of_commute, Equiv.Perm.self_mem_cycle_factors_commute, Commute.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
intro : ∀ (val : Fintype β), P σ
⊢ P σ

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
this : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
x : { l : List (Perm β) // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l } := σ.truncCycleFactors.out
⊢ P σ

Tactic:
(congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)

Premises used: Eq.mp, congr_arg, And.right, And.left, Subtype.val, Subtype.property