awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
inl : ∀ (h2 : g1 ∈ f.cycleFactorsFinset), Commute g1 g1
inr : ∀ (h : g1 ≠ g2), Commute g1 g2
⊢ Commute g1 g2

Tactic:
rcases eq_or_ne g1 g2 with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g1 : Perm α
h1 h2 : g1 ∈ f.cycleFactorsFinset
⊢ Commute g1 g1

Tactic:
apply Commute.refl

Premises used: Commute.refl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2

Tactic:
Equiv.Perm.cycleFactorsFinset_mem_commute f h1 h2 h

Premises used: Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2

Tactic:
exact Equiv.Perm.cycleFactorsFinset_mem_commute f h1 h2 h

Premises used: Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
comm : (↑f.cycleFactorsFinset : Set (Perm α)).Pairwise Commute
⊢ f.cycleFactorsFinset.noncommProd id comm = f

Tactic:
(cycleFactorsFinset_eq_finset.mp rfl).2.choose_spec

Premises used: Exists.choose_spec, Equiv.Perm.cycleFactorsFinset_eq_finset, And.right, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
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 : α)
⊢ 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

Premises used: Equiv.Perm.cycleFactorsFinset, Finset.exists_list_nodup_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
rw : p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
⊢ p ∈ f.cycleFactorsFinset ↔
    p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)

Tactic:
rw [← hl']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f

Tactic:
rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'

Premises used: eq_comm, Equiv.Perm.cycleFactorsFinset_eq_list_toFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)

Tactic:
simpa [List.mem_toFinset, Ne, ← hl'.right.right] using
    mem_list_cycles_iff hl'.left hl'.right.left

Premises used: List.mem_toFinset, Equiv.Perm.mem_list_cycles_iff, Ne, And.right, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
rw :
  ((f.cycleOf x).IsCycle ∧
      ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) ↔
    x ∈ f.support
⊢ f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support

Tactic:
rw [mem_cycleFactorsFinset_iff]

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
mpr :
  x ∈ f.support →
    (f.cycleOf x).IsCycle ∧
      ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
⊢ ((f.cycleOf x).IsCycle ∧
      ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) ↔
    x ∈ f.support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 : α)
mp : ∀ (hc : x ∉ f.support), ¬(f.cycleOf x).IsCycle
⊢ x ∈ f.support

Tactic:
contrapose hc
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 = 1

Tactic:
rw [notMem_support, ← cycleOf_eq_one_iff] at hc

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.cycleOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 : f.cycleOf x = 1
⊢ ¬(f.cycleOf x).IsCycle

Tactic:
simp [hc]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 : α)

Tactic:
⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩

Premises used: Equiv.Perm.isCycle_cycleOf, Equiv.Perm.mem_support, And.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
mpr : ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
⊢ (f.cycleOf x).IsCycle ∧
    ∀ a ∈ (f.cycleOf x).support, Eq (α := α) ((f.cycleOf x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)

Tactic:
refine ⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ∈ (f.cycleOf x).support
⊢ (f.cycleOf x : (a : α) → α) y ≠ y

Tactic:
rw [mem_support] at hy

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x : (a : α) → α) y ≠ y
mpr : Eq (α := α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α) ((f : (a : α) → α) y : α)
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)

Tactic:
rw [cycleOf_apply]

Premises used: Equiv.Perm.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 : α)
neg : ∀ (H : ¬f.SameCycle x y), y = (f : (a : α) → α) y
⊢ Eq (α := α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α) ((f : (a : α) → α) y : α)

Tactic:
split_ifs with H
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
⊢ Eq (α := α) ((f : (a : α) → α) y : α) ((f : (a : α) → α) y : α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 ≠ y

Tactic:
rw [cycleOf_apply_of_not_sameCycle H] at hy

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
hy₁ : y ≠ y
⊢ ¬f.SameCycle x y

Tactic:
rw [cycleOf_apply_of_not_sameCycle H] at hy

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ≠ y
H : ¬f.SameCycle x y
⊢ y = (f : (a : α) → α) y

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
rw₃ rw₄ : ¬(g : (a : α) → α) x = x ↔ (g : (a : α) → α) x ≠ x
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]

Premises used: Equiv.Perm.cycleOf_eq_one_iff, Equiv.Perm.mem_support, ne_eq, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
p f : Perm α
h : p ∈ f.cycleFactorsFinset
⊢ p.IsCycle ∧ ∀ a ∈ p.support, Eq (α := α) ((p : (a : α) → α) a : α) ((f : (a : α) → α) a : α)

Tactic:
rw [mem_cycleFactorsFinset_iff] at h

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
rwa₁ : (p : (a : α) → α) x ≠ x
rwa₂ rwa₃ rwa₄ rwa₅ : x ∈ p.support
⊢ x ∈ f.support

Tactic:
rwa [mem_support, ← h.right x hx, ← mem_support]

