[GOAL]
p q r : ℕ+
⊢ sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹
[PROOFSTEP]
simp only [sumInv, add_zero, insert_eq_cons, add_assoc, map_cons, sum_cons, map_singleton, sum_singleton]
[GOAL]
pqr : Multiset ℕ+
⊢ Admissible pqr → 1 < sumInv pqr
[PROOFSTEP]
rw [Admissible]
[GOAL]
pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr
[PROOFSTEP]
rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)
[GOAL]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, A', sumInv_pqr, add_assoc]
[GOAL]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)
[PROOFSTEP]
simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
[GOAL]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹
[PROOFSTEP]
apply add_pos
[GOAL]
case inl.intro.intro.ha
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹
[PROOFSTEP]
simp only [PNat.pos, Nat.cast_pos, inv_pos]
[GOAL]
case inl.intro.intro.hb
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑q')⁻¹
[PROOFSTEP]
simp only [PNat.pos, Nat.cast_pos, inv_pos]
[GOAL]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, D', sumInv_pqr]
[GOAL]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
| (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
| (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
| (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑(1 + 1))⁻¹ + (↑(1 + 1))⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr
case inr.inr.inr.inr pqr : Multiset ℕ+ H : E' 5 = pqr ⊢ 1 < sumInv pqr
[PROOFSTEP]
all_goals
  rw [← H, E', sumInv_pqr]
  conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, E', sumInv_pqr]
[GOAL]
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 3 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 3 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 3 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, E', sumInv_pqr]
[GOAL]
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 4 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 4 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 4 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, E', sumInv_pqr]
[GOAL]
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 5 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 5 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 5 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ p < 3
[PROOFSTEP]
have h3 : (0 : ℚ) < 3 := by norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ 0 < 3
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
h3 : 0 < 3
⊢ p < 3
[PROOFSTEP]
contrapose! H
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
⊢ sumInv {p, q, r} ≤ 1
[PROOFSTEP]
rw [sumInv_pqr]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have h3q := H.trans hpq
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have h3r := h3q.trans hqr
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := by
  rw [inv_le_inv _ h3]
  assumption_mod_cast
  norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ (↑↑p)⁻¹ ≤ 3⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h3]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ 3 ≤ ↑↑p
p q r : ℕ+ hpq : p ≤ q hqr : q ≤ r h3 : 0 < 3 H : 3 ≤ p h3q : 3 ≤ q h3r : 3 ≤ r ⊢ 0 < ↑↑p
[PROOFSTEP]
assumption_mod_cast
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ 0 < ↑↑p
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := by
  rw [inv_le_inv _ h3]
  assumption_mod_cast
  norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ (↑↑q)⁻¹ ≤ 3⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h3]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑q
p q r : ℕ+ hpq : p ≤ q hqr : q ≤ r h3 : 0 < 3 H : 3 ≤ p h3q : 3 ≤ q h3r : 3 ≤ r hp : (↑↑p)⁻¹ ≤ 3⁻¹ ⊢ 0 < ↑↑q
[PROOFSTEP]
assumption_mod_cast
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑q
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := by
  rw [inv_le_inv _ h3]
  assumption_mod_cast
  norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ (↑↑r)⁻¹ ≤ 3⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h3]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑r
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
[PROOFSTEP]
assumption_mod_cast
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
hr : (↑↑r)⁻¹ ≤ 3⁻¹
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
calc
  (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
  _ = 1 := by norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
hr : (↑↑r)⁻¹ ≤ 3⁻¹
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ q < 4
[PROOFSTEP]
have h4 : (0 : ℚ) < 4 := by norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
h4 : 0 < 4
⊢ q < 4
[PROOFSTEP]
contrapose! H
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1
[PROOFSTEP]
rw [sumInv_pqr]
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have h4r := H.trans hqr
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := by
  rw [inv_le_inv _ h4]
  assumption_mod_cast
  norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ (↑↑q)⁻¹ ≤ 4⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h4]
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 4 ≤ ↑↑q
q r : ℕ+ hqr : q ≤ r h4 : 0 < 4 H : 4 ≤ q h4r : 4 ≤ r ⊢ 0 < ↑↑q
[PROOFSTEP]
assumption_mod_cast
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 0 < ↑↑q
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := by
  rw [inv_le_inv _ h4]
  assumption_mod_cast
  norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑r)⁻¹ ≤ 4⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h4]
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 4 ≤ ↑↑r
q r : ℕ+ hqr : q ≤ r h4 : 0 < 4 H : 4 ≤ q h4r : 4 ≤ r hq : (↑↑q)⁻¹ ≤ 4⁻¹ ⊢ 0 < ↑↑r
[PROOFSTEP]
assumption_mod_cast
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
calc
  (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
  _ = 1 := by norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ 2⁻¹ + 4⁻¹ + 4⁻¹ = 1
[PROOFSTEP]
norm_num
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ r < 6
[PROOFSTEP]
have h6 : (0 : ℚ) < 6 := by norm_num
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ 0 < 6
[PROOFSTEP]
norm_num
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
h6 : 0 < 6
⊢ r < 6
[PROOFSTEP]
contrapose! H
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1
[PROOFSTEP]
rw [sumInv_pqr]
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := by
  rw [inv_le_inv _ h6]
  assumption_mod_cast
  norm_num
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑r)⁻¹ ≤ 6⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h6]
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 6 ≤ ↑↑r
r : ℕ+ h6 : 0 < 6 H : 6 ≤ r ⊢ 0 < ↑↑r
[PROOFSTEP]
assumption_mod_cast
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r
[PROOFSTEP]
norm_num
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
calc
  (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
  _ = 1 := by norm_num
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ 2⁻¹ + 3⁻¹ + 6⁻¹ = 1
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}
[PROOFSTEP]
have hp3 : p < 3 := lt_three hpq hqr H
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p < 3
⊢ Admissible {p, q, r}
[PROOFSTEP]
replace hp3 := Finset.mem_Iio.mpr hp3
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
⊢ Admissible {p, q, r}
[PROOFSTEP]
conv at hp3 => change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3
[PROOFSTEP]
change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3
[PROOFSTEP]
change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3
[PROOFSTEP]
change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ {1, 2}
⊢ Admissible {p, q, r}
[PROOFSTEP]
fin_cases hp3
[GOAL]
case head
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}
[PROOFSTEP]
exact admissible_A' q r
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}
[PROOFSTEP]
have hq4 : q < 4 := lt_four hqr H
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Admissible {2, q, r}
[PROOFSTEP]
replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}
[PROOFSTEP]
clear hpq
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}
[PROOFSTEP]
conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4
[PROOFSTEP]
change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4
[PROOFSTEP]
change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4
[PROOFSTEP]
change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ {2, 3}
⊢ Admissible {2, q, r}
[PROOFSTEP]
fin_cases hq4
[GOAL]
case tail.head.head
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}
[PROOFSTEP]
exact admissible_D' r
[GOAL]
case tail.head.tail.head
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}
[PROOFSTEP]
have hr6 : r < 6 := lt_six H
[GOAL]
case tail.head.tail.head
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Admissible {2, 3, r}
[PROOFSTEP]
replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩
[GOAL]
case tail.head.tail.head
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}
[PROOFSTEP]
clear hqr
[GOAL]
case tail.head.tail.head
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}
[PROOFSTEP]
conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6
[PROOFSTEP]
change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6
[PROOFSTEP]
change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6
[PROOFSTEP]
change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
case tail.head.tail.head
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ {3, 4, 5}
⊢ Admissible {2, 3, r}
[PROOFSTEP]
fin_cases hr6
[GOAL]
case tail.head.tail.head.head
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}
[PROOFSTEP]
exact admissible_E6
[GOAL]
case tail.head.tail.head.tail.head
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}
[PROOFSTEP]
exact admissible_E7
[GOAL]
case tail.head.tail.head.tail.tail.head
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}
[PROOFSTEP]
exact admissible_E8
[GOAL]
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
⊢ Admissible ↑[p, q, r]
[PROOFSTEP]
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r
[GOAL]
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
⊢ (p ≤ q ∧ p ≤ r) ∧ q ≤ r
case intro.intro
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]
[PROOFSTEP]
simpa using hs
[GOAL]
case intro.intro
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]
[PROOFSTEP]
exact admissible_of_one_lt_sumInv_aux' hpq hqr H
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}
[PROOFSTEP]
simp only [Admissible]
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
let S := sort ((· ≤ ·) : ℕ+ → ℕ+ → Prop) { p, q, r }
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
have hS : S.Sorted (· ≤ ·) := sort_sorted _ _
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
have hpqr : ({ p, q, r } : Multiset ℕ+) = S := (sort_eq LE.le { p, q, r }).symm
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
rw [hpqr]
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
[PROOFSTEP]
rw [hpqr] at H
[GOAL]
p q r : ℕ+
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
[PROOFSTEP]
apply admissible_of_one_lt_sumInv_aux hS _ H
[GOAL]
p q r : ℕ+
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ List.length S = 3
[PROOFSTEP]
simp only [ge_iff_le, insert_eq_cons, length_sort, card_cons, card_singleton]


