awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
refine_3 : ∀ (hx : (σ : (a : α) → α) x = x), (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
refine_3₁ : ∀ (hx : (τ : (a : α) → α) x = x), (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
rcases hd x with hx | hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
exact Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
refine_3 : (τ * f⁻¹ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
pos : ∀ (hfx : (f : (a : α) → α) x = x), (τ * f⁻¹ : (a : α) → α) x = x
neg : ∀ (hfx : ¬(f : (a : α) → α) x = x), (τ * f⁻¹ : (a : α) → α) x = x
⊢ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
by_cases hfx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : (f : (a : α) → α) x = x
pos : Eq (α := α) ((τ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
rw [← hfx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : (f : (a : α) → α) x = x
⊢ Eq (α := α) ((τ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)

Tactic:
simpa [hx] using hfx.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
neg : (τ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
⊢ (τ * f⁻¹ : (a : α) → α) x = x

Tactic:
rw [mul_apply]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (f : (a : α) → α) x = x

Tactic:
rw [← hf.right _ (mem_support.mpr hfx)] at hx

Premises used: Iff.mpr, Equiv.Perm.mem_support, And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
hx₁ : (f : (a : α) → α) x = x
⊢ ¬(f : (a : α) → α) x = x

Tactic:
rw [← hf.right _ (mem_support.mpr hfx)] at hx

Premises used: Iff.mpr, Equiv.Perm.mem_support, And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (f : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (τ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ f ∉ σ.cycleFactorsFinset

Tactic:
fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))

Premises used: Disjoint.le_bot, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, Finset.notMem_empty, Finset.mem_inter_of_mem, Not
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ f ∉ σ.cycleFactorsFinset

Tactic:
exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))

Premises used: Disjoint.le_bot, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, Finset.notMem_empty, Finset.mem_inter_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g z : Perm α
h :
  ∀ (a : Perm α),
    a ∈ g.cycleFactorsFinset → Commute z a ↔
      a ∈ g.cycleFactorsFinset →
        ∃ (hc : ∀ (x : α), Membership.mem (α := α) a.support ((z : (a : α) → α) x : α) ↔ x ∈ a.support),
          Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers a)
            ((ofSubtype (p := fun (x : α) ↦ x ∈ a.support) : (a : Perm ↥a.support) → Perm α)
                (z.subtypePerm (p := Membership.mem a.support) hc) :
              Perm α)
⊢ (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
    ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
        Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
              (z.subtypePerm (p := Membership.mem c.support) hc) :
            Perm α)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g z c : Perm α
h :
  c ∈ g.cycleFactorsFinset →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
        Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
              (z.subtypePerm (p := Membership.mem c.support) hc) :
            Perm α))
⊢ c ∈ g.cycleFactorsFinset → Commute z c ↔
    c ∈ g.cycleFactorsFinset →
      ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
        Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
              (z.subtypePerm (p := Membership.mem c.support) hc) :
            Perm α)

Tactic:
apply imp_congr_right

Premises used: imp_congr_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g z c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute z c ↔
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            (z.subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)

Tactic:
IsCycle.commute_iff (mem_cycleFactorsFinset_iff.mp hc).1

Premises used: And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp, Equiv.Perm.IsCycle.commute_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g z c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute z c ↔
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            (z.subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)

Tactic:
exact IsCycle.commute_iff (mem_cycleFactorsFinset_iff.mp hc).1

Premises used: And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp, Equiv.Perm.IsCycle.commute_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
H :
  ∀ (x : α) (hx : x ∈ c.support),
    Eq.{u_2 + 1} (α := α)
      (↑((g.subtypePerm (p := Membership.mem c.support) ⋯ : (a : ↥c.support) → ↥c.support)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
        α)
      (↑((c.subtypePermOfSupport : (a : ↥c.support) → ↥c.support)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
        α)
⊢ g.subtypePerm (p := Membership.mem c.support) ⋯ = c.subtypePermOfSupport

Tactic:
ext ⟨x, hx⟩
-- 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
H : Eq (α := α) ((g : (a : α) → α) x : α) ((c : (a : α) → α) x : α)
⊢ Eq.{u_2 + 1} (α := α)
    (↑((g.subtypePerm (p := Membership.mem c.support) ⋯ : (a : ↥c.support) → ↥c.support)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)
    (↑((c.subtypePermOfSupport : (a : ↥c.support) → ↥c.support) (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)

Tactic:
simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]

Premises used: Subtype.coe_mk, Equiv.Perm.subtypePermOfSupport, Equiv.Perm.subtypePerm_apply
-- 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
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((c : (a : α) → α) x : α)

Tactic:
((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm

Premises used: And.right, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp, Eq.symm
-- 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
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((c : (a : α) → α) x : α)

Tactic:
exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm

Premises used: And.right, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
rw :
  (∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (k.subtypePerm (p := Membership.mem c.support) hc')) ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support))
        (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) ⋯))
        (k.subtypePerm (p := Membership.mem c.support) hc')
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support))
        (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) ⋯))
        (k.subtypePerm (p := Membership.mem c.support) hc')

Tactic:
rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]

Premises used: Equiv.Perm.IsCycle.commute_iff', 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 k c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  ∀ (a : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (k.subtypePerm (p := Membership.mem c.support) a) ↔
      Membership.mem (γ := Subgroup (Perm ↥c.support))
        (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) ⋯))
        (k.subtypePerm (p := Membership.mem c.support) a)
⊢ (∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (k.subtypePerm (p := Membership.mem c.support) hc')) ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support))
        (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) ⋯))
        (k.subtypePerm (p := Membership.mem c.support) hc')

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support
h :
  ∀ (a : ℤ),
    HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport a = k.subtypePerm (p := Membership.mem c.support) hc' ↔
      g.subtypePerm (p := Membership.mem c.support) ⋯ ^ a = k.subtypePerm (p := Membership.mem c.support) hc'
⊢ (∃ (k_1 : ℤ),
      HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k_1 = k.subtypePerm (p := Membership.mem c.support) hc') ↔
    ∃ (k_1 : ℤ),
      g.subtypePerm (p := Membership.mem c.support) ⋯ ^ k_1 = k.subtypePerm (p := Membership.mem c.support) hc'

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support
n : ℤ
h h₁ :
  HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport n = k.subtypePerm (p := Membership.mem c.support) hc' ↔
    HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport n = k.subtypePerm (p := Membership.mem c.support) hc'
⊢ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport n = k.subtypePerm (p := Membership.mem c.support) hc' ↔
    g.subtypePerm (p := Membership.mem c.support) ⋯ ^ n = k.subtypePerm (p := Membership.mem c.support) hc'

Tactic:
rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]

Premises used: Equiv.Perm.subtypePerm_on_cycleFactorsFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
apply : n < c.sum
⊢ n < Fintype.card α

Tactic:
apply lt_of_lt_of_le _ hc

Premises used: lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
rw : ∃ s ∈ c.ranges, n ∈ s
⊢ n < c.sum

Tactic:
rw [← mem_mem_ranges_iff_lt_sum]

Premises used: List.mem_mem_ranges_iff_lt_sum
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ ∃ s ∈ c.ranges, n ∈ s

Tactic:
⟨l, hl, hn⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ ∃ s ∈ c.ranges, n ∈ s

Tactic:
exact ⟨l, hl, hn⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
⊢ ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α

Tactic:
have hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α := by
    intro l hl n hn
    apply lt_of_lt_of_le _ hc
    rw [← mem_mem_ranges_iff_lt_sum]
    exact ⟨l, hl, hn⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
a : List ℕ
ha : a ∈ c.ranges
rw : map id a
| a

Tactic:
rw [← List.map_id a]

Premises used: List.map_id
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
a : List ℕ
ha : a ∈ c.ranges
conv_rhs : map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = map id a
⊢ map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a

Tactic:
conv_rhs => rw [← List.map_id a]

Premises used: List.map_id