Theorem: OnCycleFactors.hψ_range_card' (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Set.range ⇑(θ g)) = Fintype.card ↥(MonoidHom.ker (φ g))
Tactic:
let u : (Set.range (θ g)) → (φ g).ker := fun ⟨z, hz⟩ => by
  rw [← hφ_ker_eq_θ_range] at hz
  suffices ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g by
    use ⟨ConjAct.toConjAct z, this⟩
    have hK : Function.Injective (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g).subtype := by
      apply Subgroup.subtype_injective
    rw [← Subgroup.mem_map_iff_mem hK]
    simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
    exact hz
  obtain ⟨u, ⟨_, hu'⟩⟩ := hz
  rw [← hu']
  exact u.prop
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Fintype.card ↑(Set.range ⇑(θ g)) = Fintype.card ↥(MonoidHom.ker (φ g))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Fintype.card ↑(Set.range ⇑(θ g)) = Fintype.card ↥(MonoidHom.ker (φ g))
Tactic:
suffices Function.Bijective u by
  exact Fintype.card_of_bijective this
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Function.Bijective u

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Function.Bijective u
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Function.Injective u

case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Function.Surjective u

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz : z ∈ Set.range ⇑(θ g)
⊢ ↥(MonoidHom.ker (φ g))
Tactic:
rw [← hφ_ker_eq_θ_range] at hz
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
⊢ ↥(MonoidHom.ker (φ g))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
⊢ ↥(MonoidHom.ker (φ g))
Tactic:
suffices ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g by
  use ⟨ConjAct.toConjAct z, this⟩
  have hK : Function.Injective (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g).subtype := by
    apply Subgroup.subtype_injective
  rw [← Subgroup.mem_map_iff_mem hK]
  simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
  exact hz
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
⊢ ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
⊢ ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
obtain ⟨u, ⟨_, hu'⟩⟩ := hz
State after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
u : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
left✝ : u ∈ ↑(MonoidHom.ker (φ g))
hu' : (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) u = ConjAct.toConjAct z
⊢ ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g

State before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
u : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
left✝ : u ∈ ↑(MonoidHom.ker (φ g))
hu' : (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) u = ConjAct.toConjAct z
⊢ ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
rw [← hu']
State after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
u : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
left✝ : u ∈ ↑(MonoidHom.ker (φ g))
hu' : (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) u = ConjAct.toConjAct z
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) u ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g

State before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
u : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
left✝ : u ∈ ↑(MonoidHom.ker (φ g))
hu' : (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) u = ConjAct.toConjAct z
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) u ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
exact u.prop
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ ↥(MonoidHom.ker (φ g))
Tactic:
use ⟨ConjAct.toConjAct z, this⟩
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ { val := ConjAct.toConjAct z, property := this } ∈ MonoidHom.ker (φ g)

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ { val := ConjAct.toConjAct z, property := this } ∈ MonoidHom.ker (φ g)
Tactic:
have hK : Function.Injective (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g).subtype := by
  apply Subgroup.subtype_injective
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hK : Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
⊢ { val := ConjAct.toConjAct z, property := this } ∈ MonoidHom.ker (φ g)

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hK : Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
⊢ { val := ConjAct.toConjAct z, property := this } ∈ MonoidHom.ker (φ g)
Tactic:
rw [← Subgroup.mem_map_iff_mem hK]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hK : Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
      { val := ConjAct.toConjAct z, property := this } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hK : Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
⊢ (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
      { val := ConjAct.toConjAct z, property := this } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
Tactic:
simp only [Subgroup.coeSubtype, Subgroup.coe_mk]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hK : Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
⊢ ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hK : Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
⊢ ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
Tactic:
exact hz
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x✝ : ↑(Set.range ⇑(θ g))
z : Equiv.Perm α
hz :
  ConjAct.toConjAct z ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))
this : ConjAct.toConjAct z ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ Function.Injective ⇑(Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g))
Tactic:
apply Subgroup.subtype_injective
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card ↑(Set.range ⇑(θ g)) = Fintype.card ↥(MonoidHom.ker (φ g))
Tactic:
exact Fintype.card_of_bijective this
State after:
no goals

State before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Function.Injective u
Tactic:
rintro ⟨z, hz⟩ ⟨w, hw⟩ hzw
State after:
case left.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
z : Equiv.Perm α
hz : z ∈ Set.range ⇑(θ g)
w : Equiv.Perm α
hw : w ∈ Set.range ⇑(θ g)
hzw : u { val := z, property := hz } = u { val := w, property := hw }
⊢ { val := z, property := hz } = { val := w, property := hw }

State before:
case left.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
z : Equiv.Perm α
hz : z ∈ Set.range ⇑(θ g)
w : Equiv.Perm α
hw : w ∈ Set.range ⇑(θ g)
hzw : u { val := z, property := hz } = u { val := w, property := hw }
⊢ { val := z, property := hz } = { val := w, property := hw }
Tactic:
simpa only [u, Subtype.mk_eq_mk, MulEquiv.apply_eq_iff_eq] using hzw
State after:
no goals

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
⊢ Function.Surjective u
Tactic:
rintro ⟨w, hw⟩
State after:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ ∃ a, u a = { val := w, property := hw }

State before:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ ∃ a, u a = { val := w, property := hw }
Tactic:
use! ConjAct.ofConjAct ((MulAction.stabilizer (ConjAct (Equiv.Perm α)) g).subtype w)
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w) ∈ Set.range ⇑(θ g)

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ u
      { val := ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w),
        property := ?property } =
    { val := w, property := hw }

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w) ∈ Set.range ⇑(θ g)

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ u
      { val := ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w),
        property := ?property } =
    { val := w, property := hw }
Tactic:
rw [← hφ_ker_eq_θ_range]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ ConjAct.toConjAct (ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w)) ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ u
      { val := ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w),
        property := ⋯ } =
    { val := w, property := hw }

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ ConjAct.toConjAct (ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w)) ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) (MonoidHom.ker (φ g))

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ u
      { val := ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w),
        property := ⋯ } =
    { val := w, property := hw }
Tactic:
simp only [Subgroup.coeSubtype, ConjAct.toConjAct_ofConjAct, Subgroup.mem_map,
  SetLike.coe_eq_coe, exists_prop, exists_eq_right, hw]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ u
      { val := ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w),
        property := ⋯ } =
    { val := w, property := hw }

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : ↑(Set.range ⇑(θ g)) → ↥(MonoidHom.ker (φ g)) :=
  fun x =>
    match x with
    | { val := z, property := hz } =>
      let_fun this := ⋯;
      { val := { val := ConjAct.toConjAct z, property := this }, property := ⋯ }
w : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
hw : w ∈ MonoidHom.ker (φ g)
⊢ u
      { val := ConjAct.ofConjAct ((Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) w),
        property := ⋯ } =
    { val := w, property := hw }
Tactic:
simp only [u, Subgroup.coeSubtype, ConjAct.toConjAct_ofConjAct, Subtype.mk_eq_mk, SetLike.eta]
State after:
no goals