-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_range_eq :
    (kerParam g).range = (toPermHom g).ker.map (Subgroup.subtype _)

Proof state:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
⊢ ↑p ∈ (kerParam g).range

Tactic:
use (u, v)

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
⊢ (kerParam g) (u, v) = ↑p

Proof state:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
i : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
refine ⟨⟨i, mem_centralizer_singleton_iff.mpr (self_mem_cycle_factors_commute i.2)⟩, ?_, rfl⟩

Result:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
i : { x // x ∈ g.cycleFactorsFinset }
⊢ ⟨↑i, ⋯⟩ ∈ ↑(toPermHom g).ker

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ map (centralizer {g}).subtype (toPermHom g).ker ≤ (kerParam g).range

Tactic:
rintro - ⟨p, hp, rfl⟩

Result:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
⊢ (centralizer {g}).subtype p ∈ (kerParam g).range

Proof state:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
⊢ ↑p ∈ (kerParam g).range

Tactic:
set u : Perm (Function.fixedPoints g) :=
  subtypePerm p (fun x ↦ mem_fixedPoints_iff_apply_mem_of_mem_centralizer p.2)

Result:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
⊢ ↑p ∈ (kerParam g).range

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range = map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range ≤ map (centralizer {g}).subtype (toPermHom g).ker

case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ map (centralizer {g}).subtype (toPermHom g).ker ≤ (kerParam g).range

Proof state:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
⊢ (centralizer {g}).subtype p ∈ (kerParam g).range

Tactic:
simp only [coe_subtype]

Result:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
⊢ ↑p ∈ (kerParam g).range

Proof state:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ ((kerParam g) (u, v)) x = ↑p x

Tactic:
rw [kerParam_apply]

Result:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x) = ↑p x

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ (ofSubtype u) x = ↑p x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, not_mem_support] at hx

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx : g x = x
⊢ (ofSubtype u) x = ↑p x

Proof state:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ (i : { x // x ∈ g.cycleFactorsFinset }), ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
intro i

Result:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
i : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Proof state:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x) = ↑p x

Tactic:
split_ifs with hx

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ↑(v ⟨g.cycleOf x, hx⟩) x = ↑p x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ (ofSubtype u) x = ↑p x

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range ≤ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_range, sup_le_iff, noncommPiCoprod_range, iSup_le_iff]

Result:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    ∀ (i : { x // x ∈ g.cycleFactorsFinset }), zpowers ↑i ≤ map (centralizer {g}).subtype (toPermHom g).ker