awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
⊢ p ∈ f.cycleFactorsFinset ↔
    p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
have obtain : ∀ (l : List (Perm α)) (hl : l.Nodup) (hl' : l.toFinset = f.cycleFactorsFinset),
  p ∈ f.cycleFactorsFinset ↔
    p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
Tactic: obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ f.cycleFactorsFinset ↔
    p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
have rw : p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
Tactic: rw [← hl']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
have hl'₁ : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
Tactic: rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
Cleared hypotheses: hl'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support
have rw : ((f.cycleOf x).IsCycle ∧
    ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) ↔
  x ∈ f.support
Tactic: rw [mem_cycleFactorsFinset_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧
      ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) ↔
    x ∈ f.support
have mp : ((f.cycleOf x).IsCycle ∧
    ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) →
  x ∈ f.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
mp :
  ((f.cycleOf x).IsCycle ∧
      ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) →
    x ∈ f.support
⊢ ((f.cycleOf x).IsCycle ∧
      ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) ↔
    x ∈ f.support
have mpr : x ∈ f.support →
  (f.cycleOf x).IsCycle ∧
    ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hc : (f.cycleOf x).IsCycle
right : ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
⊢ x ∈ f.support
have mp : ∀ (hc : x ∉ f.support), ¬(f.cycleOf x).IsCycle
Tactic: contrapose hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
right : ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
hc : x ∉ f.support
⊢ ¬(f.cycleOf x).IsCycle
have hc₁ : f.cycleOf x = 1
Tactic: rw [notMem_support, ← cycleOf_eq_one_iff] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
⊢ (f.cycleOf x).IsCycle ∧
    ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
have mpr : ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
Tactic: refine ⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ∈ (f.cycleOf x).support
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
have hy₁ : (f.cycleOf x : (a : α) → α) y ≠ y
Tactic: rw [mem_support] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x : (a : α) → α) y ≠ y
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
have mpr : Eq (α := α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α) ((f : (a : α) → α) y : α)
Tactic: rw [cycleOf_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x : (a : α) → α) y ≠ y
⊢ Eq (α := α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α) ((f : (a : α) → α) y : α)
have pos : ∀ (H : f.SameCycle x y), Eq (α := α) ((f : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x : (a : α) → α) y ≠ y
pos : ∀ (H : f.SameCycle x y), Eq (α := α) ((f : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
⊢ Eq (α := α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α) ((f : (a : α) → α) y : α)
have neg : ∀ (H : ¬f.SameCycle x y), y = (f : (a : α) → α) y
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x : (a : α) → α) y ≠ y
H : ¬f.SameCycle x y
⊢ y = (f : (a : α) → α) y
have hy₁ : y ≠ y
Tactic: rw [cycleOf_apply_of_not_sameCycle H] at hy
Cleared hypotheses: hy, H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
have rw : g.cycleOf x ≠ 1 ↔ x ∈ g.support
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
rw : g.cycleOf x ≠ 1 ↔ x ∈ g.support
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
have rw₁ : g.cycleOf x ≠ 1 ↔ (g : (a : α) → α) x ≠ x
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
rw : g.cycleOf x ≠ 1 ↔ x ∈ g.support
rw₁ : g.cycleOf x ≠ 1 ↔ (g : (a : α) → α) x ≠ x
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
have rw₂ : ¬g.cycleOf x = 1 ↔ (g : (a : α) → α) x ≠ x
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
rw : g.cycleOf x ≠ 1 ↔ x ∈ g.support
rw₁ : g.cycleOf x ≠ 1 ↔ (g : (a : α) → α) x ≠ x
rw₂ : ¬g.cycleOf x = 1 ↔ (g : (a : α) → α) x ≠ x
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
have rw₃ : ¬(g : (a : α) → α) x = x ↔ (g : (a : α) → α) x ≠ x
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
p f : Perm α
h : p ∈ f.cycleFactorsFinset
⊢ p.support ≤ f.support
have h₁ : p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
Tactic: rw [mem_cycleFactorsFinset_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
x : α
hx : x ∈ p.support
⊢ x ∈ f.support
have rwa : (f : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← h.right x hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
x : α
hx : x ∈ p.support
rwa : (f : (a : α) → α) x ≠ x
⊢ x ∈ f.support
have rwa₁ : (p : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← h.right x hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
v : ↥(Subgroup.zpowers (↑c : Perm α))
⊢ (↑v : Perm α).support ≤ g.support
have obtain : ∀ (m : ℤ) (hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑v : Perm α)), (↑v : Perm α).support ≤ g.support
Tactic: obtain ⟨m, hm⟩ := v.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
v : ↥(Subgroup.zpowers (↑c : Perm α))
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑v : Perm α)
⊢ (↑v : Perm α).support ≤ g.support
have simp : ((↑c : Perm α) ^ m).support ≤ g.support
Tactic: simp only [← hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑c : Perm α)) x
hy : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑d : Perm α)) y
⊢ x.Disjoint y
have obtain : ∀ (m : ℤ) (hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = x), x.Disjoint y
Tactic: obtain ⟨m, hm⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
hy : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑d : Perm α)) y
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = x
⊢ x.Disjoint y
have obtain : ∀ (n : ℤ) (hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = y), x.Disjoint y
Tactic: obtain ⟨n, hn⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = x
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = y
⊢ x.Disjoint y
have simp : ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)
Tactic: simp only [← hm, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = x
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = y
⊢ ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)
have hστ : (↑c : Perm α).Disjoint (↑d : Perm α)
Tactic: apply Disjoint.zpow_disjoint_zpow
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 α))
⊢ 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)
have 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))
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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))
⊢ 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)
have 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)
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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)
⊢ 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)
have 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
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ 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)
have 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))
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 α))
a : ↥f.cycleFactorsFinset
h_1 : a ∈ (↑univ : Set ↥f.cycleFactorsFinset)
b : ↥f.cycleFactorsFinset
h_2 : b ∈ (↑univ : Set ↥f.cycleFactorsFinset)
h : a ≠ b
⊢ 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))
    a b
have comm : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑a : Perm α))
  ((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) :
        Perm α))
    a)
Tactic: apply f.pairwise_commute_of_mem_zpowers h