-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
comm :
  (↑univ : Set ↥f.cycleFactorsFinset).Pairwise
    (onFun (β := Perm α) Commute fun (i : ↥f.cycleFactorsFinset) ↦
      ((fun (i : ↥f.cycleFactorsFinset) ↦
              (Subgroup.subtype
                  ((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) :
                ↥((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) →*
                  Perm α))
            i :
          (a :
              (fun (i : ↥f.cycleFactorsFinset) ↦
                  ↥((fun (i : ↥f.cycleFactorsFinset) ↦ Subgroup.zpowers (↑i : Perm α)) i))
                i) →
            Perm α)
        (v i))
hom :
  ∀ (a b : Perm α),
    Disjoint
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
          u)
        a →
      Disjoint
          ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
            u)
          b →
        Disjoint
          ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
            u)
          (a * b)
unit :
  Disjoint.{u_2} (α := α)
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    1
base :
  ∀ (x : ↥f.cycleFactorsFinset),
    Membership.mem (γ := Finset ↥f.cycleFactorsFinset) univ x →
      Disjoint.{u_2} (α := α)
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
          u)
        (((fun (i : ↥f.cycleFactorsFinset) ↦
                (Subgroup.subtype
                    ((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) :
                  ↥((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) →*
                    Perm α))
              x :
            (a :
                (fun (i : ↥f.cycleFactorsFinset) ↦
                    ↥((fun (i : ↥f.cycleFactorsFinset) ↦ Subgroup.zpowers (↑i : Perm α)) i))
                  x) →
              Perm α)
          (v x))
⊢ Disjoint.{u_2} (α := α)
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    ((Subgroup.noncommPiCoprod ⋯ : (a : (i : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑i : Perm α))) → Perm α) v)

Tactic:
apply Finset.noncommProd_induction

Premises used: Finset.noncommProd_induction