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
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
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) :
          α) :
      α)
⊢ (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 rw : 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) c :
            ↥g.cycleFactorsFinset) :
        α) :
    α)
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a _ _ rfl]
-- 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
⊢ 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) c :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
have rw : 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) c :
        ↥g.cycleFactorsFinset) :
    α)
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
x : α
⊢ a.ofPermHomFun 1 x = x
have inl : ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x), a.ofPermHomFun 1 x = 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
x : α
inl : ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x), a.ofPermHomFun 1 x = x
⊢ a.ofPermHomFun 1 x = x
have inr : ∀ (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support) (m : ℤ)
  (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x), a.ofPermHomFun 1 x = 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
x : α
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ a.ofPermHomFun 1 x = x
have inl : x = x
Tactic: rw [ofPermHomFun_apply_of_mem_fixedPoints a _ 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
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ a.ofPermHomFun 1 x = x
have inr : (g ^ m : (a : α) → α)
    ((a : (a : ↥g.cycleFactorsFinset) → α)
        (((↑1 : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
          ↥g.cycleFactorsFinset) :
      α) =
  x
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, 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
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
inr :
  (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑1 : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) =
    x
⊢ a.ofPermHomFun 1 x = x
have inr₁ : (g ^ m : (a : α) → α)
    ((a : (a : ↥g.cycleFactorsFinset) → α)
        ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c : ↥g.cycleFactorsFinset) :
      α) =
  x
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, 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
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
inr :
  (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑1 : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) =
    x
inr₁ :
  (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c : ↥g.cycleFactorsFinset) :
        α) =
    x
⊢ a.ofPermHomFun 1 x = x
have inr₂ : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) (id c) : α) = x
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, 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
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
inr :
  (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑1 : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) =
    x
inr₁ :
  (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c : ↥g.cycleFactorsFinset) :
        α) =
    x
inr₂ : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) (id c) : α) = x
inr₃ : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ a.ofPermHomFun 1 x = x
have inr₄ : x = x
Tactic: rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, 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
c : ↥g.cycleFactorsFinset
τ_1 τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ⁻¹ (a.ofPermHomFun τ x) = x
have rw : a.ofPermHomFun (τ⁻¹ * τ) x = x
Tactic: rw [← ofPermHomFun_mul, inv_mul_cancel, ofPermHomFun_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
c : ↥g.cycleFactorsFinset
τ_1 τ : ↥(range_toPermHom' g)
x : α
rw : a.ofPermHomFun (τ⁻¹ * τ) x = x
⊢ a.ofPermHomFun τ⁻¹ (a.ofPermHomFun τ x) = x
have rw₁ : a.ofPermHomFun 1 x = x
Tactic: rw [← ofPermHomFun_mul, inv_mul_cancel, ofPermHomFun_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
c : ↥g.cycleFactorsFinset
τ_1 τ : ↥(range_toPermHom' g)
x : α
rw : a.ofPermHomFun (τ⁻¹ * τ) x = x
rw₁ : a.ofPermHomFun 1 x = x
⊢ a.ofPermHomFun τ⁻¹ (a.ofPermHomFun τ x) = x
have rw₂ : x = x
Tactic: rw [← ofPermHomFun_mul, inv_mul_cancel, ofPermHomFun_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
c : ↥g.cycleFactorsFinset
τ_1 τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ (a.ofPermHomFun τ⁻¹ x) = x
have rw : a.ofPermHomFun (τ * τ⁻¹) x = x
Tactic: rw [← ofPermHomFun_mul, mul_inv_cancel, ofPermHomFun_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
c : ↥g.cycleFactorsFinset
τ_1 τ : ↥(range_toPermHom' g)
x : α
rw : a.ofPermHomFun (τ * τ⁻¹) x = x
⊢ a.ofPermHomFun τ (a.ofPermHomFun τ⁻¹ x) = x
have rw₁ : a.ofPermHomFun 1 x = x
Tactic: rw [← ofPermHomFun_mul, mul_inv_cancel, ofPermHomFun_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
c : ↥g.cycleFactorsFinset
τ_1 τ : ↥(range_toPermHom' g)
x : α
rw : a.ofPermHomFun (τ * τ⁻¹) x = x
rw₁ : a.ofPermHomFun 1 x = x
⊢ a.ofPermHomFun τ (a.ofPermHomFun τ⁻¹ x) = x
have rw₂ : x = x
Tactic: rw [← ofPermHomFun_mul, mul_inv_cancel, ofPermHomFun_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)
⊢ Eq (α := Finset α) (support ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ))
    ((↑τ : Perm ↥g.cycleFactorsFinset).support.biUnion fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support)
have h : ∀ (x : α),
  Membership.mem (γ := Finset α) (support ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ)) x ↔
    Membership.mem (γ := Finset α)
      ((↑τ : Perm ↥g.cycleFactorsFinset).support.biUnion fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) 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 α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ Membership.mem (γ := Finset α) (support ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ)) x ↔
    Membership.mem (γ := Finset α)
      ((↑τ : Perm ↥g.cycleFactorsFinset).support.biUnion fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) x
have h : a.ofPermHomFun τ x ≠ x ↔
  ∃ (a : ↥g.cycleFactorsFinset),
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
      ((↑a : Perm α) : (a : α) → α) x ≠ x
Tactic: simp only [mem_support, Finset.mem_biUnion, ofPermHom_apply]
-- 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 ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have h : ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
  a.ofPermHomFun τ x ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ 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 : α
h :
  ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
    a.ofPermHomFun τ x ≠ x ↔
      ∃ (a : ↥g.cycleFactorsFinset),
        ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
          ((↑a : Perm α) : (a : α) → α) x ≠ x
⊢ a.ofPermHomFun τ x ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have h₁ : ∀ (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support) (m : ℤ)
  (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
  a.ofPermHomFun τ x ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ 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 : α
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ a.ofPermHomFun τ x ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have h : ¬∃ a ∈ (↑τ : Perm ↥g.cycleFactorsFinset).support, x ∈ (↑a : Perm α).support
Tactic: simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
      ← mem_support]
-- 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 : α
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
⊢ False
have h : ∀ (hx : (g : (a : α) → α) x = x) (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support), False
Tactic: rw [Function.mem_fixedPoints_iff] at hx
Cleared hypotheses: hx, c, hc
-- 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 ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have h : (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) ≠
    x ↔
  ∃ (a : ↥g.cycleFactorsFinset),
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
      ((↑a : Perm α) : (a : α) → α) x ≠ x
Tactic: rw [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) :
        α) ≠
    x
have rw : Ne (α := α)
  ((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) → α) c : α) : α)
Tactic: rw [← 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) :
          α) ≠
      x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have h : Ne (α := α)
    ((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) → α) c : α) : α) ↔
  ∃ (a : ↥g.cycleFactorsFinset),
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
      ((↑a : Perm α) : (a : α) → α) x ≠ x
