awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha2 :
  Membership.mem (α := α) (↑((u, v).2 a) : Perm α).support
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
ha1 : ¬(↑a : Perm α) = g.cycleOf x
⊢ (↑a : Perm α).Disjoint (g.cycleOf x)

Tactic:
have key := cycleFactorsFinset_pairwise_disjoint g a.2 hx ha1
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha2 :
  Membership.mem (α := α) (↑((u, v).2 a) : Perm α).support
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
ha1 : ¬(↑a : Perm α) = g.cycleOf x
key : (↑a : Perm α).Disjoint (g.cycleOf x)
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a : Perm α).support → a_1 ∉ (g.cycleOf x).support

Tactic:
rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at key

Premises used: Finset.disjoint_left, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha2 :
  Membership.mem (α := α) (↑((u, v).2 a) : Perm α).support
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
ha1 : ¬(↑a : Perm α) = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a : Perm α).support → a_1 ∉ (g.cycleOf x).support
pos :
  ∀ (k : ℤ) (hk : (↑a : Perm α) ^ k = (↑(v a) : Perm α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x

Tactic:
obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v a).2

Premises used: Iff.mp, Subgroup.mem_zpowers_iff, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha2 :
  Membership.mem (α := α) (↑((u, v).2 a) : Perm α).support
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
ha1 : ¬(↑a : Perm α) = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a : Perm α).support → a_1 ∉ (g.cycleOf x).support
k : ℤ
hk : (↑a : Perm α) ^ k = (↑(v a) : Perm α)
⊢ (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α) ∉
    (g.cycleOf x).support

Tactic:
replace ha2 := key (support_zpow_le a.1 k (hk ▸ ha2))
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha1 : ¬(↑a : Perm α) = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a : Perm α).support → a_1 ∉ (g.cycleOf x).support
k : ℤ
hk : (↑a : Perm α) ^ k = (↑(v a) : Perm α)
ha2 :
  (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α) ∉
    (g.cycleOf x).support
pos :
  ∀ (k : ℤ)
    (hk :
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k =
        (↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x

Tactic:
obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v ⟨g.cycleOf x, hx⟩).2

Premises used: Subtype.mk, Iff.mp, Subgroup.mem_zpowers_iff, Subtype.property, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha1 : ¬(↑a : Perm α) = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a : Perm α).support → a_1 ∉ (g.cycleOf x).support
k_1 : ℤ
hk_1 : (↑a : Perm α) ^ k_1 = (↑(v a) : Perm α)
ha2 :
  (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α) ∉
    (g.cycleOf x).support
k : ℤ
hk :
  (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k =
    (↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α)
pos :
  ∀
    (ha2 :
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k : (a : α) → α)
            x :
          α) ∉
        (g.cycleOf x).support)
    (hk :
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k =
        (↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
pos₁ :
  ∀ (ha2 : x ∉ (g.cycleOf x).support)
    (hk :
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k =
        (↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
pos₂ :
  ∀ (ha2 : (g.cycleOf x : (a : α) → α) x = x)
    (hk :
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k =
        (↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
pos₃ pos₄ pos₅ pos₆ :
  ∀ (ha2 : (g : (a : α) → α) x = x)
    (hk :
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α) ^ k =
        (↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x

Tactic:
rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.zpow_apply_mem_support, Equiv.Perm.cycleOf_apply_self
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ x ∉ g.support

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff] at hx

Premises used: Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : x ∉ g.support
neg : x ∉ support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq,
      ← notMem_support]

Premises used: Equiv.Perm.notMem_support, MonoidHom.noncommCoprod_apply, Equiv.Perm.OnCycleFactors.kerParam, Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : x ∉ g.support
neg :
  ∀
    (hx :
      Membership.mem (γ := Finset α)
        (support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2))
        x),
    x ∈ g.support
⊢ x ∉ support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)

Tactic:
contrapose hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx :
  Membership.mem (γ := Finset α)
    (support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)) x
neg : ∀ (a : ↥g.cycleFactorsFinset) (ha : x ∈ (↑(v a) : Perm α).support), x ∈ g.support
⊢ x ∈ g.support

Tactic:
obtain ⟨a, -, ha⟩ := mem_support_of_mem_noncommProd_support
      (comm := fun a ha b hb h ↦ g.pairwise_commute_of_mem_zpowers h (v a) (v b) (v a).2 (v b).2) hx

Premises used: Equiv.Perm.mem_support_of_mem_noncommProd_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx :
  Membership.mem (γ := Finset α)
    (support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)) x
a : ↥g.cycleFactorsFinset
ha : x ∈ (↑(v a) : Perm α).support
⊢ x ∈ g.support

Tactic:
support_zpowers_of_mem_cycleFactorsFinset_le (v a) ha

Premises used: Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx :
  Membership.mem (γ := Finset α)
    (support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)) x
a : ↥g.cycleFactorsFinset
ha : x ∈ (↑(v a) : Perm α).support
⊢ x ∈ g.support