[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ List.prod l ∈ alternatingGroup α ↔ Even (List.length l)
[PROOFSTEP]
rw [mem_alternatingGroup, sign_prod_list_swap hl, ← Units.val_eq_one, Units.val_pow_eq_pow_val, Units.coe_neg_one,
  neg_one_pow_eq_one_iff_even]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ finRotate (bit1 n) ∈ alternatingGroup (Fin (bit1 n))
[PROOFSTEP]
rw [mem_alternatingGroup, bit1, sign_finRotate, pow_bit0', Int.units_mul_self, one_pow]
[GOAL]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
[PROOFSTEP]
let this := (QuotientGroup.quotientKerEquivOfSurjective _ (sign_surjective α)).toEquiv
[GOAL]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
[PROOFSTEP]
rw [← Fintype.card_units_int, ← Fintype.card_congr this]
[GOAL]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ card (Perm α ⧸ MonoidHom.ker sign) * card { x // x ∈ alternatingGroup α } = card (Perm α)
[PROOFSTEP]
apply (Subgroup.card_eq_card_quotient_mul_card_subgroup _).symm
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : { x // x ∈ alternatingGroup α }
hc : IsConj ↑σ ↑τ
hσ : Finset.card (support ↑σ) + 2 ≤ card α
⊢ IsConj σ τ
[PROOFSTEP]
obtain ⟨σ, hσ⟩ := σ
[GOAL]
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : { x // x ∈ alternatingGroup α }
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑τ
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
⊢ IsConj { val := σ, property := hσ✝ } τ
[PROOFSTEP]
obtain ⟨τ, hτ⟩ := τ
[GOAL]
case mk.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
obtain ⟨π, hπ⟩ := isConj_iff.1 hc
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * ↑{ val := σ, property := hσ✝ } * π⁻¹ = ↑{ val := τ, property := hτ }
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
rw [Subtype.coe_mk, Subtype.coe_mk] at hπ
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
cases' Int.units_eq_one_or (Perm.sign π) with h h
[GOAL]
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = 1
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
rw [isConj_iff]
[GOAL]
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = 1
⊢ ∃ c, c * { val := σ, property := hσ✝ } * c⁻¹ = { val := τ, property := hτ }
[PROOFSTEP]
refine' ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective _⟩
[GOAL]
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = 1
⊢ ↑({ val := π, property := (_ : ↑sign π = 1) } * { val := σ, property := hσ✝ } *
        { val := π, property := (_ : ↑sign π = 1) }⁻¹) =
    ↑{ val := τ, property := hτ }
[PROOFSTEP]
simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using hπ
[GOAL]
case mk.mk.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
have h2 : 2 ≤ σ.supportᶜ.card :=
  by
  rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
  exact hσ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
⊢ 2 ≤ Finset.card (support σ)ᶜ
[PROOFSTEP]
rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
⊢ Finset.card (support σ) + 2 ≤ card α
[PROOFSTEP]
exact hσ
[GOAL]
case mk.mk.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
obtain ⟨a, ha, b, hb, ab⟩ := Finset.one_lt_card.1 h2
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
refine' isConj_iff.2 ⟨⟨π * swap a b, _⟩, Subtype.val_injective _⟩
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ π * swap a b ∈ alternatingGroup α
[PROOFSTEP]
rw [mem_alternatingGroup, MonoidHom.map_mul, h, sign_swap ab, Int.units_mul_self]
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ ↑({ val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) } * { val := σ, property := hσ✝ } *
        { val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) }⁻¹) =
    ↑{ val := τ, property := hτ }
[PROOFSTEP]
simp only [← hπ, coe_mk, Subgroup.coe_mul, Subtype.val]
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ π * swap a b * σ * ↑{ val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) }⁻¹ = π * σ * π⁻¹
[PROOFSTEP]
have hd : Disjoint (swap a b) σ :=
  by
  rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left, Finset.disjoint_singleton_left]
  exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ Perm.Disjoint (swap a b) σ
[PROOFSTEP]
rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left, Finset.disjoint_singleton_left]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ ¬a ∈ support σ ∧ ¬b ∈ support σ
[PROOFSTEP]
exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
hd : Perm.Disjoint (swap a b) σ
⊢ π * swap a b * σ * ↑{ val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) }⁻¹ = π * σ * π⁻¹
[PROOFSTEP]
rw [mul_assoc π _ σ, hd.commute.eq, coe_inv, coe_mk]
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
hd : Perm.Disjoint (swap a b) σ
⊢ π * (σ * swap a b) * (π * swap a b)⁻¹ = π * σ * π⁻¹
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
σ τ : { x // x ∈ alternatingGroup α }
hσ : IsThreeCycle ↑σ
hτ : IsThreeCycle ↑τ
⊢ Finset.card (support ↑σ) + 2 ≤ card α
[PROOFSTEP]
rwa [hσ.card_support]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ σ ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
suffices hind :
  ∀ (n : ℕ) (l : List (Perm α)) (_ : ∀ g, g ∈ l → IsSwap g) (_ : l.length = 2 * n),
    l.prod ∈ closure {σ : Perm α | IsThreeCycle σ}
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
⊢ σ ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ
[GOAL]
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = n + n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [← two_mul] at hn
[GOAL]
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = 2 * n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact hind n l hl hn
[GOAL]
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
intro n
[GOAL]
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
induction' n with n ih
[GOAL]
case hind.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * Nat.zero → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
intro l hl hn
[GOAL]
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * Nat.succ n → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
intro l hl hn
[GOAL]
case hind.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.zero
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
simp [List.length_eq_zero.1 hn, one_mem]
[GOAL]
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.succ n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [Nat.mul_succ] at hn
[GOAL]
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * n + 2
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
[GOAL]
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length (a :: l) = 2 * n + 2
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [List.length_cons, Nat.succ_inj'] at hn
[GOAL]
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length l = 2 * n + 1
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
[GOAL]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ List.prod (a :: b :: l) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, ← mul_assoc]
[GOAL]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [List.length_cons, Nat.succ_inj'] at hn
[GOAL]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length l = 2 * n
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact
  mul_mem
    (IsSwap.mul_mem_closure_three_cycles (hl a (List.mem_cons_self a _))
      (hl b (List.mem_cons_of_mem a (l.mem_cons_self b))))
    (ih _ (fun g hg => hl g (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hg))) hn)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
⊢ ⊤ ≤ normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ ⊤ ≤ normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
refine' eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) _))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ map (Subgroup.subtype (alternatingGroup α)) ⊤ ≤
    map (Subgroup.subtype (alternatingGroup α)) (normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }})
