-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem toCentralizer_equivariant :
    (toCentralizer a τ) • c = (τ : Perm g.cycleFactorsFinset) c

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
have := ofPermHomFun_commute_zpow_apply a τ x 1

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ ((g ^ 1) x) = (g ^ 1) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
⊢ ↑(a.toCentralizer τ) * ↑c = ↑(↑τ c) * ↑(a.toCentralizer τ)

Tactic:
ext x

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
⊢ (↑(a.toCentralizer τ) * ↑c) x = (↑(↑τ c) * ↑(a.toCentralizer τ)) x

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
rw [not_mem_support.mp hx, eq_comm, ← not_mem_support,
  ofPermHomFun_apply_mem_support_cycle_iff]

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ x ∉ (↑c).support

Proof state:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support

Tactic:
rw [ofPermHomFun_apply_mem_support_cycle_iff]

Result:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ x ∈ (↑c).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
⊢ a.toCentralizer τ • c = ↑τ c

Tactic:
simp only [← Subtype.coe_inj, val_centralizer_smul, InvMemClass.coe_inv, mul_inv_eq_iff_eq_mul]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
⊢ ↑(a.toCentralizer τ) * ↑c = ↑(↑τ c) * ↑(a.toCentralizer τ)

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ x ∉ (↑c).support

Tactic:
exact hx

Result:
no goals

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
⊢ (↑(a.toCentralizer τ) * ↑c) x = (↑(↑τ c) * ↑(a.toCentralizer τ)) x

Tactic:
simp only [mul_apply, toCentralizer_apply]

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
rw [this, ← (mem_cycleFactorsFinset_iff.mp ((τ : Perm g.cycleFactorsFinset) c).prop).2]

Result:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support

Proof state:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ x ∈ (↑c).support

Tactic:
exact hx

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
rw [(mem_cycleFactorsFinset_iff.mp c.prop).2 x hx]

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ ((g ^ 1) x) = (g ^ 1) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
simp only [zpow_one] at this

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
by_cases hx : x ∈ c.val.support

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : { x // x ∈ g.cycleFactorsFinset }
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)