awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
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
⊢ 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

Tactic:
rw [mem_range_toPermHom_iff, funext_iff]

Premises used: funext_iff, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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) ↔
    ∀ (x : ↥g.cycleFactorsFinset),
      ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
            (⇑τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
          x =
        #(↑x : Perm α).support

Tactic:
simp only [Subtype.forall, Function.comp_apply]

Premises used: Subtype.forall, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h :
  ∀ (τ : Perm ↥g.cycleFactorsFinset),
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
⊢ Eq (α := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) (range_toPermHom' g)

Tactic:
ext τ
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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) τ
h₁ 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
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ

Tactic:
rw [mem_range_toPermHom_iff, mem_range_toPermHom'_iff]

Premises used: Equiv.Perm.OnCycleFactors.mem_range_toPermHom'_iff, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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

Premises used: Equiv.Perm.support, Finset.card, Subtype.val
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)
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)!)
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ 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]

Premises used: DomMulAct.stabilizer_card', Finset.univ_eq_attach, Set.coe_setOf, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)
simp_rw :
  Eq (α := ℕ)
    (∏ x ∈ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach,
      (Multiset.count x g.cycleType)!)
    (∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!)
⊢ 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_rw [← CycleType.count_def]

Premises used: Equiv.Perm.CycleType.count_def
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)
apply :
  Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach =
    g.cycleType.toFinset
⊢ Eq (α := ℕ)
    (∏ x ∈ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach,
      (Multiset.count x g.cycleType)!)
    (∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!)

Tactic:
apply Finset.prod_congr _ (fun _ _ => rfl)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)
h :
  ∀ (n : ℕ),
    Membership.mem (γ := Finset ℕ)
        (Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach) n ↔
      n ∈ g.cycleType.toFinset
⊢ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach =
    g.cycleType.toFinset

Tactic:
ext n
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)
n : ℕ
h : (∃ a ∈ g.cycleFactorsFinset, #a.support = n) ↔ n ∈ g.cycleType
⊢ Membership.mem (γ := Finset ℕ)
      (Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach) n ↔
    n ∈ g.cycleType.toFinset

Tactic:
simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]

Premises used: Finset.mem_image, Finset.mem_attach, Subtype.exists, exists_prop, Multiset.mem_toFinset, true_and
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)
n : ℕ
⊢ (∃ a ∈ g.cycleFactorsFinset, #a.support = n) ↔ n ∈ g.cycleType

Tactic:
simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]

Premises used: Multiset.mem_map, Function.comp_apply, Equiv.Perm.cycleType_def, Finset.mem_val
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
suffices :
  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)!

Tactic:
suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
simp :
  Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Nat.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
⊢ 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)

Tactic:
simp only [Fintype.card_eq_nat_card]

Premises used: Fintype.card_eq_nat_card
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
e_α :
  Eq.{u_1 + 1} (α := Perm ↥g.cycleFactorsFinset → Prop)
    (fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x)
    fun (x : Perm ↥g.cycleFactorsFinset) ↦
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Nat.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
e_α :
  ∀ (x : Perm ↥g.cycleFactorsFinset),
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x ↔
      Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
        {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
⊢ Eq.{u_1 + 1} (α := Perm ↥g.cycleFactorsFinset → Prop)
    (fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x)
    fun (x : Perm ↥g.cycleFactorsFinset) ↦
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
x : Perm ↥g.cycleFactorsFinset
e_α :
  (Eq (α := ↥g.cycleFactorsFinset → ℕ)
      ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
        (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
      fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ↔
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
e_α₁ e_α₂ :
  (Eq (α := ↥g.cycleFactorsFinset → ℕ)
      ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
        (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
      fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ↔
    sc ∘ (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x ↔
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x

Tactic:
rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]

Premises used: Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff', Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
pos :
  ∀ (hx : g.cycleOf x ∈ g.cycleFactorsFinset),
    Eq (α := α)
      ((((kerParam g :
                  (a :
                      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                    Perm α)
                (u, v) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x :
        α)
neg :
  ∀ (hx : g.cycleOf x ∉ g.cycleFactorsFinset),
    Eq (α := α)
      ((((kerParam g :
                  (a :
                      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                    Perm α)
                (u, v) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x :
        α)
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
        ((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x
      else
        (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x :
      α)

Tactic:
split_ifs with hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
have hx' := hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx hx' : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∉ Function.fixedPoints (⇑g : (a : α) → α)

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

Premises used: Equiv.Perm.mem_support, Function.mem_fixedPoints_iff, Ne, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
pos :
  (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α) ∉
    support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯)
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
        x :
      α)

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply', mul_apply, ofSubtype_apply_of_not_mem u hx',
      noncommPiCoprod_apply, ← Finset.noncommProd_erase_mul _ (Finset.mem_univ ⟨g.cycleOf x, hx⟩),
      mul_apply, ← notMem_support]

Premises used: Finset.mem_univ, Equiv.Perm.notMem_support, Finset.univ, Subgroup.noncommPiCoprod_apply, Finset.noncommProd_erase_mul, Finset.mem_of_mem_erase, Equiv.Perm.OnCycleFactors.kerParam, Equiv.Perm.ofSubtype_apply_of_not_mem, Equiv.Perm.mul_apply, MonoidHom.noncommCoprod_apply'
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
pos :
  ∀
    (hx' :
      Membership.mem (α := α) (γ := Finset α)
        (support
          ((Finset.erase Finset.univ
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
            (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
        (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
              (a : α) → α)
            x :
          α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α) ∉
    support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯)

Tactic:
contrapose hx'
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
pos :
  ∀ (a : ↥g.cycleFactorsFinset)
    (ha1 :
      a ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx))
    (ha2 :
      Membership.mem (α := α) (↑((u, v).2 a) : Perm α).support
        (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
              (a : α) → α)
            x :
          α)),
    Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x

Tactic:
obtain ⟨a, ha1, ha2⟩ := mem_support_of_mem_noncommProd_support hx'

Premises used: Equiv.Perm.mem_support_of_mem_noncommProd_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  Membership.mem (α := α) (γ := Finset α)
    (support
      ((Finset.erase Finset.univ
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)).noncommProd
        (fun (i : ↥g.cycleFactorsFinset) ↦ (↑((u, v).2 i) : Perm α)) ⋯))
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
a : ↥g.cycleFactorsFinset
ha1 : a ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)
ha2 :
  Membership.mem (α := α) (↑((u, v).2 a) : Perm α).support
    (((↑((u, v).2 (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) :
          (a : α) → α)
        x :
      α)
⊢ ¬(↑a : Perm α) = g.cycleOf x

Tactic:
simp only [Finset.mem_erase, Finset.mem_univ, and_true, Ne, Subtype.ext_iff] at ha1

Premises used: Finset.mem_univ, and_true, Ne, Subtype.ext_iff, Finset.mem_erase