[PROOFSTEP]
rw [← MonoidHom.range_eq_map, subtype_range, normalClosure, MonoidHom.map_closure]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ alternatingGroup α ≤
    closure
      (↑(Subgroup.subtype (alternatingGroup α)) ''
        Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }})
[PROOFSTEP]
refine' (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono _)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ {σ | IsThreeCycle σ} ⊆
    ↑(Subgroup.subtype (alternatingGroup α)) ''
      Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
intro g h
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
g : Perm α
h : g ∈ {σ | IsThreeCycle σ}
⊢ g ∈
    ↑(Subgroup.subtype (alternatingGroup α)) ''
      Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
c : Perm α
h : c * f * c⁻¹ ∈ {σ | IsThreeCycle σ}
⊢ c * f * c⁻¹ ∈
    ↑(Subgroup.subtype (alternatingGroup α)) ''
      Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
refine' ⟨⟨c * f * c⁻¹, h.mem_alternatingGroup⟩, _, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
c : Perm α
h : c * f * c⁻¹ ∈ {σ | IsThreeCycle σ}
⊢ { val := c * f * c⁻¹, property := (_ : c * f * c⁻¹ ∈ alternatingGroup α) } ∈
    Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
rw [Group.mem_conjugatesOfSet_iff]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
c : Perm α
h : c * f * c⁻¹ ∈ {σ | IsThreeCycle σ}
⊢ ∃ a,
    a ∈ {{ val := f, property := (_ : f ∈ alternatingGroup α) }} ∧
      IsConj a { val := c * f * c⁻¹, property := (_ : c * f * c⁻¹ ∈ alternatingGroup α) }
