Theorem: alternatingGroup.mem_V4_of_order_two_pow (Jordan/V4.lean)

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
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}

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
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}

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
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}

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
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}

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]
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 α

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
State after:
no goals

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
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

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
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}

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]
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}

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
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

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]
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

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
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

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
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

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
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

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
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

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]
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

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
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

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))
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

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]
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

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
State after:
no goals

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
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

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
State after:
no goals

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]
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

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
⊢ ∀ b ∈ Equiv.Perm.cycleType g, b = 2
Tactic:
intro i hi
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i = 2

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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i = 2
Tactic:
have : i ∣ 2 ^ n := by
  apply Nat.dvd_trans _ hg
  exact Multiset.dvd_lcm hi
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
this : i ∣ 2 ^ n
⊢ i = 2

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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
this : i ∣ 2 ^ n
⊢ i = 2
Tactic:
rw [Nat.dvd_prime_pow] at this
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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
this : ∃ k ≤ n, i = 2 ^ k
⊢ i = 2

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

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
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
this : ∃ k ≤ n, i = 2 ^ k
⊢ i = 2

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:
obtain ⟨k, hk, hlcm⟩ := this
State after:
case neg.intro.intro
α : 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
⊢ i = 2

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

State before:
case neg.intro.intro
α : 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
⊢ i = 2

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:
suffices k = 1 by
  rw [hlcm, this]; norm_num
State after:
case neg.intro.intro
α : 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
⊢ k = 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

State before:
case neg.intro.intro
α : 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
⊢ k = 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:
apply le_antisymm
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 ^ k
⊢ k ≤ 1

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
⊢ 1 ≤ k

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

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
⊢ k ≤ 1

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
⊢ 1 ≤ k

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 [← not_lt]
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 ^ k
⊢ ¬1 < k

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
⊢ 1 ≤ k

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

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
⊢ ¬1 < k

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
⊢ 1 ≤ k

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:
intro hk1
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 ^ k
hk1 : 1 < k
⊢ False

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
⊢ 1 ≤ k

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

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
hk1 : 1 < k
⊢ False

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
⊢ 1 ≤ k

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:
suffices k = 2 by
  apply h4
  rw [this] at hlcm ; norm_num at hlcm
  rw [← hlcm]
  exact hi
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 ^ k
hk1 : 1 < k
⊢ k = 2

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
⊢ 1 ≤ k

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

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
hk1 : 1 < k
⊢ k = 2

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
⊢ 1 ≤ k

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:
refine' le_antisymm _ hk1
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 ^ k
hk1 : 1 < k
⊢ k ≤ 2

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
⊢ 1 ≤ k

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

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
⊢ 1 ≤ k

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 [Nat.one_le_iff_ne_zero]
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 ^ k
⊢ k ≠ 0

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

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
⊢ k ≠ 0

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:
intro hk0
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 ^ 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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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}

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
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}

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
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}

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
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}

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
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

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
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

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
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
⊢ ℕ

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]
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

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
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

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
State after:
no goals

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
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}

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]
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}

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]
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}

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]
State after:
no goals

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
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}

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
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}

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
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}

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
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}

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
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}

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
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}

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
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}

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]
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}

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
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 = ∅

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]
State after:
no goals

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
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)

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
State after:
no goals

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]
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

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
State after:
no goals

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
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

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
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

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 ^ 2
hk1 : 1 < k
this : k = 2
⊢ 4 ∈ Equiv.Perm.cycleType g
Tactic:
norm_num at hlcm
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
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ 4 ∈ Equiv.Perm.cycleType g

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
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ 4 ∈ Equiv.Perm.cycleType g
Tactic:
rw [← hlcm]
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
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ i ∈ Equiv.Perm.cycleType g

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
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ i ∈ Equiv.Perm.cycleType g
Tactic:
exact hi
State after:
no goals

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
hk1 : 1 < k
⊢ k ≤ 2
Tactic:
rw [← Nat.pow_le_pow_iff_right (Nat.le_refl 2)]
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 ^ k
hk1 : 1 < k
⊢ 2 ^ k ≤ 2 ^ 2

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
hk1 : 1 < k
⊢ 2 ^ k ≤ 2 ^ 2
Tactic:
norm_num
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 ^ k
hk1 : 1 < k
⊢ 2 ^ k ≤ 4

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
hk1 : 1 < k
⊢ 2 ^ k ≤ 4
Tactic:
rw [← hα4, ← hlcm]
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 ^ k
hk1 : 1 < k
⊢ i ≤ Fintype.card α

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
hk1 : 1 < k
⊢ i ≤ Fintype.card α
Tactic:
apply le_trans (Equiv.Perm.le_card_support_of_mem_cycleType hi)
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 ^ k
hk1 : 1 < k
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α

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
hk1 : 1 < k
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Tactic:
apply Finset.card_le_univ
State after:
no goals