Theorem: OnCycleFactors.hφ_mem_ker_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g)) ↔
    ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g)) →
    ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ (∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t) →
    ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g)) →
    ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
intro hz
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
rw [Subgroup.mem_map] at hz
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
hz :
  ∃ x ∈ MonoidHom.ker (φ g),
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) x = ConjAct.toConjAct z
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
hz :
  ∃ x ∈ MonoidHom.ker (φ g),
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) x = ConjAct.toConjAct z
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
obtain ⟨⟨k, hkK⟩, hk, hk'⟩ := hz
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk : { val := k, property := hkK } ∈ MonoidHom.ker (φ g)
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk : { val := k, property := hkK } ∈ MonoidHom.ker (φ g)
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
simp only [MonoidHom.mem_ker] at hk
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
⊢ ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
Tactic:
intro t ht
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Commute z t

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Commute z t
Tactic:
change z * t = t * z
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ z * t = t * z

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ z * t = t * z
Tactic:
rw [← mul_inv_eq_iff_eq_mul, ← MulAut.conj_apply, ← ConjAct.ofConjAct_toConjAct z,
  ← ConjAct.smul_eq_mulAut_conj _ t, ← hk']
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } • t = t

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } • t = t
Tactic:
simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ k • t = t

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ k • t = t
Tactic:
simp only [← φ_eq g k hkK t ht, hk]
State after:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(1 { val := t, property := ht }) = t

State before:
case mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
k : ConjAct (Equiv.Perm α)
hkK : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hk' :
  (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := k, property := hkK } =
    ConjAct.toConjAct z
hk : (φ g) { val := k, property := hkK } = 1
t : Equiv.Perm α
ht : t ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(1 { val := t, property := ht }) = t
Tactic:
rfl
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
⊢ (∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t) →
    ConjAct.toConjAct z ∈
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
Tactic:
intro H
State after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
Tactic:
rw [Subgroup.mem_map]
State after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ∃ x ∈ MonoidHom.ker (φ g),
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) x = ConjAct.toConjAct z

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ∃ x ∈ MonoidHom.ker (φ g),
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) x = ConjAct.toConjAct z
Tactic:
use! ConjAct.toConjAct z
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ { val := ConjAct.toConjAct z, property := ?property } ∈ MonoidHom.ker (φ g) ∧
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
        { val := ConjAct.toConjAct z, property := ?property } =
      ConjAct.toConjAct z

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ { val := ConjAct.toConjAct z, property := ⋯ } ∈ MonoidHom.ker (φ g) ∧
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := ConjAct.toConjAct z, property := ⋯ } =
      ConjAct.toConjAct z
Tactic:
simp only [MonoidHom.mem_ker]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (φ g) { val := ConjAct.toConjAct z, property := ⋯ } = 1 ∧
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := ConjAct.toConjAct z, property := ⋯ } =
      ConjAct.toConjAct z

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (φ g) { val := ConjAct.toConjAct z, property := ⋯ } = 1 ∧
    (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := ConjAct.toConjAct z, property := ⋯ } =
      ConjAct.toConjAct z
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (φ g) { val := ConjAct.toConjAct z, property := ⋯ } = 1

case h.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := ConjAct.toConjAct z, property := ⋯ } =
    ConjAct.toConjAct z

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
rw [MulAction.mem_stabilizer_iff]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.toConjAct z • g = g

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.toConjAct z • g = g
Tactic:
rw [ConjAct.smul_eq_mulAut_conj]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (MulAut.conj (ConjAct.ofConjAct (ConjAct.toConjAct z))) g = g

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (MulAut.conj (ConjAct.ofConjAct (ConjAct.toConjAct z))) g = g
Tactic:
rw [MulAut.conj_apply]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g * (ConjAct.ofConjAct (ConjAct.toConjAct z))⁻¹ = g

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g * (ConjAct.ofConjAct (ConjAct.toConjAct z))⁻¹ = g
Tactic:
rw [mul_inv_eq_iff_eq_mul]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g = g * ConjAct.ofConjAct (ConjAct.toConjAct z)

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ ConjAct.ofConjAct (ConjAct.toConjAct z) * g = g * ConjAct.ofConjAct (ConjAct.toConjAct z)
Tactic:
rw [ConjAct.ofConjAct_toConjAct]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ z * g = g * z

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ z * g = g * z
Tactic:
exact Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute z g H
State after:
no goals

State before:
case h.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (φ g) { val := ConjAct.toConjAct z, property := ⋯ } = 1
Tactic:
ext ⟨c, hc⟩
State after:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ ↑(((φ g) { val := ConjAct.toConjAct z, property := ⋯ }) { val := c, property := hc }) x✝ =
    ↑(1 { val := c, property := hc }) x✝

State before:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ ↑(((φ g) { val := ConjAct.toConjAct z, property := ⋯ }) { val := c, property := hc }) x✝ =
    ↑(1 { val := c, property := hc }) x✝
Tactic:
rw [φ_eq']
State after:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (z * c * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝

State before:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (z * c * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝
Tactic:
rw [H c hc]
State after:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (c * z * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝

State before:
case h.left.H.mk.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x✝ : α
⊢ (c * z * z⁻¹) x✝ = ↑(1 { val := c, property := hc }) x✝
Tactic:
simp only [mul_inv_cancel_right, Equiv.Perm.coe_one, id.def, Subtype.coe_mk]
State after:
no goals

State before:
case h.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Equiv.Perm α
H : ∀ t ∈ Equiv.Perm.cycleFactorsFinset g, Commute z t
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) { val := ConjAct.toConjAct z, property := ⋯ } =
    ConjAct.toConjAct z
Tactic:
simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
State after:
no goals