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

Proof state:
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

Tactic:
simp only [zpowers_le]

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 }), ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Proof state:
case a.left.intro.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a * g = g * ofSubtype a

Tactic:
exact Disjoint.commute (disjoint_iff_disjoint_support.mpr (ofSubtype_support_disjoint a))

Result:
no goals

Proof state:
case a.left.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a ∈ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
refine ⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩

Result:
case a.left.intro.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a ∈ centralizer {g}

case a.left.intro.refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ⟨ofSubtype a, ?a.left.intro.refine_1✝⟩ ∈ ↑(toPermHom g).ker

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 x = x
⊢ (ofSubtype u) x = ↑p x

Tactic:
rwa [ofSubtype_apply_of_mem, subtypePerm_apply]

Result:
no goals

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

Tactic:
rintro - ⟨a, rfl⟩

Result:
case a.left.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a ∈ map (centralizer {g}).subtype (toPermHom g).ker

Proof state:
case a.left.intro.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a ∈ centralizer {g}

Tactic:
rw [mem_centralizer_singleton_iff]

Result:
case a.left.intro.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a * g = g * ofSubtype a

Proof state:
case pos.ha
α : 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
hx : g x ≠ x
⊢ x ∈ (↑⟨g.cycleOf x, hx✝⟩).support

Tactic:
rwa [mem_support, cycleOf_apply_self, ne_eq]

Result:
no goals

Proof state:
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

Tactic:
ext x

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 : α
⊢ ((kerParam g) (u, v)) x = ↑p x

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
⊢ ↑p ∈ (kerParam g).range

Tactic:
set v : (c : g.cycleFactorsFinset) → (Subgroup.zpowers c.val) :=
  fun c => ⟨ofSubtype
      (p.1.subtypePerm (Classical.choose (hp c.val c.prop))),
        Classical.choose_spec (hp c.val c.prop)⟩

Result:
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

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

Tactic:
exact Perm.ext fun x ↦ Subtype.ext (cycleFactorsFinset_mem_commute' g i.2 x.2).mul_inv_cancel

Result:
no goals

Proof state:
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 }), ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
constructor

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

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 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

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support] at 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
hx : g x ≠ x
⊢ ↑(v ⟨g.cycleOf x, hx✝⟩) x = ↑p x

Proof state:
case a.left.intro.refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ⟨ofSubtype a, ⋯⟩ ∈ ↑(toPermHom g).ker

Tactic:
exact Perm.ext fun x ↦ Subtype.ext (disjoint_iff_disjoint_support.mpr
  ((ofSubtype_support_disjoint a).mono_right
    (mem_cycleFactorsFinset_support_le x.2))).commute.mul_inv_cancel

Result:
no goals