awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : Perm ↥g.cycleFactorsFinset
hσ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    a
hτ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    b
hσ₁ :
  ∀ (a_1 : Perm α) (b : a_1 ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((a : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a_1 b)) :
            Perm α)) =
      #a_1.support
⊢ ∀ (a : Perm α) (b_1 : a ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((b : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b_1)) :
            Perm α)) =
      #a.support

Tactic:
simp only [Subtype.forall, Set.mem_setOf_eq] at hσ hτ

Premises used: Subtype.forall, Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : Perm ↥g.cycleFactorsFinset
hσ :
  ∀ (a_1 : Perm α) (b : a_1 ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((a : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a_1 b)) :
            Perm α)) =
      #a_1.support
hτ :
  ∀ (a : Perm α) (b_1 : a ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((b : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b_1)) :
            Perm α)) =
      #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
rw :
  Finset.card.{u_1} (α := α)
      (support
        (↑((b : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) c hc)) :
          Perm α)) =
    #c.support
rw₁ rw₂ : #c.support = #c.support
⊢ Finset.card.{u_1} (α := α)
      (support
        (↑((a : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              ((b : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) c hc))) :
          Perm α)) =
    #c.support

Tactic:
rw [hσ, hτ]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : Perm ↥g.cycleFactorsFinset
hσ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    x
simp :
  ∀
    (hσ :
      ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α)
            (support
              (↑((x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                    (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b)) :
                Perm α)) =
          #a.support)
    (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((x⁻¹ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b)) :
            Perm α)) =
      #a.support
⊢ Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    x⁻¹

Tactic:
simp only [Subtype.forall, Set.mem_setOf_eq] at hσ ⊢

Premises used: Subtype.forall, Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : Perm ↥g.cycleFactorsFinset
hσ :
  ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b)) :
            Perm α)) =
      #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ (↑((x⁻¹ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) c hc)) :
      Perm α) ∈
    g.cycleFactorsFinset

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : Perm ↥g.cycleFactorsFinset
hσ :
  ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b)) :
            Perm α)) =
      #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
rw :
  Finset.card.{u_1} (α := α)
      (support
        (↑((x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset)
                (↑((x⁻¹ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                      (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) c hc)) :
                  Perm α)
                ⋯)) :
          Perm α)) =
    #c.support
⊢ Finset.card.{u_1} (α := α)
      (support
        (↑((x⁻¹ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) c hc)) :
          Perm α)) =
    #c.support

Tactic:
rw [← hσ _ (by simp)]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : Perm ↥g.cycleFactorsFinset
hσ :
  ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b)) :
            Perm α)) =
      #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Finset.card.{u_1} (α := α)
      (support
        (↑((x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset)
                (↑((x⁻¹ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                      (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) c hc)) :
                  Perm α)
                ⋯)) :
          Perm α)) =
    #c.support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ ↔
    ∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
simp :
  (∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
      Eq (α := ↥g.cycleFactorsFinset)
        ((((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset :
                    (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
                  k :
                Perm ↥g.cycleFactorsFinset) :
              (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b) :
          ↥g.cycleFactorsFinset)
        ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b) :
          ↥g.cycleFactorsFinset)) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k : Perm α) c
⊢ k ∈ MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k : Perm α) c

Tactic:
simp only [toPermHom, MonoidHom.mem_ker, DFunLike.ext_iff, Subtype.forall]

Premises used: Subtype.forall, MonoidHom.mem_ker, DFunLike.ext_iff, Equiv.Perm.OnCycleFactors.toPermHom
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ (∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
      Eq (α := ↥g.cycleFactorsFinset)
        ((((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset :
                    (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
                  k :
                Perm ↥g.cycleFactorsFinset) :
              (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b) :
          ↥g.cycleFactorsFinset)
        ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b) :
          ↥g.cycleFactorsFinset)) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k : Perm α) c

Tactic:
forall₂_congr (fun _ _ ↦ ?_)

Premises used: forall₂_congr
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
refine :
  ∀ (x : Perm α) (x_1 : x ∈ g.cycleFactorsFinset),
    Eq (α := ↥g.cycleFactorsFinset)
        ((((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset :
                    (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
                  k :
                Perm ↥g.cycleFactorsFinset) :
              (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) x x_1) :
          ↥g.cycleFactorsFinset)
        ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) x x_1) :
          ↥g.cycleFactorsFinset) ↔
      Commute (↑k : Perm α) x
