-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
lemma disjoint_ofSubtype_noncommPiCoprod (u : Perm (Function.fixedPoints f))
    (v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) :
    Disjoint (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v)

Proof state:
case comm
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ (↑univ).Pairwise (Commute on fun i => ((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) i) (v i))

Tactic:
intro a _ b _ h

Result:
case comm
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
a : { x // x ∈ f.cycleFactorsFinset }
a✝¹ : a ∈ ↑univ
b : { x // x ∈ f.cycleFactorsFinset }
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (Commute on fun i => ((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) i) (v i)) a b

Proof state:
case comm
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
a : { x // x ∈ f.cycleFactorsFinset }
a✝¹ : a ∈ ↑univ
b : { x // x ∈ f.cycleFactorsFinset }
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (Commute on fun i => ((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) i) (v i)) a b

Tactic:
apply f.pairwise_commute_of_mem_zpowers h <;> simp only [Subgroup.coe_subtype, SetLike.coe_mem]

Result:
no goals

Proof state:
case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ (a b : Perm α), (ofSubtype u).Disjoint a → (ofSubtype u).Disjoint b → (ofSubtype u).Disjoint (a * b)

Tactic:
intro x y

Result:
case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
x y : Perm α
⊢ (ofSubtype u).Disjoint x → (ofSubtype u).Disjoint y → (ofSubtype u).Disjoint (x * y)

Proof state:
case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ f.cycleFactorsFinset }
a✝ : c ∈ univ
⊢ (ofSubtype u).Disjoint (((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) c) (v c))

Tactic:
simp only [Subgroup.coe_subtype]

Result:
case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ f.cycleFactorsFinset }
a✝ : c ∈ univ
⊢ (ofSubtype u).Disjoint ↑(v c)

Proof state:
case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
x y : Perm α
⊢ (ofSubtype u).Disjoint x → (ofSubtype u).Disjoint y → (ofSubtype u).Disjoint (x * y)

Tactic:
exact Disjoint.mul_right

Result:
no goals

Proof state:
case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) x) (v x))

Tactic:
intro c _

Result:
case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ f.cycleFactorsFinset }
a✝ : c ∈ univ
⊢ (ofSubtype u).Disjoint (((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) c) (v c))

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint ((Subgroup.noncommPiCoprod ⋯) v)

Tactic:
apply Finset.noncommProd_induction

Result:
case comm
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ (↑univ).Pairwise (Commute on fun i => ((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) i) (v i))

case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ (a b : Perm α), (ofSubtype u).Disjoint a → (ofSubtype u).Disjoint b → (ofSubtype u).Disjoint (a * b)

case unit
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint 1

case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i => ((fun i => Subgroup.zpowers ↑i) i).subtype) x) (v x))

Proof state:
case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ f.cycleFactorsFinset }
a✝ : c ∈ univ
⊢ (ofSubtype u).Disjoint ↑(v c)

Tactic:
exact Disjoint.mono (disjoint_ofSubtype_of_memFixedPoints_self u)
  le_rfl (support_zpowers_of_mem_cycleFactorsFinset_le (v c))

Result:
no goals

Proof state:
case unit
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : { x // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint 1

Tactic:
exact disjoint_one_right _

Result:
no goals