internlm/Lean-Github huggingface dataset:
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ alternatingGroup α ≤ G
Tactic:
exfalso
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ False
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ False
Tactic:
exact Subgroup.index_ne_zero_of_finite h
Proof state after:
no goals
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Subgroup.index G = Nat.succ 0
⊢ alternatingGroup α ≤ G
Tactic:
rw [Subgroup.index_eq_one] at h
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ G
Tactic:
rw [h]
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ ⊤
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ ⊤
Tactic:
exact le_top
Proof state after:
no goals
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2
Tactic:
rw [mul_comm, Subgroup.index_mul_card, mul_comm]
Proof state after:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
exact hG
Proof state after:
no goals
Theorem: contains_alternating_of_index_le_2'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ alternatingGroup α ≤ G
Tactic:
apply large_subgroup_of_perm_contains_alternating
Proof state after:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Theorem: contains_alternating_of_index_le_2'
Proof state before:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
rw [← Subgroup.index_mul_card G]
Proof state after:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Subgroup.index G * Fintype.card ↥G ≤ 2 * Fintype.card ↥G
Theorem: contains_alternating_of_index_le_2'
Proof state before:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Subgroup.index G * Fintype.card ↥G ≤ 2 * Fintype.card ↥G
Tactic:
apply Nat.mul_le_mul_right _ hG
Proof state after:
no goals
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : orderOf g ∣ 2 ^ n
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
rw [← Equiv.Perm.lcm_cycleType] at hg
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
rw [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_of_cycleType] at hg0
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
have hg4 : g.cycleType.sum ≤ 4 := by
  rw [← hα4, Equiv.Perm.sum_cycleType]
  apply Finset.card_le_univ
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
by_cases h4 : 4 ∈ g.cycleType
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
Tactic:
rw [← hα4, Equiv.Perm.sum_cycleType]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Tactic:
apply Finset.card_le_univ
Proof state after:
no goals
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
exfalso
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ False
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ False
Tactic:
suffices g.cycleType = {4} by
  rw [this, ← Units.eq_iff] at hg0 ; norm_num at hg0
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Equiv.Perm.cycleType g = {4}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Equiv.Perm.cycleType g = {4}
Tactic:
rw [← Multiset.cons_erase h4]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ 4 ::ₘ Multiset.erase (Equiv.Perm.cycleType g) 4 = {4}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ 4 ::ₘ Multiset.erase (Equiv.Perm.cycleType g) 4 = {4}
Tactic:
apply symm
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ {4} = 4 ::ₘ Multiset.erase (Equiv.Perm.cycleType g) 4
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ {4} = 4 ::ₘ Multiset.erase (Equiv.Perm.cycleType g) 4
Tactic:
rw [Multiset.singleton_eq_cons_iff]
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ 4 = 4 ∧ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ 4 = 4 ∧ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Tactic:
apply And.intro rfl
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Tactic:
rw [← Multiset.cons_erase h4] at hg4
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (4 ::ₘ Multiset.erase (Equiv.Perm.cycleType g) 4) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (4 ::ₘ Multiset.erase (Equiv.Perm.cycleType g) 4) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
⊢ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Tactic:
simp only [Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff, Multiset.sum_eq_zero_iff] at hg4
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
⊢ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
⊢ Multiset.erase (Equiv.Perm.cycleType g) 4 = 0
Tactic:
ext x
Proof state after:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
⊢ Multiset.count x (Multiset.erase (Equiv.Perm.cycleType g) 4) = Multiset.count x 0
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
⊢ Multiset.count x (Multiset.erase (Equiv.Perm.cycleType g) 4) = Multiset.count x 0
Tactic:
simp only [Multiset.count_zero, Multiset.count_eq_zero]
Proof state after:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
⊢ x ∉ Multiset.erase (Equiv.Perm.cycleType g) 4
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
⊢ x ∉ Multiset.erase (Equiv.Perm.cycleType g) 4
Tactic:
intro hx
Proof state after:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
hx : x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4
⊢ False
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
hx : x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4
⊢ False
Tactic:
apply not_le.mpr (Equiv.Perm.one_lt_of_mem_cycleType (Multiset.mem_of_mem_erase hx))
Proof state after:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
hx : x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4
⊢ x ≤ 1
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
hx : x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4
⊢ x ≤ 1
Tactic:
rw [hg4 x hx]
Proof state after:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
hx : x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4
⊢ 0 ≤ 1
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case pos.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
h4 : 4 ∈ Equiv.Perm.cycleType g
hg4 : ∀ x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4, x = 0
x : ℕ
hx : x ∈ Multiset.erase (Equiv.Perm.cycleType g) 4
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
this : Equiv.Perm.cycleType g = {4}
⊢ False
Tactic:
rw [this, ← Units.eq_iff] at hg0
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : ↑((-1) ^ (Multiset.sum {4} + Multiset.card {4})) = ↑1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
this : Equiv.Perm.cycleType g = {4}
⊢ False
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : ↑((-1) ^ (Multiset.sum {4} + Multiset.card {4})) = ↑1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∈ Equiv.Perm.cycleType g
this : Equiv.Perm.cycleType g = {4}
⊢ False
Tactic:
norm_num at hg0
Proof state after:
no goals
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
⊢ Equiv.Perm.cycleType g = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
Tactic:
rw [Multiset.eq_replicate_card]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
⊢ ∀ b ∈ Equiv.Perm.cycleType g, b = 2