Theorem: OnCycleFactors.kerφ_le_alternating_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α ↔
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
rw [SetLike.le_def]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) ↔
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) ↔
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) →
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ((∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1) →
    ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) →
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
    Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
      ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
    Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
      ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
constructor
State after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ i ∈ Equiv.Perm.cycleType g, Odd i

case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

State before:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ i ∈ Equiv.Perm.cycleType g, Odd i

case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
exact odd_of_mem_kerφ h
State after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

State before:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
constructor
State after:
case mp.right.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1

case mp.right.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

State before:
case mp.right.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1

case mp.right.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
exact card_le_of_mem_kerφ h
State after:
case mp.right.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

State before:
case mp.right.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
exact count_le_one_of_mem_kerφ h
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ((∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1) →
    ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
Tactic:
rintro ⟨h_odd, h_fixed, h_count⟩ x hx
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ x ∈ alternatingGroup α

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ x ∈ Set.range ⇑(θ g)
Tactic:
suffices (OnCycleFactors.φ g).ker = ⊤ by
  rw [← OnCycleFactors.hφ_ker_eq_θ_range, this]
  simp only [Subgroup.coeSubtype, Subgroup.mem_map, Subgroup.mem_top, true_and]
  exact ⟨⟨x, hx⟩, rfl⟩
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ MonoidHom.ker (φ g) = ⊤

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ MonoidHom.ker (φ g) = ⊤
Tactic:
rw [eq_top_iff]
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ ⊤ ≤ MonoidHom.ker (φ g)

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ ⊤ ≤ MonoidHom.ker (φ g)
Tactic:
intro y _
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
⊢ y ∈ MonoidHom.ker (φ g)

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
⊢ y ∈ MonoidHom.ker (φ g)
Tactic:
suffices (OnCycleFactors.φ g).range = ⊥ by
  rw [MonoidHom.mem_ker, ← Subgroup.mem_bot, ← this, MonoidHom.mem_range]
  exact ⟨y, rfl⟩
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
⊢ MonoidHom.range (φ g) = ⊥

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
⊢ MonoidHom.range (φ g) = ⊥
Tactic:
rw [eq_bot_iff]
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
⊢ MonoidHom.range (φ g) ≤ ⊥

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
⊢ MonoidHom.range (φ g) ≤ ⊥
Tactic:
intro z
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z ∈ MonoidHom.range (φ g) → z ∈ ⊥

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z ∈ MonoidHom.range (φ g) → z ∈ ⊥
Tactic:
rw [← OnCycleFactors.Iφ_eq_range, Subgroup.mem_bot]
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z ∈ Iφ g → z = 1

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z ∈ Iφ g → z = 1
Tactic:
intro hz
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
⊢ z = 1

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
⊢ z = 1
Tactic:
apply Equiv.ext
State after:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
⊢ ∀ (x : ↑↑(Equiv.Perm.cycleFactorsFinset g)), z x = 1 x

State before:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
⊢ ∀ (x : ↑↑(Equiv.Perm.cycleFactorsFinset g)), z x = 1 x
Tactic:
intro c
State after:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z c = 1 c

State before:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z c = 1 c
Tactic:
rw [← Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleType_def,
  Multiset.nodup_map_iff_inj_on (Equiv.Perm.cycleFactorsFinset g).nodup]
  at h_count
State after:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count :
  ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val,
    ∀ y ∈ (Equiv.Perm.cycleFactorsFinset g).val,
      (Finset.card ∘ Equiv.Perm.support) x = (Finset.card ∘ Equiv.Perm.support) y → x = y
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z c = 1 c

State before:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count :
  ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val,
    ∀ y ∈ (Equiv.Perm.cycleFactorsFinset g).val,
      (Finset.card ∘ Equiv.Perm.support) x = (Finset.card ∘ Equiv.Perm.support) y → x = y
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ z c = 1 c
Tactic:
rw [Equiv.Perm.coe_one, id.def, ← Subtype.coe_inj]
State after:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count :
  ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val,
    ∀ y ∈ (Equiv.Perm.cycleFactorsFinset g).val,
      (Finset.card ∘ Equiv.Perm.support) x = (Finset.card ∘ Equiv.Perm.support) y → x = y
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(z c) = ↑c

State before:
case mpr.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count :
  ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val,
    ∀ y ∈ (Equiv.Perm.cycleFactorsFinset g).val,
      (Finset.card ∘ Equiv.Perm.support) x = (Finset.card ∘ Equiv.Perm.support) y → x = y
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
z : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hz : z ∈ Iφ g
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(z c) = ↑c
Tactic:
exact h_count (z c) (z c).prop c c.prop (hz c)
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : x ∈ Set.range ⇑(θ g)
⊢ x ∈ alternatingGroup α
Tactic:
obtain ⟨⟨y, uv⟩, rfl⟩ := Set.mem_range.mp hx'
State after:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (θ g) (y, uv) ∈ alternatingGroup α

State before:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (θ g) (y, uv) ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup, OnCycleFactors.sign_ψ]
State after:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Equiv.Perm.sign y * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(uv c)) = 1

