internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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 α
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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⟩
Proof 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) = ⊤
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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]
Proof 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)
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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 _
Proof 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)
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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⟩
Proof 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) = ⊥
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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]
Proof 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) ≤ ⊥
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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 ∈ ⊥
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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]
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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)
Proof state after:
no goals
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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'
Proof 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 α
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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_ψ]
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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 _
Proof 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
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof 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
Proof 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