Theorem: OnCycleFactors.θAux_one (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
⊢ θAux g 1 1 x = x
Tactic:
unfold θAux
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
⊢ (if hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g then
      ↑(1 { val := Equiv.Perm.cycleOf g x, property := hx }) x
    else (Equiv.Perm.ofSubtype 1) x) =
    x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
⊢ (if hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g then
      ↑(1 { val := Equiv.Perm.cycleOf g x, property := hx }) x
    else (Equiv.Perm.ofSubtype 1) x) =
    x
Tactic:
split_ifs
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(1 { val := Equiv.Perm.cycleOf g x, property := h✝ }) x = x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype 1) x = x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(1 { val := Equiv.Perm.cycleOf g x, property := h✝ }) x = x
Tactic:
simp only [Pi.one_apply, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
h✝ : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype 1) x = x
Tactic:
simp only [map_one, Equiv.Perm.coe_one, id_eq]
State after:
no goals