State before:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Equiv.Perm.sign y * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(uv c)) = 1
Tactic:
convert mul_one _
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(uv c)) = 1

case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ 1 = Equiv.Perm.sign y

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(uv c)) = 1
Tactic:
apply Finset.prod_eq_one
State after:
case h.e'_2.h.e'_6.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ ∀ x ∈ Finset.univ, Equiv.Perm.sign ↑(uv x) = 1

State before:
case h.e'_2.h.e'_6.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ ∀ x ∈ Finset.univ, Equiv.Perm.sign ↑(uv x) = 1
Tactic:
rintro ⟨c, hc⟩ _
State after:
case h.e'_2.h.e'_6.h.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1

State before:
case h.e'_2.h.e'_6.h.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1
Tactic:
obtain ⟨k, hk⟩ := (uv _).prop
State after:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑?m.575606 ^ x) k = ↑(uv ?m.575606)
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1

State before:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑?m.575606 ^ x) k = ↑(uv ?m.575606)
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1
Tactic:
rw [← hk, map_zpow]
State after:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } ^ k = 1

State before:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } ^ k = 1
Tactic:
convert one_zpow k
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } = 1

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } = 1
Tactic:
simp only
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign c = 1

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign c = 1
Tactic:
rw [Equiv.Perm.IsCycle.sign, Odd.neg_one_pow, neg_neg]
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Odd (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Odd (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
apply h_odd
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ (Equiv.Perm.support c).card ∈ Equiv.Perm.cycleType g

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ (Equiv.Perm.support c).card ∈ Equiv.Perm.cycleType g

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
rw [Equiv.Perm.cycleType_def, Multiset.mem_map]
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
use c
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ c ∈ (Equiv.Perm.cycleFactorsFinset g).val ∧ (Finset.card ∘ Equiv.Perm.support) c = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ c ∈ (Equiv.Perm.cycleFactorsFinset g).val ∧ (Finset.card ∘ Equiv.Perm.support) c = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
exact ⟨hc, rfl⟩
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
rw [Equiv.Perm.mem_cycleFactorsFinset_iff] at hc
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc✝ : c ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
a✝ : { val := c, property := hc✝ } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc✝ } ^ x) k = ↑(uv { val := c, property := hc✝ })
⊢ Equiv.Perm.IsCycle c

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc✝ : c ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
a✝ : { val := c, property := hc✝ } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc✝ } ^ x) k = ↑(uv { val := c, property := hc✝ })
⊢ Equiv.Perm.IsCycle c
Tactic:
exact hc.left
State after:
no goals

State before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ 1 = Equiv.Perm.sign y
Tactic:
apply symm
State after:
case h.e'_3.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Equiv.Perm.sign y = 1

State before:
case h.e'_3.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Equiv.Perm.sign y = 1
Tactic:
convert Equiv.Perm.sign_one
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ y = 1

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ y = 1
Tactic:
rw [← Equiv.Perm.card_support_le_one]
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Equiv.Perm.support y).card ≤ 1

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Equiv.Perm.support y).card ≤ 1
Tactic:
apply le_trans (Finset.card_le_univ _)
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) ≤ 1

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) ≤ 1
Tactic:
change Fintype.card (MulAction.fixedBy α g) ≤ 1
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(MulAction.fixedBy α g) ≤ 1

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(MulAction.fixedBy α g) ≤ 1
Tactic:
rw [OnCycleFactors.Equiv.Perm.card_fixedBy g, tsub_le_iff_left]
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
Tactic:
exact h_fixed
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ x ∈ Set.range ⇑(θ g)
Tactic:
rw [← OnCycleFactors.hφ_ker_eq_θ_range, this]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ConjAct.toConjAct x ∈ Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ⊤

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ConjAct.toConjAct x ∈ Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ⊤
Tactic:
simp only [Subgroup.coeSubtype, Subgroup.mem_map, Subgroup.mem_top, true_and]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ∃ x_1, ↑x_1 = ConjAct.toConjAct x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ∃ x_1, ↑x_1 = ConjAct.toConjAct x
Tactic:
exact ⟨⟨x, hx⟩, rfl⟩
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
this : MonoidHom.range (φ g) = ⊥
⊢ y ∈ MonoidHom.ker (φ g)
Tactic:
rw [MonoidHom.mem_ker, ← Subgroup.mem_bot, ← this, MonoidHom.mem_range]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
this : MonoidHom.range (φ g) = ⊥
⊢ ∃ x, (φ g) x = (φ g) y

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
this : MonoidHom.range (φ g) = ⊥
⊢ ∃ x, (φ g) x = (φ g) y
Tactic:
exact ⟨y, rfl⟩
State after:
no goals