[PROOFSTEP]
exact ⟨⟨f, hf.mem_alternatingGroup⟩, Set.mem_singleton _, isThreeCycle_isConj h5 hf h⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h : 3 ∈ cycleType g
⊢ IsThreeCycle (g * g)
[PROOFSTEP]
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ IsThreeCycle (c * g' * (c * g'))
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ IsThreeCycle (c * (g' * (c * g')))
[PROOFSTEP]
rw [hd.commute.eq, ← mul_assoc g']
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ IsThreeCycle (c * (g' * g' * c))
[PROOFSTEP]
suffices hg' : orderOf g' ∣ 2
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
hg' : orderOf g' ∣ 2
⊢ IsThreeCycle (c * (g' * g' * c))
[PROOFSTEP]
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
hg' : orderOf g' ∣ 2
⊢ IsThreeCycle (c * c)
[PROOFSTEP]
exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
[GOAL]
case hg'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ orderOf g' ∣ 2
[PROOFSTEP]
rw [← lcm_cycleType, Multiset.lcm_dvd]
[GOAL]
case hg'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ ∀ (b : ℕ), b ∈ cycleType g' → b ∣ 2
[PROOFSTEP]
intro n hn
[GOAL]
case hg'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ n ∣ 2
[PROOFSTEP]
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ Finset.card (support g') ≤ 2
[PROOFSTEP]
apply le_of_add_le_add_left
[GOAL]
case bc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ ?a + Finset.card (support g') ≤ ?a + 2
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ ℕ
[PROOFSTEP]
rw [← hd.card_support_mul, h3]
[GOAL]
case bc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ Finset.card (support (c * g')) ≤ 3 + 2
[PROOFSTEP]
exact (c * g').support.card_le_univ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
[PROOFSTEP]
haveI := Fintype.one_lt_card_iff_nontrivial.1 (lt_trans (by decide) h3)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
[PROOFSTEP]
rw [← Fintype.one_lt_card_iff_nontrivial]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 1 < card { x // x ∈ alternatingGroup α }
[PROOFSTEP]
refine' lt_of_mul_lt_mul_left _ (le_of_lt Nat.prime_two.pos)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 2 * 1 < 2 * card { x // x ∈ alternatingGroup α }
[PROOFSTEP]
rw [two_mul_card_alternatingGroup, card_perm, ← Nat.succ_le_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nat.succ (2 * 1) ≤ Nat.factorial (card α)
[PROOFSTEP]
exact le_trans h3 (card α).self_le_factorial
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ 3 ≤ card (Fin (n + 3))
[PROOFSTEP]
rw [card_fin]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ 3 ≤ n + 3
[PROOFSTEP]
exact le_add_left (le_refl 3)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ⊤ ≤ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
have h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹) :=
  card_support_eq_three_iff.1 (by decide)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Finset.card (support (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)) = 3
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ ⊤ ≤ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
rw [← h3.alternating_normalClosure (by rw [card_fin])]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ 5 ≤ card (Fin 5)
[PROOFSTEP]
rw [card_fin]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ normalClosure
      {{ val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
          property :=
            (_ :
              Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) }} ≤
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
refine' normalClosure_le_normal _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ {{ val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
        property :=
          (_ : Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) }} ⊆
    ↑(normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }})
[PROOFSTEP]
rw [Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ { val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
      property :=
        (_ : Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) } ∈
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
have h : (⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ : alternatingGroup (Fin 5)) ∈ normalClosure _ :=
  SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
h :
  { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) } ∈
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
⊢ { val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
      property :=
        (_ : Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) } ∈
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
exact
  (mul_mem
      (Subgroup.normalClosure_normal.conj_mem _ h
        ⟨Fin.cycleRange 2, Fin.isThreeCycle_cycleRange_two.mem_alternatingGroup⟩)
      (inv_mem h)
        --Porting note : added `: _` :
    _)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign (swap 0 4 * swap 1 3) = 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
[PROOFSTEP]
let g1 := (⟨swap 0 2 * swap 0 1, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign (swap 0 2 * swap 0 1) = 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
[PROOFSTEP]
let g2 := (⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
⊢ ↑sign (swap 0 4 * swap 1 3) = 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
[PROOFSTEP]
have h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ :=
  by
  rw [Subtype.ext_iff]
  simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
[PROOFSTEP]
rw [Subtype.ext_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ ↑(g1 * g2 * g1⁻¹ * g2⁻¹) =
    ↑{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
[PROOFSTEP]
simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← normalClosure_finRotate_five]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} ≤
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
[PROOFSTEP]
refine' normalClosure_le_normal _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} ⊆
    ↑(normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }})
[PROOFSTEP]
rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
[PROOFSTEP]
have h : g2 ∈ normalClosure { g2 } := SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
h : g2 ∈ normalClosure {g2}
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
[PROOFSTEP]
exact mul_mem (Subgroup.normalClosure_normal.conj_mem _ h g1) (inv_mem h)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
have h := g.support.card_le_univ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
h : Finset.card (support g) ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [← Multiset.eq_replicate_card] at h2
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : Finset.card (support g) ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
have h : Multiset.card g.cycleType ≤ 3 :=
  le_of_mul_le_mul_right (le_trans h (by simp only [card_fin]; ring_nf)) (by simp)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ card (Fin 5) ≤ 3 * 2
[PROOFSTEP]
simp only [card_fin]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ 5 ≤ 3 * 2
[PROOFSTEP]
ring_nf
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ 0 < 2
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha :
  (-1) ^
      (Multiset.sum (Multiset.replicate (↑Multiset.card (cycleType g)) 2) +
        ↑Multiset.card (Multiset.replicate (↑Multiset.card (cycleType g)) 2)) =
    1
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
norm_num at ha
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : (-1) ^ (↑Multiset.card (cycleType g) * 2 + ↑Multiset.card (cycleType g)) = 1
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [pow_add, pow_mul, Int.units_pow_two, one_mul, Units.ext_iff, Units.val_one, Units.val_pow_eq_pow_val,
  Units.coe_neg_one, neg_one_pow_eq_one_iff_even _] at ha
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : Even (↑Multiset.card (cycleType g))
⊢ IsConj (swap 0 4 * swap 1 3) g
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : (-1) ^ ↑Multiset.card (cycleType g) = 1
⊢ -1 ≠ 1
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : (-1) ^ ↑Multiset.card (cycleType g) = 1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : Even (↑Multiset.card (cycleType g))
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [isConj_iff_cycleType_eq, h2]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : Even (↑Multiset.card (cycleType g))
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate (↑Multiset.card (cycleType g)) 2
[PROOFSTEP]
interval_cases h_1 : Multiset.card g.cycleType
[GOAL]
case «0»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 0
h2 : cycleType g = Multiset.replicate 0 2
h✝ : 0 * 2 ≤ card (Fin 5)
h : 0 ≤ 3
ha : Even 0
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 0 2
[PROOFSTEP]
exact (h1 (card_cycleType_eq_zero.1 h_1)).elim
[GOAL]
case «1»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 1
h2 : cycleType g = Multiset.replicate 1 2
h✝ : 1 * 2 ≤ card (Fin 5)
h : 1 ≤ 3
ha : Even 1
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 1 2
[PROOFSTEP]
contrapose! ha
[GOAL]
case «1»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 1
h2 : cycleType g = Multiset.replicate 1 2
h✝ : 1 * 2 ≤ card (Fin 5)
h : 1 ≤ 3
ha : cycleType (swap 0 4 * swap 1 3) ≠ Multiset.replicate 1 2
⊢ ¬Even 1
[PROOFSTEP]
simp [h_1]
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 2 2
[PROOFSTEP]
have h04 : (0 : Fin 5) ≠ 4 := by decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
⊢ 0 ≠ 4
[PROOFSTEP]
decide
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 2 2
[PROOFSTEP]
have h13 : (1 : Fin 5) ≠ 3 := by decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
⊢ 1 ≠ 3
[PROOFSTEP]
decide
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 2 2
[PROOFSTEP]
rw [Disjoint.cycleType, (isCycle_swap h04).cycleType, (isCycle_swap h13).cycleType, card_support_swap h04,
  card_support_swap h13]
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ ↑[2] + ↑[2] = Multiset.replicate 2 2
[PROOFSTEP]
rfl
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ Perm.Disjoint (swap 0 4) (swap 1 3)
[PROOFSTEP]
rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13]
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ _root_.Disjoint {0, 4} {1, 3}
[PROOFSTEP]
decide
[GOAL]
case «3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 3
h2 : cycleType g = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
ha : Even 3
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 3 2
[PROOFSTEP]
contrapose! ha
[GOAL]
case «3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 3
h2 : cycleType g = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
ha : cycleType (swap 0 4 * swap 1 3) ≠ Multiset.replicate 3 2
⊢ ¬Even 3
[PROOFSTEP]
simp [h_1]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
⊢ Normal H → H = ⊥ ∨ H = ⊤
[PROOFSTEP]
intro Hn
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
refine' or_not.imp id fun Hb => _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
Hb : ¬H = ⊥
⊢ H = ⊤
[PROOFSTEP]
rw [eq_bot_iff_forall] at Hb
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
Hb : ¬∀ (x : { x // x ∈ alternatingGroup (Fin 5) }), x ∈ H → x = 1
⊢ H = ⊤
[PROOFSTEP]
push_neg at Hb
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
Hb : ∃ x, x ∈ H ∧ x ≠ 1
⊢ H = ⊤
[PROOFSTEP]
obtain ⟨⟨g, gA⟩, gH, g1⟩ : ∃ x : ↥(alternatingGroup (Fin 5)), x ∈ H ∧ x ≠ 1 := Hb
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : { val := g, property := gA } ∈ H
g1 : { val := g, property := gA } ≠ 1
⊢ H = ⊤
[PROOFSTEP]
rw [← SetLike.mem_coe, ← Set.singleton_subset_iff] at gH
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
⊢ H = ⊤
[PROOFSTEP]
refine'
  eq_top_iff.2
    (le_trans (ge_of_eq _) (normalClosure_le_normal gH))
      -- It suffices to show that the normal closure of `g` in $A_5$ is $A_5$.
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
by_cases h2 :
  ∀ n ∈ g.cycleType,
    n =
      2
        -- If the cycle decomposition of `g` consists entirely of swaps, then the cycle type is $(2,2)$.
            -- This means that it is conjugate to $(04)(13)$, whose normal closure is $A_5$.
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
rw [Ne.def, Subtype.ext_iff] at g1
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : ¬↑{ val := g, property := gA } = ↑1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
exact (isConj_swap_mul_swap_of_cycleType_two gA g1 h2).normalClosure_eq_top_of normalClosure_swap_mul_swap_five
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
h2 : ¬∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
push_neg at h2
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
h2 : ∃ n, n ∈ cycleType g ∧ n ≠ 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
obtain ⟨n, ng, n2⟩ : ∃ n : ℕ, n ∈ g.cycleType ∧ n ≠ 2 := h2
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
have n2' : 2 < n := lt_of_le_of_ne (two_le_of_mem_cycleType ng) n2.symm
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
have n5 : n ≤ 5 := le_trans ?_ g.support.card_le_univ
[GOAL]
case neg.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
n5 : n ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
case neg.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
⊢ n ≤ Finset.card (support g)
[PROOFSTEP]
swap
[GOAL]
case neg.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
⊢ n ≤ Finset.card (support g)
[PROOFSTEP]
obtain ⟨m, hm⟩ := Multiset.exists_cons_of_mem ng
[GOAL]
case neg.intro.intro.refine_1.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
m : Multiset ℕ
hm : cycleType g = n ::ₘ m
⊢ n ≤ Finset.card (support g)
[PROOFSTEP]
rw [← sum_cycleType, hm, Multiset.sum_cons]
[GOAL]
case neg.intro.intro.refine_1.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
m : Multiset ℕ
hm : cycleType g = n ::ₘ m
⊢ n ≤ n + Multiset.sum m
[PROOFSTEP]
exact le_add_right le_rfl
[GOAL]
case neg.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
n5 : n ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
interval_cases n
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← (isThreeCycle_sq_of_three_mem_cycleType_five ng).alternating_normalClosure (by rw [card_fin])]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ 5 ≤ card (Fin 5)
[PROOFSTEP]
rw [card_fin]
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ normalClosure {{ val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) }} ≤
    normalClosure {{ val := g, property := gA }}
[PROOFSTEP]
refine' normalClosure_le_normal _
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ {{ val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) }} ⊆
    ↑(normalClosure {{ val := g, property := gA }})
[PROOFSTEP]
rw [Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ { val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) } ∈ normalClosure {{ val := g, property := gA }}
[PROOFSTEP]
have h := SetLike.mem_coe.1 (subset_normalClosure (G := alternatingGroup (Fin 5)) (Set.mem_singleton ⟨g, gA⟩))
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
h : { val := g, property := gA } ∈ normalClosure {{ val := g, property := gA }}
⊢ { val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) } ∈ normalClosure {{ val := g, property := gA }}
[PROOFSTEP]
exact mul_mem h h
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
have con := mem_alternatingGroup.1 gA
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : ↑sign g = 1
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
contrapose! con
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ ↑sign g ≠ 1
[PROOFSTEP]
rw [sign_of_cycleType, cycleType_of_card_le_mem_cycleType_add_two (by decide) ng]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ card (Fin 5) < 4 + 2
[PROOFSTEP]
decide
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ (-1) ^ (Multiset.sum {4} + ↑Multiset.card {4}) ≠ 1
[PROOFSTEP]
dsimp only
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ (-1) ^ (Multiset.sum {4} + ↑Multiset.card {4}) ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg.intro.intro.refine_2.«5»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 5 ∈ cycleType g
n2 : 5 ≠ 2
n2' : 2 < 5
n5 : 5 ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
refine' (isConj_iff_cycleType_eq.2 _).normalClosure_eq_top_of normalClosure_finRotate_five
[GOAL]
case neg.intro.intro.refine_2.«5»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 5 ∈ cycleType g
n2 : 5 ≠ 2
n2' : 2 < 5
n5 : 5 ≤ 5
⊢ cycleType (finRotate 5) = cycleType g
[PROOFSTEP]
rw [cycleType_of_card_le_mem_cycleType_add_two (by decide) ng, cycleType_finRotate]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 5 ∈ cycleType g
n2 : 5 ≠ 2
n2' : 2 < 5
n5 : 5 ≤ 5
⊢ card (Fin 5) < 5 + 2
[PROOFSTEP]
decide


