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 : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
        x :
      α)
have pos : (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
      x :
    α) ∉
  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 α)) sorry)
Tactic: rw [kerParam, MonoidHom.noncommCoprod_apply', mul_apply, ofSubtype_apply_of_not_mem u hx',
      noncommPiCoprod_apply, ← Finset.noncommProd_erase_mul _ (Finset.mem_univ ⟨g.cycleOf x, hx⟩),
      mul_apply, ← 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 : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
⊢ (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α) ∉
    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 α)) ⋯)
have pos : ∀
  (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 α)) sorry))
      (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
            (a : α) → α)
          x :
        α)),
  Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
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 : 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 :
      α)
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have pos : ∀ (a : ↥g.cycleFactorsFinset)
  (ha1 : a ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx))
  (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 :
        α)),
  Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
Tactic: obtain ⟨a, ha1, ha2⟩ := mem_support_of_mem_noncommProd_support hx'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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 ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)
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 :
      α)
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have ha1₁ : ¬(↑a : Perm α) = g.cycleOf x
Tactic: simp only [Finset.mem_erase, Finset.mem_univ, and_true, Ne, Subtype.ext_iff] at ha1
Cleared hypotheses: ha1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have key : (↑a : Perm α).Disjoint (g.cycleOf x)
Tactic: have key := cycleFactorsFinset_pairwise_disjoint g a.2 hx ha1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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)
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have key₁ : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a : Perm α).support → a_1 ∉ (g.cycleOf x).support
Tactic: rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at key
Cleared hypotheses: key
-- 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 : 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
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have pos : ∀ (k : ℤ) (hk : (↑a : Perm α) ^ k = (↑(v a) : Perm α)),
  Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
Tactic: obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v a).2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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 α)
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have ha2₁ : (((↑((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))
Cleared hypotheses: ha2
-- 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 : 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
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have 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
Tactic: obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v ⟨g.cycleOf x, hx⟩).2
-- 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 : 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 α)
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have 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
Tactic: rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2
Cleared hypotheses: ha2, hk
-- 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 : 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
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have 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
Tactic: rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2
Cleared hypotheses: ha2, hk
-- 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 : 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
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have 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
Tactic: rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2
Cleared hypotheses: ha2, hk
-- 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 : 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
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
have 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
Tactic: rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2
Cleared hypotheses: ha2, hk
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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
⊢ 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 hx₁ : x ∉ g.support
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff] at hx
Cleared hypotheses: hx