internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk0 : k = 0
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Tactic:
rw [hk0] at hlcm
Proof state after:
case neg.intro.intro.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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ 0
hk0 : k = 0
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ 0
hk0 : k = 0
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Tactic:
norm_num at hlcm
Proof state after:
case neg.intro.intro.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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk0 : k = 0
hlcm : i = 1
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk0 : k = 0
hlcm : i = 1
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Tactic:
rw [hlcm] at hi
Proof state after:
case neg.intro.intro.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
i : ℕ
hi : 1 ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk0 : k = 0
hlcm : i = 1
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.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
i : ℕ
hi : 1 ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk0 : k = 0
hlcm : i = 1
⊢ False

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Tactic:
apply Nat.lt_irrefl 1
Proof state after:
case neg.intro.intro.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
i : ℕ
hi : 1 ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk0 : k = 0
hlcm : i = 1
⊢ 1 < 1

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.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
i : ℕ
hi : 1 ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk0 : k = 0
hlcm : i = 1
⊢ 1 < 1

case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Tactic:
exact Equiv.Perm.one_lt_of_mem_cycleType hi
Proof state after:
case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.pp
α : 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
this : i ∣ 2 ^ n
⊢ Nat.Prime 2
Tactic:
exact Nat.prime_two
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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
rw [this] at hg0
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 :
  (-1) ^
      (Multiset.sum (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2) +
        Multiset.card (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2)) =
    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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
⊢ 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 (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2) +
        Multiset.card (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2)) =
    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 = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
simp only [pow_add, pow_mul, Multiset.sum_replicate, Algebra.id.smul_eq_mul,
  Multiset.card_replicate, Int.units_sq, one_mul] at hg0
Proof state after:
α : 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
⊢ 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 α
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
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
have hk2 : Multiset.card g.cycleType ≤ 2 := by
  rw [this] at hg4 ; rw [Multiset.sum_replicate] at hg4
  apply Nat.le_of_mul_le_mul_left; rw [Nat.mul_comm 2]
  exact hg4
  norm_num
Proof state after:
α : 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
⊢ 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 α
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
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}
Tactic:
cases' Nat.eq_or_lt_of_le hk2 with hk2 hk1
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 (Multiset.card (Equiv.Perm.cycleType g)) 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}

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}
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 α
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
⊢ Multiset.card (Equiv.Perm.cycleType g) ≤ 2
Tactic:
rw [this] at hg4
Proof state after:
α : 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 (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2) ≤ 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
⊢ Multiset.card (Equiv.Perm.cycleType g) ≤ 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 α
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType g)) 2) ≤ 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
⊢ Multiset.card (Equiv.Perm.cycleType g) ≤ 2
Tactic:
rw [Multiset.sum_replicate] at hg4
Proof state after:
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ Multiset.card (Equiv.Perm.cycleType g) ≤ 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 α
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ Multiset.card (Equiv.Perm.cycleType g) ≤ 2
Tactic:
apply Nat.le_of_mul_le_mul_left
Proof state after:
case 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ ?c * Multiset.card (Equiv.Perm.cycleType g) ≤ ?c * 2

case hc
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ 0 < ?c

case c
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ ℕ
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ ?c * Multiset.card (Equiv.Perm.cycleType g) ≤ ?c * 2

case hc
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ 0 < ?c

case c
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ ℕ
Tactic:
rw [Nat.mul_comm 2]
Proof state after:
case 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ Multiset.card (Equiv.Perm.cycleType g) * 2 ≤ 2 * 2

case hc
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ 0 < 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ Multiset.card (Equiv.Perm.cycleType g) * 2 ≤ 2 * 2

case hc
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ 0 < 2
Tactic:
exact hg4
Proof state after:
case hc
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ 0 < 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case hc
α : 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.card (Equiv.Perm.cycleType g) • 2 ≤ 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
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
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 (Multiset.card (Equiv.Perm.cycleType g)) 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:
rw [hk2] at 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
⊢ Equiv.Perm.cycleType g = ∅ ∨ Equiv.Perm.cycleType g = {2, 2}