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 α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∉ g.support
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d : Perm α).support
⊢ False
have inl : x ∈ g.support
Tactic: apply hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      (a.ofPermHomFun τ x) ↔
    x ∈ (↑c : Perm α).support
have inr : Membership.mem (α := α) (γ := Finset α)
    (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
    ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
              ↥g.cycleFactorsFinset) :
          α) :
      α) ↔
  x ∈ (↑c : Perm α).support
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a τ hd hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((g ^ m : (a : α) → α)
          ((a : (a : ↥g.cycleFactorsFinset) → α)
              (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
                ↥g.cycleFactorsFinset) :
            α) :
        α) ↔
    x ∈ (↑c : Perm α).support
have inr : Membership.mem (α := α) (γ := Finset α)
    (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
    ((a : (a : ↥g.cycleFactorsFinset) → α)
        (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
          ↥g.cycleFactorsFinset) :
      α) ↔
  x ∈ (↑c : Perm α).support
Tactic: rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
have pos : ∀ (h : c = d),
  Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
Tactic: by_cases h : c = d
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
pos :
  ∀ (h : c = d),
    Membership.mem (α := α) (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
              ↥g.cycleFactorsFinset) :
          α) ↔
      x ∈ (↑c : Perm α).support
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
have neg : ∀ (h : ¬c = d),
  Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
Tactic: by_cases h : c = d
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
have H : (↑c : Perm α).Disjoint (↑d : Perm α)
Tactic: have H : Disjoint c.val d.val :=
        cycleFactorsFinset_pairwise_disjoint g c.prop d.prop (Subtype.coe_ne_coe.mpr h)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
h' :
  Eq.{u_1 + 1} (α := Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
⊢ False
have apply : c = d
Tactic: apply h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
have H' : Disjoint.{u_1} (α := α)
  (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
  (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
Tactic: have H' : Disjoint ((τ : Perm g.cycleFactorsFinset) c : Perm α)
        ((τ : Perm g.cycleFactorsFinset) d : Perm α) :=
        cycleFactorsFinset_pairwise_disjoint g ((τ : Perm g.cycleFactorsFinset) c).prop
          ((τ : Perm g.cycleFactorsFinset) d).prop (by
          intro h'; apply h
          simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h')
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
H' :
  Disjoint.{u_1} (α := α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
have H₁ : ∀ ⦃a : α⦄, a ∈ (↑d : Perm α).support → a ∉ (↑c : Perm α).support
Tactic: rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'
Cleared hypotheses: H, H'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
H' :
  Disjoint.{u_1} (α := α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
H₁ : ∀ ⦃a : α⦄, a ∈ (↑d : Perm α).support → a ∉ (↑c : Perm α).support
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
have H'₁ : ∀ ⦃a : α⦄,
  Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α))
      a →
    a ∉
      support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
Tactic: rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'
Cleared hypotheses: H, H'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
have inl : ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
  a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
Tactic: rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | hx)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
inl :
  ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
    a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
have inr : ∀
  (hx :
    ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
      (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
  a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
Tactic: rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | hx)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
have inl : Membership.mem (α := α) (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) ((g ^ j : (a : α) → α) x : α)
Tactic: rw [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ofPermHomFun_apply_of_mem_fixedPoints]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Eq (α := α) ((g : (a : α) → α) ((g ^ j : (a : α) → α) x : α) : α) ((g ^ j : (a : α) → α) x : α)
have inl : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
Tactic: simp only [← mul_apply, ← zpow_one_add, add_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
| ((g ^ j : (a : α) → α) x : α)
have rw : ((g ^ (j + 1) : (a : α) → α) x : α)
Tactic: rw [← hx, ← mul_apply, ← zpow_add_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
have conv_rhs : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
Tactic: conv_rhs => rw [← hx, ← mul_apply, ← zpow_add_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
conv_rhs : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
⊢ Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
have inl : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ (j + 1) : (a : α) → α) x : α)
Tactic: conv_rhs => rw [← hx, ← mul_apply, ← zpow_add_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx :
  ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
    (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
have inr : ∀ (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support) (m : ℤ)
  (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
  a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
Tactic: obtain ⟨c, hc, m, hm⟩ := 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 α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
have rw : Eq (α := α) ((g ^ j * g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
  ((g ^ j : (a : α) → α) x : α)
Tactic: rw [zpow_add, mul_apply, hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
rw :
  Eq (α := α) ((g ^ j * g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
⊢ Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
have rw₁ : Eq (α := α) ((g ^ j : (a : α) → α) ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α) : α)
  ((g ^ j : (a : α) → α) x : α)
Tactic: rw [zpow_add, mul_apply, hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
rw :
  Eq (α := α) ((g ^ j * g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((g ^ j : (a : α) → α) ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α) : α)
    ((g ^ j : (a : α) → α) x : α)
⊢ Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
have rw₂ : Eq (α := α) ((g ^ j : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
Tactic: rw [zpow_add, mul_apply, hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
have hm' : Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
  ((g ^ j : (a : α) → α) x : α)
Tactic: have hm' : (g ^ (j + m)) (a c) = (g ^ j) x := by rw [zpow_add, mul_apply, hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hm' :
  Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
have rw : Membership.mem (α := α) (↑c : Perm α).support ((g ^ j : (a : α) → α) x : α)
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm, ofPermHomFun_apply_of_cycleOf_mem a τ _ hm',
      ← mul_apply, ← zpow_add]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
have inl : ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
  a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
Tactic: rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
inl :
  ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
    a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
have inr : ∀ (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support) (m : ℤ)
  (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
  a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
Tactic: rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
have inr : (g ^ m : (a : α) → α)
    ((a : (a : ↥g.cycleFactorsFinset) → α)
        (((↑(σ * τ) : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
          ↥g.cycleFactorsFinset) :
      α) =
  a.ofPermHomFun σ
    ((g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α))
Tactic: simp only [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑(σ * τ) : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) =
    a.ofPermHomFun σ
      ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α))
have inr : Eq (α := α)
  ((g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑(σ * τ) : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) :
    α)
  ((g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑σ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) :
            ↥g.cycleFactorsFinset) :
        α) :
    α)
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a _ _ rfl]