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 : 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
⊢ x ∉ (↑d : Perm α).support
have this : (↑c : Perm α) ≠ (↑d : Perm α) → (↑c : Perm α).Disjoint (↑d : Perm α)
Tactic: have := g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥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 α)
⊢ x ∉ (↑d : Perm α).support
have this₁ : (↑c : Perm α) ≠ (↑d : Perm α) → ∀ ⦃a : α⦄, a ∈ (↑c : Perm α).support → a ∉ (↑d : Perm α).support
Tactic: rw [disjoint_iff_disjoint_support, Finset.disjoint_left] 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 : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ Finset.card.{u_1} (α := α) (support ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ)) =
    ∑ c ∈ (↑τ : Perm ↥g.cycleFactorsFinset).support, #(↑c : Perm α).support
have rw : (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset).PairwiseDisjoint (α := Finset α)
  fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support
Tactic: rw [ofPermHom_support, Finset.card_biUnion]
-- 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)
c : ↥g.cycleFactorsFinset
h_1 : c ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
d : ↥g.cycleFactorsFinset
h_2 : d ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
h : c ≠ d
⊢ Function.onFun (β := Finset α) _root_.Disjoint (fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) c d
have h₁ : (↑c : Perm α).Disjoint (↑d : Perm α)
Tactic: apply Equiv.Perm.Disjoint.disjoint_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)
⊢ Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (centralizer {g})
    ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α)
have rw : HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g =
  HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α)
Tactic: rw [mem_centralizer_singleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g =
    HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α)
have H : ∀ (x : α),
  Eq (α := α)
    ((HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g : (a : α) → α) x : α)
    ((HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) 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 : α
⊢ Eq (α := α)
    ((HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g : (a : α) → α) x : α)
    ((HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x : α)
have H : Eq (α := α)
  ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) ((g : (a : α) → α) x : α) : α)
  ((g : (a : α) → α) ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x : α) : α)
Tactic: simp only [mul_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
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
⊢ HSMul.hSMul (α := ↥(centralizer {g}))
      ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) c =
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c
have simp : (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) =
  HMul.hMul (α := Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α)
