internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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))
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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
Theorem: OnCycleFactors.hψ_range_card'
Proof 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']
Proof 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
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card'
Proof 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⟩
Proof 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)
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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)
Theorem: OnCycleFactors.hψ_range_card'
Proof 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]
Proof 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))
Theorem: OnCycleFactors.hψ_range_card'
Proof 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]
Proof 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))
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof 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 }
Theorem: OnCycleFactors.hψ_range_card'
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hψ_range_card'
Proof 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⟩
Proof 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 }
Theorem: OnCycleFactors.hψ_range_card'
Proof 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)
Proof 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 }
Theorem: OnCycleFactors.hψ_range_card'
Proof 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]
Proof 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 }
Theorem: OnCycleFactors.hψ_range_card'
Proof 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]
Proof 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 }
Theorem: OnCycleFactors.hψ_range_card'
Proof 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]
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.card_fixedBy
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.fixedBy α g) = Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Tactic:
rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.fixedBy α g) = (Equiv.Perm.support g)ᶜ.card
Theorem: OnCycleFactors.Equiv.Perm.card_fixedBy
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.fixedBy α g) = (Equiv.Perm.support g)ᶜ.card
Tactic:
simp only [Fintype.card_ofFinset, Set.mem_compl_iff, Finset.mem_coe,
  Equiv.Perm.mem_support, Classical.not_not]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ).card = (Equiv.Perm.support g)ᶜ.card
Theorem: OnCycleFactors.Equiv.Perm.card_fixedBy
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ).card = (Equiv.Perm.support g)ᶜ.card
Tactic:
apply congr_arg
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ = (Equiv.Perm.support g)ᶜ
Theorem: OnCycleFactors.Equiv.Perm.card_fixedBy
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ = (Equiv.Perm.support g)ᶜ
Tactic:
ext x
Proof state after:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x : α
⊢ x ∈ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ ↔ x ∈ (Equiv.Perm.support g)ᶜ
Theorem: OnCycleFactors.Equiv.Perm.card_fixedBy
Proof state before:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x : α
⊢ x ∈ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ ↔ x ∈ (Equiv.Perm.support g)ᶜ
Tactic:
simp only [MulAction.mem_fixedBy, Equiv.Perm.smul_def, Finset.mem_filter, Finset.mem_univ,
  true_and_iff, Finset.mem_compl, Equiv.Perm.mem_support, Classical.not_not]
Proof state after:
no goals