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 α
i : ↥g.cycleFactorsFinset
⊢ (↑i : Perm α) ∈
    map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g))
have a : Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x) (↑i : Perm α) sorry ∈
  (↑(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) : Set ↥(centralizer {g}))
Tactic: refine ⟨⟨i, mem_centralizer_singleton_iff.mpr (self_mem_cycle_factors_commute i.2)⟩, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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}))
⊢ 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 α)
have a : (↑p : Perm α) ∈
  MonoidHom.range (G :=
    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
    (kerParam g)
Tactic: simp only [coe_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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 : α) → α))) ⋯
⊢ (↑p : Perm α) ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g)
have 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 α)
Tactic: simp only [SetLike.mem_coe, mem_ker_toPermHom_iff, IsCycle.forall_commute_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
⊢ (↑p : Perm α) ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g)
have h : (kerParam g :
      (a :
          Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
            ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
        Perm α)
    (u, v) =
  (↑p : Perm α)
Tactic: use (u, v)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
⊢ (kerParam g :
        (a :
            Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
              ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
          Perm α)
      (u, v) =
    (↑p : Perm α)
have h : ∀ (x : α),
  Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have h : Eq (α := α)
  (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
      ((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α) x
    else
      (((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 :
    α)
  (((↑p : Perm α) : (a : α) → α) x : α)
Tactic: rw [kerParam_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
⊢ Eq (α := α)
    (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
        ((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x
      else
        (((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 :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have pos : ∀ (hx : g.cycleOf x ∈ g.cycleFactorsFinset),
  Eq (α := α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
pos :
  ∀ (hx : g.cycleOf x ∈ g.cycleFactorsFinset),
    Eq (α := α)
      (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x :
        α)
      (((↑p : Perm α) : (a : α) → α) x : α)
⊢ Eq (α := α)
    (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
        ((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x
      else
        (((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 :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have neg : ∀ (hx : g.cycleOf x ∉ g.cycleFactorsFinset),
  Eq (α := α)
    ((((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 :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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) ⋯))
      ⋯
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ Eq (α := α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have hx₁ : (g : (a : α) → α) x ≠ x
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support] at hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
hx_1 : g.cycleOf x ∈ g.cycleFactorsFinset
hx : (g : (a : α) → α) x ≠ x
⊢ Eq (α := α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1)) : Perm α) : (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have pos : x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α).support
Tactic: rw [ofSubtype_apply_of_mem, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
hx_1 : g.cycleOf x ∈ g.cycleFactorsFinset
hx : (g : (a : α) → α) x ≠ x
⊢ x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α).support
have pos : ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α) : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, cycleOf_apply_self, ne_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
hx_1 : g.cycleOf x ∈ g.cycleFactorsFinset
hx : (g : (a : α) → α) x ≠ x
pos :
  ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α) : (a : α) → α) x ≠ x
pos₁ : (g : (a : α) → α) x ≠ x
⊢ x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α).support
have pos₂ : ¬(g : (a : α) → α) x = x
Tactic: rwa [mem_support, cycleOf_apply_self, ne_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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) ⋯))
      ⋯
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ Eq (α := α)
    ((((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 :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have hx₁ : (g : (a : α) → α) x = x
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, notMem_support] at 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 α
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) ⋯))
      ⋯
x : α
hx : (g : (a : α) → α) x = x
⊢ Eq (α := α)
    ((((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 :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have neg : Eq (α := α)
  ((↑((u :
            (a : { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) →
              { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) })
          (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) x
            hx)) :
      α) :
    α)
  (((↑p : Perm α) : (a : α) → α) x : α)
Tactic: rwa [ofSubtype_apply_of_mem, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) ⋯))
      ⋯
x : α
hx : (g : (a : α) → α) x = x
neg :
  Eq (α := α)
    ((↑((u :
              (a : { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) →
                { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) })
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) x
              hx)) :
        α) :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((((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 :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
have neg₁ : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
Tactic: rwa [ofSubtype_apply_of_mem, subtypePerm_apply]