-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_apply {u : Perm (Function.fixedPoints g)}
    {v : (c : g.cycleFactorsFinset) → Subgroup.zpowers c.val} {x : α} :
    kerParam g (u,v) x =
    if hx : g.cycleOf x ∈ g.cycleFactorsFinset
    then (v ⟨g.cycleOf x, hx⟩ : Perm α) x
    else ofSubtype u x

Proof state:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v a).2

Result:
case pos.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k : ℤ
hk : ↑a ^ k = ↑(v a)
⊢ x ∈ Function.fixedPoints ⇑g

Proof state:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
have key := cycleFactorsFinset_pairwise_disjoint g a.2 hx ha1

Result:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
key : (↑a).Disjoint (g.cycleOf x)
⊢ x ∈ Function.fixedPoints ⇑g

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx hx' : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, Ne, ← Function.mem_fixedPoints_iff] at hx'

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Proof state:
case pos.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k : ℤ
hk : ↑a ^ k = ↑(v a)
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
replace ha2 := key (support_zpow_le a.1 k (hk ▸ ha2))

Result:
case pos.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k : ℤ
hk : ↑a ^ k = ↑(v a)
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉ (g.cycleOf x).support
⊢ x ∈ Function.fixedPoints ⇑g

Proof state:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha1 : a ∈ Finset.univ.erase ⟨g.cycleOf x, hx⟩
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
simp only [Finset.mem_erase, Finset.mem_univ, and_true, Ne, Subtype.ext_iff] at ha1

Result:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
a : { x // x ∈ g.cycleFactorsFinset }
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
⊢ x ∈ Function.fixedPoints ⇑g

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq,
  ← not_mem_support]

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ x ∉ ((noncommPiCoprod ⋯) (u, v).2).support

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ x ∉ ((noncommPiCoprod ⋯) (u, v).2).support

Tactic:
contrapose! hx

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : x ∈ ((noncommPiCoprod ⋯) (u, v).2).support
⊢ x ∈ g.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
⊢ ((kerParam g) (u, v)) x =
    if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x

Tactic:
split_ifs with hx

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x