awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (g * (k * k⁻¹)).cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
⊢ (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
have this₁ : g.cycleFactorsFinset =
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
    g.cycleFactorsFinset
Tactic: simp only [mul_inv_cancel, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  g.cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
| (↑g.cycleFactorsFinset : Set (Perm α))
have rw : (↑(HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset) :
  Set (Perm α))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  g.cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
⊢ (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
have conv_lhs : (↑(HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g.cycleFactorsFinset) :
    Set (Perm α)) =
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
    (↑g.cycleFactorsFinset : Set (Perm α))
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k l : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ (k * l) • c = k • l • c
have simp : (↑((k * l) • c) : Perm α) = (↑(k • l • c) : Perm α)
Tactic: simp only [← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
⊢ HSMul.hSMul (α := ↥(centralizer {g})) 1 c = c
have rw : (↑(HSMul.hSMul (α := ↥(centralizer {g})) 1 c) : Perm α) = (↑c : Perm α)
Tactic: rw [← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ 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 * b)
have simp : ∀ (a_1 : Perm α) (b_1 : a_1 ∈ g.cycleFactorsFinset),
  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) a_1 b_1))) :
          Perm α)) =
    #a_1.support
Tactic: simp only [Subtype.forall, Set.mem_setOf_eq, coe_mul, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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
⊢ ∀ (a_1 : Perm α) (b_1 : a_1 ∈ g.cycleFactorsFinset),
    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) a_1 b_1))) :
            Perm α)) =
      #a_1.support
have 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
Tactic: simp only [Subtype.forall, Set.mem_setOf_eq] 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 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_1 : Perm α) (b_1 : a_1 ∈ g.cycleFactorsFinset),
    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) a_1 b_1))) :
            Perm α)) =
      #a_1.support
have 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
Tactic: simp only [Subtype.forall, Set.mem_setOf_eq] 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 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
⊢ 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
have 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
Tactic: rw [hσ, hτ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ 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
have rw₁ : #c.support = #c.support
Tactic: rw [hσ, hτ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ 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⁻¹
have 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
Tactic: simp only [Subtype.forall, Set.mem_setOf_eq] at hσ ⊢
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) c hc)) :
          Perm α)) =
    #c.support
have 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 α)
              sorry)) :
        Perm α)) =
  #c.support
Tactic: rw [← hσ _ (by simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ k ∈ MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k : Perm α) c
have 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
Tactic: simp only [toPermHom, MonoidHom.mem_ker, DFunLike.ext_iff, Subtype.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
have 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
Tactic: refine forall₂_congr (fun _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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')
⊢ a = a'
have 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'
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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')
⊢ { toFun := toFun, mem_support_self' := mem_support_self' : g.Basis } = a'
have 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 }
Tactic: cases a'
Cleared hypotheses: a', h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Nonempty.{u_1 + 1} g.Basis
have this : ∀ (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
-- 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 d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
⊢ c = d
have rw : (↑c : Perm α) = (↑d : Perm α)
Tactic: rw [← Subtype.coe_inj]
-- 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 d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
⊢ (↑c : Perm α) = (↑d : Perm α)
have apply : ¬(↑c : Perm α).Disjoint (↑d : Perm α)
Tactic: apply g.cycleFactorsFinset_pairwise_disjoint.eq c.prop d.prop
-- 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 d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
⊢ ¬(↑c : Perm α).Disjoint (↑d : Perm α)
have simp : ∃ (x : α), ¬((↑c : Perm α) : (a : α) → α) x = x ∧ ¬((↑d : Perm α) : (a : α) → α) x = x
Tactic: simp only [Disjoint, not_forall, not_or]
-- 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 d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
⊢ ∃ (x : α), ¬((↑c : Perm α) : (a : α) → α) x = x ∧ ¬((↑d : Perm α) : (a : α) → α) x = x
have 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 : α)
Tactic: use a 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
c d : ↥g.cycleFactorsFinset
h : Eq (α := α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
| ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
      ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)
have rw : ¬Eq (α := α) (((↑d : Perm α) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) : α)
    ((a : (a : ↥g.cycleFactorsFinset) → α) d : α)
Tactic: rw [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
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) → α) c : α) : α)
        ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)
have 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 : α)
Tactic: conv_rhs => rw [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
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
have rw : x ∉ Function.fixedPoints (⇑g : (a : α) → α) →
  ∃ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
⊢ ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
    (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
have hx₁ : g.cycleOf x ∈ g.cycleFactorsFinset
Tactic: rw [Function.mem_fixedPoints_iff, ← ne_eq, ← mem_support,
    ← cycleOf_mem_cycleFactorsFinset_iff] at 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
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
    (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
have refine : x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α).support
Tactic: refine ⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle 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 : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α).support
have rw : g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset
Tactic: rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]