awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ ∀ (i : ↥g.cycleFactorsFinset),
    Function.Injective.{u_1 + 1, u_1 + 1} (α :=
      ↥((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i)) (β := Perm α)
      (⇑(Subgroup.subtype ((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i)) :
        (a : ↥((fun (c : ↥g.cycleFactorsFinset) ↦ zpowers (↑c : Perm α)) i)) → Perm α)

Tactic:
exact fun i ↦ subtype_injective _

Premises used: Subgroup.subtype_injective
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_2 :
  _root_.Disjoint (α := Subgroup (Perm α))
    (closure
      (↑(MonoidHom.range (G :=
            Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x })
            (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x))) :
        Set (Perm α)))
    (⨆ (i : ↥g.cycleFactorsFinset), zpowers (↑i : Perm α))
⊢ _root_.Disjoint
    (MonoidHom.range (G := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
      (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)))
    (MonoidHom.range (G := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (noncommPiCoprod ⋯))

Tactic:
rw [noncommPiCoprod_range, ← ofSubtype.range.closure_eq]

Premises used: Subgroup.closure_eq, MonoidHom.range, Equiv.Perm.ofSubtype, Subgroup.noncommPiCoprod_range
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_2 :
  _root_.Disjoint (α := Subgroup (Perm α))
    (closure
      (↑(MonoidHom.range (G :=
            Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x })
            (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x))) :
        Set (Perm α)))
    (closure (⋃ (i : ↥g.cycleFactorsFinset), {(↑i : Perm α)}))
⊢ _root_.Disjoint (α := Subgroup (Perm α))
    (closure
      (↑(MonoidHom.range (G :=
            Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x })
            (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x))) :
        Set (Perm α)))
    (⨆ (i : ↥g.cycleFactorsFinset), zpowers (↑i : Perm α))

Tactic:
simp only [zpowers_eq_closure, ← closure_iUnion]

Premises used: Subgroup.closure_iUnion, Subgroup.zpowers_eq_closure
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_2 :
  ∀
    a ∈
      (↑(MonoidHom.range (G :=
            Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x })
            (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x))) :
        Set (Perm α)),
    ∀ (b : Perm α),
      Membership.mem (γ := Set (Perm α)) (⋃ (i : ↥g.cycleFactorsFinset), {(↑i : Perm α)}) b →
        _root_.Disjoint a.support b.support
⊢ _root_.Disjoint (α := Subgroup (Perm α))
    (closure
      (↑(MonoidHom.range (G :=
            Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x })
            (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x))) :
        Set (Perm α)))
    (closure (⋃ (i : ↥g.cycleFactorsFinset), {(↑i : Perm α)}))

Tactic:
apply disjoint_closure_of_disjoint_support

Premises used: Equiv.Perm.disjoint_closure_of_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x }
b : ↥g.cycleFactorsFinset
⊢ _root_.Disjoint
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
        a))
    (↑b : Perm α).support

Tactic:
(ofSubtype_support_disjoint a).mono_right (mem_cycleFactorsFinset_support_le b.2)

Premises used: Equiv.Perm.ofSubtype_support_disjoint, Equiv.Perm.mem_cycleFactorsFinset_support_le, Disjoint.mono_right, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm { x : α // Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x }
b : ↥g.cycleFactorsFinset
⊢ _root_.Disjoint
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
        a))
    (↑b : Perm α).support

Tactic:
exact (ofSubtype_support_disjoint a).mono_right (mem_cycleFactorsFinset_support_le b.2)

Premises used: Equiv.Perm.ofSubtype_support_disjoint, Equiv.Perm.mem_cycleFactorsFinset_support_le, Disjoint.mono_right, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a :
  MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g) ≤
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
a₁ :
  map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ≤
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g)
⊢ MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g) =
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a :
  MonoidHom.range (G := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
        (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) ≤
      map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ∧
    ∀ (i : ↥g.cycleFactorsFinset),
      zpowers (↑i : Perm α) ≤
        map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
⊢ MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g) ≤
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_range, sup_le_iff, noncommPiCoprod_range, iSup_le_iff]

Premises used: MonoidHom.noncommCoprod_range, sup_le_iff, Equiv.Perm.OnCycleFactors.kerParam, iSup_le_iff, Subgroup.noncommPiCoprod_range
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a :
  MonoidHom.range (G := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
        (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) ≤
      map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ∧
    ∀ (i : ↥g.cycleFactorsFinset),
      (↑i : Perm α) ∈
        map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
⊢ MonoidHom.range (G := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
        (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) ≤
      map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ∧
    ∀ (i : ↥g.cycleFactorsFinset),
      zpowers (↑i : Perm α) ≤
        map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))

Tactic:
simp only [zpowers_le]

Premises used: Subgroup.zpowers_le
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a :
  MonoidHom.range (G := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
      (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) ≤
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
a₁ :
  ∀ (i : ↥g.cycleFactorsFinset),
    (↑i : Perm α) ∈
      map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
⊢ MonoidHom.range (G := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
        (ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) ≤
      map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ∧
    ∀ (i : ↥g.cycleFactorsFinset),
      (↑i : Perm α) ∈
        map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ Membership.mem (α := Perm α)
    (map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)))
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → Perm α)
        a :
      Perm α)

Tactic:
⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Equiv.Perm.ofSubtype, And.intro, Exists.intro, Set.image, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
a₁ :
  Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (centralizer {g})
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
        a :
      Perm α)