[GOAL]
k n : ℕ
hk0 : k ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
rcases(one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)
[GOAL]
case inl
n : ℕ
hk0 : 1 ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
[PROOFSTEP]
rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩
[GOAL]
case inl.intro.intro
n : ℕ
hk0 : 1 ≠ 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
[PROOFSTEP]
exact ⟨p, hp, hnp, modEq_one⟩
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
let b := k * (n !)
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
have hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs :=
  by
  rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
  have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
  calc
    1 ≤ b - 1 := le_tsub_of_add_le_left hb
    _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs := sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
[PROOFSTEP]
rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
[GOAL]
case intro
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 1 < Int.natAbs (eval (↑b) (cyclotomic (k + 1) ℤ))
[PROOFSTEP]
have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
[GOAL]
case intro
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
hb : 2 ≤ b
⊢ 1 < Int.natAbs (eval (↑b) (cyclotomic (k + 1) ℤ))
[PROOFSTEP]
calc
  1 ≤ b - 1 := le_tsub_of_add_le_left hb
  _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs := sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
let p := minFac (eval (↑b) (cyclotomic k ℤ)).natAbs
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) :=
  by
  have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
  rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, ← Int.cast_ofNat, this, eval₂_hom,
    Int.coe_castRingHom, ZMod.int_cast_zmod_eq_zero_iff_dvd _ _]
  apply Int.dvd_natAbs.1
  exact_mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