Premises used: Equiv.Perm.mem_support, And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
v : ↥(Subgroup.zpowers (↑c : Perm α))
obtain : ∀ (m : ℤ) (hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑v : Perm α)), (↑v : Perm α).support ≤ g.support
⊢ (↑v : Perm α).support ≤ g.support

Tactic:
obtain ⟨m, hm⟩ := v.prop

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 α)
simp : ((↑c : Perm α) ^ m).support ≤ g.support
⊢ (↑v : Perm α).support ≤ g.support

Tactic:
simp only [← hm]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 α)
⊢ ((↑c : Perm α) ^ m).support ≤ g.support

Tactic:
le_trans (support_zpow_le _ _) (mem_cycleFactorsFinset_support_le c.prop)

Premises used: Equiv.Perm.support_zpow_le, Subtype.prop, Equiv.Perm.mem_cycleFactorsFinset_support_le, le_trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 α)
⊢ ((↑c : Perm α) ^ m).support ≤ g.support

Tactic:
exact le_trans (support_zpow_le _ _) (mem_cycleFactorsFinset_support_le c.prop)

Premises used: Equiv.Perm.support_zpow_le, Subtype.prop, Equiv.Perm.mem_cycleFactorsFinset_support_le, le_trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
obtain : ∀ (m : ℤ) (hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = x), x.Disjoint y
⊢ x.Disjoint y

Tactic:
obtain ⟨m, hm⟩ := hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
obtain : ∀ (n : ℤ) (hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = y), x.Disjoint y
⊢ x.Disjoint y

Tactic:
obtain ⟨n, hn⟩ := hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
simp : ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)
⊢ x.Disjoint y

Tactic:
simp only [← hm, ← hn]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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
hστ : (↑c : Perm α).Disjoint (↑d : Perm α)
⊢ ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)

Tactic:
apply Disjoint.zpow_disjoint_zpow

Premises used: Equiv.Perm.Disjoint.zpow_disjoint_zpow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 α).Disjoint (↑d : Perm α)

Tactic:
f.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr hcd)

Premises used: Iff.mpr, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Subtype.prop, Subtype.coe_ne_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
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 α).Disjoint (↑d : Perm α)

Tactic:
exact f.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr hcd)

Premises used: Iff.mpr, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Subtype.prop, Subtype.coe_ne_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ Pairwise fun (i j : ↥f.cycleFactorsFinset) ↦
    ∀ (x y : Perm α),
      Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑i : Perm α)) x →
        Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑j : Perm α)) y → Commute x y

Tactic:
f.pairwise_disjoint_of_mem_zpowers.mono
    (fun _ _ ↦ forall₂_imp (fun _ _ h hx hy ↦ (h hx hy).commute))

Premises used: Equiv.Perm.Disjoint.commute, forall₂_imp, Equiv.Perm.pairwise_disjoint_of_mem_zpowers, Pairwise.mono
-- 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 α))
a : ↥f.cycleFactorsFinset
comm :
  a ∈ (↑univ : Set ↥f.cycleFactorsFinset) →
    ∀ ⦃y : ↥f.cycleFactorsFinset⦄,
      y ∈ (↑univ : Set ↥f.cycleFactorsFinset) →
        a ≠ y →
          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 y
⊢ a ∈ (↑univ : Set ↥f.cycleFactorsFinset) →
    ∀ ⦃y : ↥f.cycleFactorsFinset⦄,
      y ∈ (↑univ : Set ↥f.cycleFactorsFinset) →
        a ≠ y →
          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 y

Tactic:
_
-- 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 α))
a : ↥f.cycleFactorsFinset
h : a ∈ (↑univ : Set ↥f.cycleFactorsFinset)
b : ↥f.cycleFactorsFinset
comm :
  b ∈ (↑univ : Set ↥f.cycleFactorsFinset) →
    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
⊢ b ∈ (↑univ : Set ↥f.cycleFactorsFinset) →
    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

Tactic:
_
-- 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 α))
a : ↥f.cycleFactorsFinset
h_1 : a ∈ (↑univ : Set ↥f.cycleFactorsFinset)
b : ↥f.cycleFactorsFinset
h_2 : b ∈ (↑univ : Set ↥f.cycleFactorsFinset)
h : a ≠ b
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)
comm₁ :
  Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑b : 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 α))
      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

Tactic:
apply f.pairwise_commute_of_mem_zpowers h

Premises used: Equiv.Perm.pairwise_commute_of_mem_zpowers
-- 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 α))
a : ↥f.cycleFactorsFinset
h_1 : a ∈ (↑univ : Set ↥f.cycleFactorsFinset)
b : ↥f.cycleFactorsFinset
h_2 : b ∈ (↑univ : Set ↥f.cycleFactorsFinset)
h : a ≠ b
⊢ 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:
simp only [Subgroup.coe_subtype, SetLike.coe_mem]

Premises used: SetLike.coe_mem, Subgroup.coe_subtype