awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ 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 :
      α)
have neg : x ∉ support ((noncommPiCoprod sorry : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)
Tactic: rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq,
      ← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ x ∉ support ((noncommPiCoprod ⋯ : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2)
have neg : ∀
  (hx :
    Membership.mem (γ := Finset α)
      (support ((noncommPiCoprod sorry : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α) (u, v).2))
      x),
  x ∈ g.support
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ x ∈ g.support
have neg : ∀ (a : ↥g.cycleFactorsFinset) (ha : x ∈ (↑(v a) : Perm α).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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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 α)
have 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 sorry) : (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 sorry))
Tactic: rw [kerParam, MonoidHom.noncommCoprod_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 ⋯))
have refine_1 : Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
  (⇑(noncommPiCoprod sorry) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α)
Tactic: refine ⟨ofSubtype_injective, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 α)
⊢ 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 ⋯))
have 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 sorry))
Tactic: refine ⟨ofSubtype_injective, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
    (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α)
have 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))
Tactic: apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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))
⊢ Function.Injective (α := (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) (β := Perm α)
    (⇑(noncommPiCoprod ⋯) : (a : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))) → Perm α)
have 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 α)
Tactic: apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
⊢ _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)
have refine_1 : _root_.Disjoint (α := Subgroup (Perm α)) (zpowers (↑a : Perm α))
  (⨆ (j : ↥g.cycleFactorsFinset), ⨆ (_ : ¬j = a), zpowers (↑j : Perm α))
Tactic: simp only [range_subtype, ne_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
⊢ _root_.Disjoint (α := Subgroup (Perm α)) (zpowers (↑a : Perm α))
    (⨆ (j : ↥g.cycleFactorsFinset), ⨆ (_ : ¬j = a), zpowers (↑j : Perm α))
have refine_1 : _root_.Disjoint (α := Subgroup (Perm α)) (closure {(↑a : Perm α)})
  (closure (⋃ (i : ↥g.cycleFactorsFinset), ⋃ (_ : ¬i = a), {(↑i : Perm α)}))
Tactic: simp only [zpowers_eq_closure, ← closure_iUnion]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
⊢ _root_.Disjoint (α := Subgroup (Perm α)) (closure {(↑a : Perm α)})
    (closure (⋃ (i : ↥g.cycleFactorsFinset), ⋃ (_ : ¬i = a), {(↑i : Perm α)}))
have 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
Tactic: apply disjoint_closure_of_disjoint_support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ _root_.Disjoint (↑a : Perm α).support (↑b : Perm α).support
have refine_1 : (↑a : Perm α).Disjoint (↑b : Perm α)
Tactic: rw [← disjoint_iff_disjoint_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ (↑a : Perm α).Disjoint (↑b : Perm α)
have refine_1 : (↑a : Perm α) ≠ (↑b : Perm α)
Tactic: apply cycleFactorsFinset_pairwise_disjoint g a.2 b.2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ (↑a : Perm α) ≠ (↑b : Perm α)
have refine_1 : ¬a = b
Tactic: simp only [ne_eq, ← Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : 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 ⋯))
have 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 α))
Tactic: rw [noncommPiCoprod_range, ← ofSubtype.range.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : 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 α))
have 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 α)}))
Tactic: simp only [zpowers_eq_closure, ← closure_iUnion]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : 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 α)))
    (closure (⋃ (i : ↥g.cycleFactorsFinset), {(↑i : Perm α)}))
have 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
Tactic: apply disjoint_closure_of_disjoint_support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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))
⊢ 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))
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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))
have 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))
Tactic: rw [kerParam, MonoidHom.noncommCoprod_range, sup_le_iff, noncommPiCoprod_range, iSup_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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))
have 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))
Tactic: simp only [zpowers_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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))
⊢ 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))
have a₁ : ∀ (i : ↥g.cycleFactorsFinset),
  (↑i : Perm α) ∈
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 α)
have 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 α)
Tactic: refine ⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 α)
⊢ 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 α)
have 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)
      sorry :
    ↥(centralizer {g}))
Tactic: refine ⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ 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 α)
have 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 α)
Tactic: rw [mem_centralizer_singleton_iff]