Tactic: conv_lhs => rw [← 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
⊢ Ne (α := α)
      ((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) → α) c : α) : α) ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have h : (¬∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
  ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
Tactic: rw [(g ^ m).injective.ne_iff, a.injective.ne_iff, not_iff_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 : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ (¬∃ (a : ↥g.cycleFactorsFinset),
        ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
          ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
have pos : ∀ (H : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c),
  (¬∃ (a : ↥g.cycleFactorsFinset),
        ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
          ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
Tactic: by_cases H : (τ : Perm g.cycleFactorsFinset) c = c
-- 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
pos :
  ∀ (H : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c),
    (¬∃ (a : ↥g.cycleFactorsFinset),
          ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
            ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
⊢ (¬∃ (a : ↥g.cycleFactorsFinset),
        ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
          ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
have neg : ∀ (H : ¬((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c),
  (¬∃ (a : ↥g.cycleFactorsFinset),
        ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
          ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
Tactic: by_cases H : (τ : Perm g.cycleFactorsFinset) c = c
-- 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
H : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
⊢ (¬∃ (a : ↥g.cycleFactorsFinset),
        ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
          ((↑a : Perm α) : (a : α) → α) x ≠ x) ↔
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
have pos : ¬∃ (a : ↥g.cycleFactorsFinset),
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
      ((↑a : Perm α) : (a : α) → α) x ≠ x
Tactic: simp only [H, iff_true]
-- 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
H : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
⊢ ¬∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x
have pos : ∀ (a : ↥g.cycleFactorsFinset)
  (_ : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a),
  ((↑a : Perm α) : (a : α) → α) x = x
Tactic: push Not
-- 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
H : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c = c
d : ↥g.cycleFactorsFinset
hd : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d ≠ d
⊢ ((↑d : Perm α) : (a : α) → α) x = x
have pos : x ∉ (↑d : Perm α).support
Tactic: rw [← notMem_support]