Tactic: simp only [← Subtype.coe_inj, val_centralizer_smul, InvMemClass.coe_inv, mul_inv_eq_iff_eq_mul]
-- 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
τ : ↥(range_toPermHom' g)
⊢ (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) =
    HMul.hMul (α := Perm α)
      (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
      (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α)
have H : ∀ (x : α),
  Eq (α := α)
    (((↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) :
          (a : α) → α)
        x :
      α)
    ((HMul.hMul (α := Perm α)
            (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
            (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) :
          (a : α) → α)
        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
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
⊢ Eq (α := α)
    (((↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) :
          (a : α) → α)
        x :
      α)
    ((HMul.hMul (α := Perm α)
            (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
            (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) :
          (a : α) → α)
        x :
      α)
have H : a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
  ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
      (a : α) → α)
    (a.ofPermHomFun τ x)
Tactic: simp only [mul_apply, toCentralizer_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
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
have pos : ∀ (hx : x ∈ (↑c : Perm α).support),
  a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
Tactic: by_cases hx : x ∈ c.val.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
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
pos :
  ∀ (hx : x ∈ (↑c : Perm α).support),
    a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
      ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
          (a : α) → α)
        (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
have neg : ∀ (hx : x ∉ (↑c : Perm α).support),
  a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
Tactic: by_cases hx : x ∈ c.val.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
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
⊢ a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
have pos : a.ofPermHomFun τ ((g : (a : α) → α) x) =
  ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
      (a : α) → α)
    (a.ofPermHomFun τ x)
Tactic: rw [(mem_cycleFactorsFinset_iff.mp c.prop).2 x hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
⊢ a.ofPermHomFun τ ((g : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
have this : a.ofPermHomFun τ ((HPow.hPow (β := ℤ) g 1 : (a : α) → α) x) =
  (HPow.hPow (β := ℤ) g 1 : (a : α) → α) (a.ofPermHomFun τ x)
Tactic: have := ofPermHomFun_commute_zpow_apply a τ x 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this :
  a.ofPermHomFun τ ((HPow.hPow (β := ℤ) g 1 : (a : α) → α) x) =
    (HPow.hPow (β := ℤ) g 1 : (a : α) → α) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
have this₁ : a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)
Tactic: simp only [zpow_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 : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this : a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
have pos : Membership.mem (γ := Finset α)
  (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
  (a.ofPermHomFun τ x)
Tactic: rw [this, ← (mem_cycleFactorsFinset_iff.mp ((τ : Perm g.cycleFactorsFinset) c).prop).2]
-- 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)
⊢ (OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
      ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) =
    (↑τ : Perm ↥g.cycleFactorsFinset)
have H : ∀ (x : ↥g.cycleFactorsFinset),
  Eq (α := ↥g.cycleFactorsFinset)
    ((((OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
              ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) :
            Perm ↥g.cycleFactorsFinset) :
          (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
        x :
      ↥g.cycleFactorsFinset)
    (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x :
      ↥g.cycleFactorsFinset)
Tactic: apply ext
-- 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)
c : ↥g.cycleFactorsFinset
⊢ Eq (α := ↥g.cycleFactorsFinset)
    ((((OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
              ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) :
            Perm ↥g.cycleFactorsFinset) :
          (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
        c :
      ↥g.cycleFactorsFinset)
    (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
      ↥g.cycleFactorsFinset)
have H : HSMul.hSMul (α := ↥(centralizer {g}))
    ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) c =
  ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c
Tactic: rw [OnCycleFactors.toPermHom_apply, toCentralizer_equivariant]
-- 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)
c : ↥g.cycleFactorsFinset
H :
  HSMul.hSMul (α := ↥(centralizer {g}))
      ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) c =
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c
⊢ Eq (α := ↥g.cycleFactorsFinset)
    ((((OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
              ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) :
            Perm ↥g.cycleFactorsFinset) :
          (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
        c :
      ↥g.cycleFactorsFinset)
    (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
      ↥g.cycleFactorsFinset)
have H₁ : Eq (α := ↥g.cycleFactorsFinset)
  (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c : ↥g.cycleFactorsFinset)
  (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c : ↥g.cycleFactorsFinset)
Tactic: rw [OnCycleFactors.toPermHom_apply, toCentralizer_equivariant]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    ∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support
have mp : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ →
  ∀ (c : ↥g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
      #(↑c : Perm α).support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
mp :
  Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ →
    ∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    ∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support
have mpr : (∀ (c : ↥g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
      #(↑c : Perm α).support) →
  Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ Finset.card.{u_1} (α := α)
      (support
        (↑((((toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset) k : Perm ↥g.cycleFactorsFinset) :
                (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              c) :
          Perm α)) =
    #(↑c : Perm α).support
have mp : #(Finset.map (Equiv.toEmbedding (↑k : Perm α)) (↑c : Perm α).support) = #(↑c : Perm α).support
Tactic: rw [coe_toPermHom, Equiv.Perm.support_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) →
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ
have mpr : ∀ (a : g.Basis),
  (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) →
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ
Tactic: obtain ⟨a⟩ := Basis.nonempty g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    Eq (α := ↥g.cycleFactorsFinset → ℕ)
      ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
        (⇑τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
      fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
have rw : (∀ (c : ↥g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
      #(↑c : Perm α).support) ↔
  ∀ (x : ↥g.cycleFactorsFinset),
    ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
          (⇑τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
        x =
      #(↑x : Perm α).support
Tactic: rw [mem_range_toPermHom_iff, funext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Eq (α := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) (range_toPermHom' g)
have h : ∀ (τ : Perm ↥g.cycleFactorsFinset),
  Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
Tactic: ext τ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
have h : (∀ (c : ↥g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
      #(↑c : Perm α).support) ↔
  Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
Tactic: rw [mem_range_toPermHom_iff, mem_range_toPermHom'_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
h :
  (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) ↔
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
have h₁ : (∀ (c : ↥g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
      #(↑c : Perm α).support) ↔
  ∀ (c : ↥g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
      #(↑c : Perm α).support
Tactic: rw [mem_range_toPermHom_iff, mem_range_toPermHom'_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have hsc : let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
Tactic: set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
this :
  Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have simp : Eq (α := ℕ)
  (∏ i ∈ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach,
    (Fintype.card.{u_1} { a : ↥g.cycleFactorsFinset // #(↑a : Perm α).support = i })!)
  (∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)
Tactic: simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]