Tactic:
exact support_zpowers_of_mem_cycleFactorsFinset_le (v a) ha

Premises used: Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) (β :=
      Perm α)
      (⇑(ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) :
        (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → Perm α) ∧
    Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
        (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → 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 ⋯))
⊢ Function.Injective (α :=
    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
    (β := Perm α)
    (⇑(kerParam g) :
      (a :
          Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
            ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
        Perm α)

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_injective]

Premises used: Equiv.Perm.OnCycleFactors.kerParam, MonoidHom.noncommCoprod_injective
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) (β :=
      Perm α)
      (⇑(ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) :
        (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → Perm α) ∧
    Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
        (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → 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:
⟨ofSubtype_injective, ?_, ?_⟩

Premises used: And.intro, Equiv.Perm.ofSubtype_injective
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_1 :
  Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
    (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α)
refine_2 :
  _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 ⋯))
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) (β :=
      Perm α)
      (⇑(ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)) :
        (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → Perm α) ∧
    Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
        (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → 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:
refine ⟨ofSubtype_injective, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_1 :
  iSupIndep (α := Subgroup (Perm α)) fun (i : ↥g.cycleFactorsFinset) ↦
    MonoidHom.range (G := ↥((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i))
      (Subgroup.subtype ((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i))
refine_1₁ :
  ∀ (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 α)
⊢ Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
    (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α)

Tactic:
apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep

Premises used: MonoidHom.injective_noncommPiCoprod_of_iSupIndep
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
refine_1 :
  _root_.Disjoint (α := Subgroup (Perm α)) (zpowers (↑a : Perm α))
    (⨆ (j : ↥g.cycleFactorsFinset), ⨆ (_ : ¬j = a), zpowers (↑j : Perm α))
⊢ _root_.Disjoint.{u_1} (α := Subgroup (Perm α))
    ((fun (i : ↥g.cycleFactorsFinset) ↦
        (MonoidHom.range (G := ↥((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i))
            (Subgroup.subtype ((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i)) :
          Subgroup (Perm α)))
      a)
    (⨆ (j : ↥g.cycleFactorsFinset),
      ⨆ (_ : j ≠ a),
        (fun (i : ↥g.cycleFactorsFinset) ↦
            (MonoidHom.range (G := ↥((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i))
                (Subgroup.subtype ((fun (c : ↥g.cycleFactorsFinset) ↦ (zpowers (↑c : Perm α) : Subgroup (Perm α))) i)) :
              Subgroup (Perm α)))
          j)

Tactic:
simp only [range_subtype, ne_eq]

Premises used: ne_eq, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
refine_1 :
  _root_.Disjoint (α := Subgroup (Perm α)) (closure {(↑a : Perm α)})
    (closure (⋃ (i : ↥g.cycleFactorsFinset), ⋃ (_ : ¬i = a), {(↑i : Perm α)}))
⊢ _root_.Disjoint (α := Subgroup (Perm α)) (zpowers (↑a : Perm α))
    (⨆ (j : ↥g.cycleFactorsFinset), ⨆ (_ : ¬j = a), zpowers (↑j : 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 α
a : ↥g.cycleFactorsFinset
refine_1 :
  ∀ (a_1 : Perm α),
    Membership.mem (γ := Set (Perm α)) {(↑a : Perm α)} a_1 →
      ∀ (b : Perm α),
        Membership.mem (γ := Set (Perm α)) (⋃ (i : ↥g.cycleFactorsFinset), ⋃ (_ : ¬i = a), {(↑i : Perm α)}) b →
          _root_.Disjoint a_1.support b.support
⊢ _root_.Disjoint (α := Subgroup (Perm α)) (closure {(↑a : Perm α)})
    (closure (⋃ (i : ↥g.cycleFactorsFinset), ⋃ (_ : ¬i = a), {(↑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 b : ↥g.cycleFactorsFinset
h : ¬b = a
refine_1 : (↑a : Perm α).Disjoint (↑b : Perm α)
⊢ _root_.Disjoint (↑a : Perm α).support (↑b : Perm α).support

Tactic:
rw [← disjoint_iff_disjoint_support]

Premises used: Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
refine_1 : (↑a : Perm α) ≠ (↑b : Perm α)
⊢ (↑a : Perm α).Disjoint (↑b : Perm α)

Tactic:
apply cycleFactorsFinset_pairwise_disjoint g a.2 b.2

Premises used: Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
refine_1 : ¬a = b
⊢ (↑a : Perm α) ≠ (↑b : Perm α)

Tactic:
simp only [ne_eq, ← Subtype.ext_iff]

Premises used: ne_eq, Subtype.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ ¬a = b

Tactic:
ne_comm.mp h

Premises used: Iff.mp, ne_comm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ ¬a = b

Tactic:
exact ne_comm.mp h

Premises used: Iff.mp, ne_comm
-- 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:
fun i ↦ subtype_injective _

Premises used: Subgroup.subtype_injective, Subgroup.zpowers, Subtype.val