internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ ∃ a, u a = { val := x, property := hx }
Tactic:
use! x
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ x ∈ Equiv.Perm.cycleFactorsFinset g

case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ?property } ∈ {x | fsc x = { val := i, isLt := hi }}
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ x ∈ Equiv.Perm.cycleFactorsFinset g

case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ?property } ∈ {x | fsc x = { val := i, isLt := hi }}
Tactic:
exact hx.1
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ⋯ } ∈ {x | fsc x = { val := i, isLt := hi }}
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ⋯ } ∈ {x | fsc x = { val := i, isLt := hi }}
Tactic:
simp only [fsc, Fin.mk.injEq, Set.mem_setOf_eq]
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ (Equiv.Perm.support x).card = i
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ (Equiv.Perm.support x).card = i
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Function.Injective u
Tactic:
rintro ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ h
Proof state after:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h :
  u { val := { val := x, property := hx }, property := hx' } =
    u { val := { val := y, property := hy }, property := hy' }
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h :
  u { val := { val := x, property := hx }, property := hx' } =
    u { val := { val := y, property := hy }, property := hy' }
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }
Tactic:
simp only [Function.comp_apply, Set.coe_setOf, Set.mem_setOf_eq, Subtype.mk.injEq, u] at h
Proof state after:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h : x = y
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }
Theorem: OnCycleFactors.hφ_range_card
Proof state before:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h : x = y
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }
Tactic:
simp only [h, Set.coe_setOf, Set.mem_setOf_eq, Subtype.mk.injEq]
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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))
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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']
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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))
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_mem_ker_iff
Proof 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]
Proof 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