awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
⊢ 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:
rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
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) :
      α)
⊢ 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 [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]

Premises used: Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 α))
    ((a : (a : ↥g.cycleFactorsFinset) → α)
        (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
          ↥g.cycleFactorsFinset) :
      α)

Tactic:
apply mem_support_self

Premises used: Equiv.Perm.Basis.mem_support_self
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
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
⊢ a.ofPermHomFun 1 x = x

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)

Premises used: Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
inl inl₁ : x = x
⊢ a.ofPermHomFun 1 x = x

Tactic:
rw [ofPermHomFun_apply_of_mem_fixedPoints a _ hx]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPoints
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
inr₄ inr₅ : x = x
⊢ a.ofPermHomFun 1 x = x

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, hm]

Premises used: OneMemClass.coe_one, Equiv.Perm.coe_one, Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem, id_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
rw₂ rw₃ : x = x
⊢ a.ofPermHomFun τ⁻¹ (a.ofPermHomFun τ x) = x

Tactic:
rw [← ofPermHomFun_mul, inv_mul_cancel, ofPermHomFun_one]

Premises used: inv_mul_cancel, Equiv.Perm.Basis.ofPermHomFun_mul, Equiv.Perm.Basis.ofPermHomFun_one
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
rw₂ rw₃ : x = x
⊢ a.ofPermHomFun τ (a.ofPermHomFun τ⁻¹ x) = x

Tactic:
rw [← ofPermHomFun_mul, mul_inv_cancel, ofPermHomFun_one]

Premises used: mul_inv_cancel, Equiv.Perm.Basis.ofPermHomFun_mul, Equiv.Perm.Basis.ofPermHomFun_one
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ_1 σ τ : ↥(range_toPermHom' g)
x : α
⊢ Eq (α := α)
    (({ toFun := a.ofPermHomFun (σ * τ), invFun := a.ofPermHomFun (σ * τ)⁻¹, left_inv := ⋯, right_inv := ⋯ : α ≃ α } :
          (a : α) → α)
        x :
      α)
    (({ toFun := a.ofPermHomFun σ, invFun := a.ofPermHomFun σ⁻¹, left_inv := ⋯, right_inv := ⋯ : α ≃ α } *
            { toFun := a.ofPermHomFun τ, invFun := a.ofPermHomFun τ⁻¹, left_inv := ⋯, right_inv := ⋯ : α ≃ α } :
          (a : α) → α)
        x :
      α)

Tactic:
simp [mul_apply, ofPermHomFun_mul a σ τ x]

Premises used: Equiv.Perm.mul_apply, Equiv.Perm.Basis.ofPermHomFun_mul
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ (((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x = a.ofPermHomFun τ x

Tactic:
rfl

Premises used: dite, Equiv.Perm.Basis.ofPermHomFun, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
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
⊢ Eq (α := Finset α) (support ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ))
    ((↑τ : Perm ↥g.cycleFactorsFinset).support.biUnion fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
h :
  a.ofPermHomFun τ x ≠ x ↔
    ∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ 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:
simp only [mem_support, Finset.mem_biUnion, ofPermHom_apply]

Premises used: Equiv.Perm.mem_support, Equiv.Perm.Basis.ofPermHom_apply, Finset.mem_biUnion
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
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
⊢ 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⟩)

Premises used: Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
h : ¬∃ a ∈ (↑τ : Perm ↥g.cycleFactorsFinset).support, x ∈ (↑a : Perm α).support
⊢ 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 [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
      ← mem_support]

Premises used: Equiv.Perm.mem_support, not_true_eq_false, false_iff, ne_eq, Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPoints
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
h : ∀ (hx : (g : (a : α) → α) x = x) (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support), False
⊢ False

Tactic:
rw [Function.mem_fixedPoints_iff] at hx

Premises used: Function.mem_fixedPoints_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : (g : (a : α) → α) x = x
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
⊢ False

Tactic:
mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx

Premises used: Equiv.Perm.mem_support, Subtype.prop, Iff.mp, Equiv.Perm.mem_cycleFactorsFinset_support_le
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : (g : (a : α) → α) x = x
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
⊢ False

Tactic:
exact mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx

Premises used: Equiv.Perm.mem_support, Subtype.prop, Iff.mp, Equiv.Perm.mem_cycleFactorsFinset_support_le
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 :
  (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
⊢ a.ofPermHomFun τ x ≠ 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]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
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 : α) : α)
| (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) ≠
    x

Tactic:
rw [← hm]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 :
  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
⊢ (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:
conv_lhs => rw [← hm]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 :
  (¬∃ (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
⊢ 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:
rw [(g ^ m).injective.ne_iff, a.injective.ne_iff, not_iff_comm]

Premises used: Equiv.Perm.Basis.injective, Function.Injective.ne_iff, HPow.hPow, Equiv.injective, not_iff_comm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
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
⊢ (¬∃ (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

Premises used: Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
pos :
  ¬∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ 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

Tactic:
simp only [H, iff_true]

Premises used: iff_true
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
pos :
  ∀ (a : ↥g.cycleFactorsFinset)
    (_ : ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a),
    ((↑a : Perm α) : (a : α) → α) x = x
⊢ ¬∃ (a : ↥g.cycleFactorsFinset),
      ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) a ≠ a ∧
        ((↑a : Perm α) : (a : α) → α) x ≠ x

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
pos : x ∉ (↑d : Perm α).support
⊢ ((↑d : Perm α) : (a : α) → α) x = x

Tactic:
rw [← notMem_support]

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
⊢ (↑c : Perm α) ≠ (↑d : Perm α) → (↑c : Perm α).Disjoint (↑d : Perm α)

Tactic:
have := g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
this : (↑c : Perm α) ≠ (↑d : Perm α) → (↑c : Perm α).Disjoint (↑d : Perm α)
⊢ (↑c : Perm α) ≠ (↑d : Perm α) → ∀ ⦃a : α⦄, a ∈ (↑c : Perm α).support → a ∉ (↑d : Perm α).support

Tactic:
rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at this

Premises used: Finset.disjoint_left, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
this : (↑c : Perm α) ≠ (↑d : Perm α) → ∀ ⦃a : α⦄, a ∈ (↑c : Perm α).support → a ∉ (↑d : Perm α).support
⊢ (↑c : Perm α) ≠ (↑d : Perm α)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
this : (↑c : Perm α) ≠ (↑d : Perm α) → ∀ ⦃a : α⦄, a ∈ (↑c : Perm α).support → a ∉ (↑d : Perm α).support
⊢ x ∉ (↑d : Perm α).support

Tactic:
exact this (by lia) hc
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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

Tactic:
simpa only [H, iff_false, not_not] using ⟨c, H, mem_support.mp hc⟩

Premises used: iff_false, Classical.not_not