⊢ (∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
      Eq (α := ↥g.cycleFactorsFinset)
        ((((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset :
                    (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
                  k :
                Perm ↥g.cycleFactorsFinset) :
              (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b) :
          ↥g.cycleFactorsFinset)
        ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a b) :
          ↥g.cycleFactorsFinset)) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k : Perm α) c

Tactic:
refine forall₂_congr (fun _ _ ↦ ?_)

Premises used: forall₂_congr
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
x : Perm α
h : x ∈ g.cycleFactorsFinset
⊢ Eq (α := ↥g.cycleFactorsFinset)
      ((((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset :
                  (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
                k :
              Perm ↥g.cycleFactorsFinset) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) x h) :
        ↥g.cycleFactorsFinset)
      ((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) x h) :
        ↥g.cycleFactorsFinset) ↔
    Commute (↑k : Perm α) x

Tactic:
simp [← Subtype.coe_inj, commute_iff_eq, mul_inv_eq_iff_eq_mul]

Premises used: Subtype.coe_inj, commute_iff_eq, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g_1 g : Perm α
a a' : g.Basis
h :
  Eq.{u_1 + 1} (α := (a : ↥g.cycleFactorsFinset) → α) ((fun (a : g.Basis) ↦ a.toFun) a)
    ((fun (a : g.Basis) ↦ a.toFun) a')
mk :
  ∀ (toFun : ↥g.cycleFactorsFinset → α)
    (mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c : Perm α).support),
    Eq.{u_1 + 1} (α := (a : ↥g.cycleFactorsFinset) → α)
        ((fun (a : g.Basis) ↦ a.toFun) { toFun := toFun, mem_support_self' := mem_support_self' })
        ((fun (a : g.Basis) ↦ a.toFun) a') →
      { toFun := toFun, mem_support_self' := mem_support_self' : g.Basis } = a'
⊢ a = a'

Tactic:
cases a
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g_1 g : Perm α
a' : g.Basis
toFun : ↥g.cycleFactorsFinset → α
mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c : Perm α).support
h :
  Eq.{u_1 + 1} (α := (a : ↥g.cycleFactorsFinset) → α)
    ((fun (a : g.Basis) ↦ a.toFun) { toFun := toFun, mem_support_self' := mem_support_self' })
    ((fun (a : g.Basis) ↦ a.toFun) a')
mk :
  ∀ (toFun_1 : ↥g.cycleFactorsFinset → α)
    (mem_support_self'_1 : ∀ (c : ↥g.cycleFactorsFinset), toFun_1 c ∈ (↑c : Perm α).support),
    Eq.{u_1 + 1} (α := (a : ↥g.cycleFactorsFinset) → α)
        ((fun (a : g.Basis) ↦ a.toFun) { toFun := toFun, mem_support_self' := mem_support_self' })
        ((fun (a : g.Basis) ↦ a.toFun) { toFun := toFun_1, mem_support_self' := mem_support_self'_1 }) →
      { toFun := toFun, mem_support_self' := mem_support_self' : g.Basis } =
        { toFun := toFun_1, mem_support_self' := mem_support_self'_1 }
⊢ { toFun := toFun, mem_support_self' := mem_support_self' : g.Basis } = a'

Tactic:
cases a'
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g_1 g : Perm α
toFun : ↥g.cycleFactorsFinset → α
mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c : Perm α).support
toFun_1 : ↥g.cycleFactorsFinset → α
mem_support_self'_1 : ∀ (c : ↥g.cycleFactorsFinset), toFun_1 c ∈ (↑c : Perm α).support
h :
  Eq.{u_1 + 1} (α := (a : ↥g.cycleFactorsFinset) → α)
    ((fun (a : g.Basis) ↦ a.toFun) { toFun := toFun, mem_support_self' := mem_support_self' })
    ((fun (a : g.Basis) ↦ a.toFun) { toFun := toFun_1, mem_support_self' := mem_support_self'_1 })
⊢ { toFun := toFun, mem_support_self' := mem_support_self' : g.Basis } =
    { toFun := toFun_1, mem_support_self' := mem_support_self'_1 }

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ ∀ (c : ↥g.cycleFactorsFinset), (↑c : Perm α).support.Nonempty

Tactic:
have (c : g.cycleFactorsFinset) : c.val.support.Nonempty :=
    IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp c.prop).1
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
this : ∀ (c : ↥g.cycleFactorsFinset), (↑c : Perm α).support.Nonempty
⊢ Nonempty.{u_1 + 1} g.Basis

