-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem cycleType_kerParam_apply_apply :
    cycleType (kerParam g ⟨k, v⟩) = cycleType k + ∑ c, (v c).val.cycleType

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c : { x // x ∈ g.cycleFactorsFinset }, (↑(v c)).cycleType

Tactic:
have hU : U.Pairwise fun i j ↦ (v i).val.Disjoint (v j).val := fun c _ d _ h ↦ by
  obtain ⟨m, hm⟩ := (v c).prop
  obtain ⟨n, hn⟩ := (v d).prop
  simp only [← hm, ← hn]
  apply Disjoint.zpow_disjoint_zpow
  apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop
  exact Subtype.coe_ne_coe.mpr h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
hU : U.Pairwise fun i j => (↑(v i)).Disjoint ↑(v j)
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c : { x // x ∈ g.cycleFactorsFinset }, (↑(v c)).cycleType

Proof state:
case intro.intro.hστ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ (↑c).Disjoint ↑d

Tactic:
apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop

Result:
case intro.intro.hστ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ ↑c ≠ ↑d

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c : { x // x ∈ g.cycleFactorsFinset }, (↑(v c)).cycleType

Tactic:
let U := (Finset.univ : Finset { x // x ∈ g.cycleFactorsFinset }).toSet

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c : { x // x ∈ g.cycleFactorsFinset }, (↑(v c)).cycleType

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ (↑(v c)).Disjoint ↑(v d)

Tactic:
simp only [← hm, ← hn]

Result:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ (↑c ^ m).Disjoint (↑d ^ n)

Proof state:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ (↑(v c)).Disjoint ↑(v d)

Tactic:
obtain ⟨n, hn⟩ := (v d).prop

Result:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ (↑(v c)).Disjoint ↑(v d)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
hU : U.Pairwise fun i j => (↑(v i)).Disjoint ↑(v j)
⊢ (ofSubtype k).cycleType + ∑ i ∈ g.cycleFactorsFinset.attach, (↑(v i)).cycleType =
    k.cycleType + ∑ c ∈ g.cycleFactorsFinset.attach, (↑(v c)).cycleType

Tactic:
exact congr_arg₂ _ cycleType_ofSubtype rfl

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ (↑c ^ m).Disjoint (↑d ^ n)

Tactic:
apply Disjoint.zpow_disjoint_zpow

Result:
case intro.intro.hστ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ (↑c).Disjoint ↑d

Proof state:
case intro.intro.hστ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
n : ℤ
hn : (fun x => ↑d ^ x) n = ↑(v d)
⊢ ↑c ≠ ↑d

Tactic:
exact Subtype.coe_ne_coe.mpr h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
⊢ (fun i j => (↑(v i)).Disjoint ↑(v j)) c d

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

Result:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
c : { x // x ∈ g.cycleFactorsFinset }
x✝¹ : c ∈ U
d : { x // x ∈ g.cycleFactorsFinset }
x✝ : d ∈ U
h : c ≠ d
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ (↑(v c)).Disjoint ↑(v d)