⊢ IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
[PROOFSTEP]
have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
⊢ ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
[PROOFSTEP]
simp
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
this : ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
⊢ IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
[PROOFSTEP]
rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, ← Int.cast_ofNat, this, eval₂_hom,
  Int.coe_castRingHom, ZMod.int_cast_zmod_eq_zero_iff_dvd _ _]
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
this : ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ eval (↑b) (cyclotomic k ℤ)
[PROOFSTEP]
apply Int.dvd_natAbs.1
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
this : ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ ↑(Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
[PROOFSTEP]
exact_mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
have hpb : ¬p ∣ b := hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
refine' ⟨p, hprime.1, not_le.1 fun habs => _, _⟩
[GOAL]
case inr.refine'_1
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
habs : p ≤ n
⊢ False
[PROOFSTEP]
exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
have hdiv : orderOf (b : ZMod p) ∣ p - 1 := ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
haveI : NeZero (k : ZMod p) := NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this : NeZero ↑k
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
rw [← this] at hdiv
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : k ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm
[GOAL]
k : ℕ
hk0 : k ≠ 0
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
refine' frequently_atTop.2 fun n => _
[GOAL]
k : ℕ
hk0 : k ≠ 0
n : ℕ
⊢ ∃ b, b ≥ n ∧ Prime b ∧ b ≡ 1 [MOD k]
[PROOFSTEP]
obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0
[GOAL]
case intro
k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b, b ≥ n ∧ Prime b ∧ b ≡ 1 [MOD k]
[PROOFSTEP]
exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