Tactic:
⟨fun c ↦ (this c).choose, fun c ↦ (this c).choose_spec⟩

Premises used: Exists.choose_spec, Equiv.Perm.Basis.mk, Nonempty.intro, Exists.choose
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
this : ∀ (c : ↥g.cycleFactorsFinset), (↑c : Perm α).support.Nonempty
⊢ Nonempty.{u_1 + 1} g.Basis

Tactic:
exact ⟨fun c ↦ (this c).choose, fun c ↦ (this c).choose_spec⟩
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
⊢ Membership.mem (α := α) (↑c : Perm α).support ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)

Tactic:
a.mem_support_self' c

Premises used: Equiv.Perm.Basis.mem_support_self', Set.Mem, setOf
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
rw : (↑c : Perm α) = (↑d : Perm α)
⊢ c = d

Tactic:
rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
apply : ¬(↑c : Perm α).Disjoint (↑d : Perm α)
⊢ (↑c : Perm α) = (↑d : Perm α)

Tactic:
apply g.cycleFactorsFinset_pairwise_disjoint.eq c.prop d.prop

Premises used: Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Subtype.prop, Set.Pairwise.eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
simp : ∃ (x : α), ¬((↑c : Perm α) : (a : α) → α) x = x ∧ ¬((↑d : Perm α) : (a : α) → α) x = x
⊢ ¬(↑c : Perm α).Disjoint (↑d : Perm α)

Tactic:
simp only [Disjoint, not_forall, not_or]

Premises used: not_or, Classical.not_forall, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
h₁ :
  ¬Eq (α := α) (((↑c : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ∧
    ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)
⊢ ∃ (x : α), ¬((↑c : Perm α) : (a : α) → α) x = x ∧ ¬((↑d : Perm α) : (a : α) → α) x = x

Tactic:
use a c

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
rw :
  ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) : α)
      ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
| ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
      ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
h₁ :
  ¬Eq (α := α) (((↑c : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ∧
    ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
⊢ ¬Eq (α := α) (((↑c : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ∧
    ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)

Tactic:
conv_rhs => rw [h]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
⊢ ¬Eq (α := α) (((↑c : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ∧
    ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)

Tactic:
simp only [← Perm.mem_support, a.mem_support_self c, a.mem_support_self d, and_self]

Premises used: and_self, Equiv.Perm.mem_support, 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
c : ↥g.cycleFactorsFinset
⊢ g.cycleOf ((a : (a : ↥g.cycleFactorsFinset) → α) c) = (↑c : Perm α)

Tactic:
(cycle_is_cycleOf (a.mem_support_self c) c.prop).symm

Premises used: Equiv.Perm.cycle_is_cycleOf, Equiv.Perm.Basis.mem_support_self, Subtype.prop, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle
    ((a : (a : ↥g.cycleFactorsFinset) → α)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx))
    x

Tactic:
(mem_support_cycleOf_iff.mp (a.mem_support_self ⟨g.cycleOf x, hx⟩)).1.symm

Premises used: Equiv.Perm.SameCycle.symm, Equiv.Perm.mem_support_cycleOf_iff, Equiv.Perm.Basis.mem_support_self, Subtype.mk, And.left, Iff.mp, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
rw :
  x ∉ Function.fixedPoints (⇑g : (a : α) → α) →
    ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
      (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x ∨
    ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
      (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x

Tactic:
rw [Classical.or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
⊢ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
rw [Function.mem_fixedPoints_iff, ← ne_eq, ← mem_support,
    ← cycleOf_mem_cycleFactorsFinset_iff] at hx

Premises used: Equiv.Perm.mem_support, Function.mem_fixedPoints_iff, ne_eq, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
    (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x

Tactic:
⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle hx)⟩

Premises used: Equiv.Perm.Basis.sameCycle, Subtype.mk, Exists.intro, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
refine : x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α).support
⊢ ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
    (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x

Tactic:
refine ⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle hx)⟩