a₂ :
  Membership.mem (α := ↥(centralizer {g}))
    (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a)
        ⋯ :
      ↥(centralizer {g}))
⊢ Membership.mem (α := Perm α)
    (map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)))
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → Perm α)
        a :
      Perm α)

Tactic:
refine ⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
a₁ :
  HMul.hMul (α := Perm α)
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a :
        Perm α)
      g =
    HMul.hMul (β := Perm α) g
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a :
        Perm α)
⊢ Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (centralizer {g})
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
        a :
      Perm α)

Tactic:
rw [mem_centralizer_singleton_iff]

Premises used: Subgroup.mem_centralizer_singleton_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ HMul.hMul (α := Perm α)
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a :
        Perm α)
      g =
    HMul.hMul (β := Perm α) g
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a :
        Perm α)

Tactic:
Disjoint.commute (disjoint_iff_disjoint_support.mpr (ofSubtype_support_disjoint a))

Premises used: Iff.mpr, Equiv.Perm.Disjoint.commute, SemiconjBy, Commute, Equiv.Perm.ofSubtype_support_disjoint, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ HMul.hMul (α := Perm α)
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a :
        Perm α)
      g =
    HMul.hMul (β := Perm α) g
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a :
        Perm α)

Tactic:
exact Disjoint.commute (disjoint_iff_disjoint_support.mpr (ofSubtype_support_disjoint a))

Premises used: Iff.mpr, Equiv.Perm.Disjoint.commute, Equiv.Perm.ofSubtype_support_disjoint, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ Membership.mem (α := ↥(centralizer {g}))
    (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a)
        ⋯ :
      ↥(centralizer {g}))

Tactic:
Perm.ext fun x ↦ Subtype.ext (disjoint_iff_disjoint_support.mpr
          ((ofSubtype_support_disjoint a).mono_right
            (mem_cycleFactorsFinset_support_le x.2))).commute.mul_inv_cancel

Premises used: Iff.mpr, Equiv.Perm.Disjoint.commute, Set.Mem, setOf, Set.preimage, Commute.mul_inv_cancel, Set.singleton, Equiv.Perm.ofSubtype_support_disjoint, Equiv.Perm.mem_cycleFactorsFinset_support_le, Equiv.Perm.disjoint_iff_disjoint_support, Disjoint.mono_right, Equiv.Perm.ext, Subtype.property, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ Membership.mem (α := ↥(centralizer {g}))
    (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          a)
        ⋯ :
      ↥(centralizer {g}))

Tactic:
exact Perm.ext fun x ↦ Subtype.ext (disjoint_iff_disjoint_support.mpr
          ((ofSubtype_support_disjoint a).mono_right
            (mem_cycleFactorsFinset_support_le x.2))).commute.mul_inv_cancel

Premises used: Equiv.Perm.ext, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
i : ↥g.cycleFactorsFinset
⊢ (↑i : Perm α) ∈
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))

Tactic:
⟨⟨i, mem_centralizer_singleton_iff.mpr (self_mem_cycle_factors_commute i.2)⟩, ?_, rfl⟩

Premises used: Iff.mpr, Set.Mem, setOf, Equiv.Perm.self_mem_cycle_factors_commute, Subgroup.mem_centralizer_singleton_iff, Subtype.mk, And.intro, Exists.intro, Set.image, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
i : ↥g.cycleFactorsFinset
a :
  Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x) (↑i : Perm α) ⋯ ∈
    (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
⊢ (↑i : Perm α) ∈
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))

Tactic:
refine ⟨⟨i, mem_centralizer_singleton_iff.mpr (self_mem_cycle_factors_commute i.2)⟩, ?_, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
i : ↥g.cycleFactorsFinset
⊢ Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x) (↑i : Perm α) ⋯ ∈
    (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))

Tactic:
Perm.ext fun x ↦ Subtype.ext (cycleFactorsFinset_mem_commute' g i.2 x.2).mul_inv_cancel

Premises used: Set.Mem, setOf, Set.preimage, Commute.mul_inv_cancel, Set.singleton, Equiv.Perm.cycleFactorsFinset_mem_commute', Equiv.Perm.ext, Subtype.property, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
i : ↥g.cycleFactorsFinset
⊢ Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x) (↑i : Perm α) ⋯ ∈
    (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))

Tactic:
exact Perm.ext fun x ↦ Subtype.ext (cycleFactorsFinset_mem_commute' g i.2 x.2).mul_inv_cancel

Premises used: Equiv.Perm.ext, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
a :
  (↑p : Perm α) ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g)
⊢ Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g))
    ((Subgroup.subtype (centralizer {g}) : (a : ↥(centralizer {g})) → Perm α) p : Perm α)

Tactic:
simp only [coe_subtype]

Premises used: Subgroup.coe_subtype
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
⊢ ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)

Tactic:
simp only [SetLike.mem_coe, mem_ker_toPermHom_iff, IsCycle.forall_commute_iff] at hp

Premises used: Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff, SetLike.mem_coe, Equiv.Perm.IsCycle.forall_commute_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
h :
  (kerParam g :
        (a :
            Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
              ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
          Perm α)
      (u, v) =
    (↑p : Perm α)
⊢ (↑p : Perm α) ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g)

Tactic:
use (u, v)

Premises used: Prod.mk