internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 2 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk2 : Multiset.card (Equiv.Perm.cycleType g) = 2
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
simp only [this]
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 2 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk2 : Multiset.card (Equiv.Perm.cycleType g) = 2
⊢ Multiset.replicate 2 2 = ∅ ∨ Multiset.replicate 2 2 = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 2 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk2 : Multiset.card (Equiv.Perm.cycleType g) = 2
⊢ Multiset.replicate 2 2 = ∅ ∨ Multiset.replicate 2 2 = {2, 2}
Tactic:
simp only [Finset.mem_univ, Multiset.replicate_succ, Multiset.replicate_one,
  Multiset.empty_eq_zero, Multiset.cons_ne_zero, Multiset.insert_eq_cons, eq_self_iff_true,
  false_or_iff, and_self_iff]
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 2 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk2 : Multiset.card (Equiv.Perm.cycleType g) = 2
⊢ 2 ::ₘ 2 ::ₘ Multiset.replicate 0 2 = 2 ::ₘ {2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 2 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk2 : Multiset.card (Equiv.Perm.cycleType g) = 2
⊢ 2 ::ₘ 2 ::ₘ Multiset.replicate 0 2 = 2 ::ₘ {2}
Tactic:
simp only [Multiset.replicate_zero, Multiset.cons_zero]
Proof state after:
no goals
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) < 2
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
rw [Nat.lt_succ_iff] at hk1
Proof state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
cases' Nat.eq_or_lt_of_le hk1 with hk1 hk0
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk1 : Multiset.card (Equiv.Perm.cycleType g) = 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}

case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk1 : Multiset.card (Equiv.Perm.cycleType g) = 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}

case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
exfalso
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk1 : Multiset.card (Equiv.Perm.cycleType g) = 1
⊢ False

case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk1 : Multiset.card (Equiv.Perm.cycleType g) = 1
⊢ False

case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
rw [hk1, ← Units.eq_iff] at hg0
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : ↑((-1) ^ 1) = ↑1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk1 : Multiset.card (Equiv.Perm.cycleType g) = 1
⊢ False

case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : ↑((-1) ^ 1) = ↑1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1✝ : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk1 : Multiset.card (Equiv.Perm.cycleType g) = 1
⊢ False

case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
norm_num at hg0
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) < 1
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
simp only [Nat.lt_one_iff] at hk0
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
rw [hk0] at this
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 0 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 0 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
simp only [this]
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 0 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Multiset.replicate 0 2 = ∅ ∨ Multiset.replicate 0 2 = {2, 2}
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 0 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Multiset.replicate 0 2 = ∅ ∨ Multiset.replicate 0 2 = {2, 2}
Tactic:
left
Proof state after:
case inr.inr.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 0 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Multiset.replicate 0 2 = ∅
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case inr.inr.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
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 = Multiset.replicate 0 2
hg0 : (-1) ^ Multiset.card (Equiv.Perm.cycleType g) = 1
hk2 : Multiset.card (Equiv.Perm.cycleType g) ≤ 2
hk1 : Multiset.card (Equiv.Perm.cycleType g) ≤ 1
hk0 : Multiset.card (Equiv.Perm.cycleType g) = 0
⊢ Multiset.replicate 0 2 = ∅
Tactic:
simp only [Multiset.replicate_zero, Multiset.empty_eq_zero]
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ∣ 2 ^ n
Tactic:
apply Nat.dvd_trans _ hg
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
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ∣ Multiset.lcm (Equiv.Perm.cycleType g)
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ∣ Multiset.lcm (Equiv.Perm.cycleType g)
Tactic:
exact Multiset.dvd_lcm hi
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
this : k = 1
⊢ i = 2
Tactic:
rw [hlcm, this]
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
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
this : k = 1
⊢ 2 ^ 1 = 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
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
this : k = 1
⊢ 2 ^ 1 = 2
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
this : k = 2
⊢ False
Tactic:
apply h4
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
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
this : k = 2
⊢ 4 ∈ Equiv.Perm.cycleType g
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
this : k = 2
⊢ 4 ∈ Equiv.Perm.cycleType g
Tactic:
rw [this] at hlcm
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
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ 2
hk1 : 1 < k
this : k = 2
⊢ 4 ∈ Equiv.Perm.cycleType g