-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem isConj_swap_mul_swap_of_cycleType_two {g : Perm (Fin 5)} (ha : g ∈ alternatingGroup (Fin 5))
    (h1 : g ≠ 1) (h2 : ∀ n, n ∈ cycleType (g : Perm (Fin 5)) → n = 2) :
    IsConj (swap 0 4 * swap 1 3) g

Proof state:
g : Perm (Fin 5)
ha : (-1) ^ ((Multiset.replicate g.cycleType.card 2).sum + (Multiset.replicate g.cycleType.card 2).card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
norm_num at ha

Result:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : (-1) ^ (g.cycleType.card * 2 + g.cycleType.card) = 1
⊢ IsConj (swap 0 4 * swap 1 3) g

Proof state:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ 0 < 2

Tactic:
simp

Result:
no goals

Proof state:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha

Result:
g : Perm (Fin 5)
ha : (-1) ^ ((Multiset.replicate g.cycleType.card 2).sum + (Multiset.replicate g.cycleType.card 2).card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Proof state:
case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = 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}

Tactic:
decide

Result:
no goals

Proof state:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : (-1) ^ g.cycleType.card = 1
⊢ -1 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
have h : Multiset.card g.cycleType ≤ 3 :=
  le_of_mul_le_mul_right (le_trans h (by norm_num only [card_fin])) (by simp)

Result:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Proof state:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
⊢ 1 ≠ 3

Tactic:
decide

Result:
no goals

Proof state:
case «0»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 0
h2 : g.cycleType = Multiset.replicate 0 2
h✝ : 0 * 2 ≤ card (Fin 5)
h : 0 ≤ 3
ha : Even 0
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 0 2

Tactic:
exact (h1 (card_cycleType_eq_zero.1 h_1)).elim

Result:
no goals

Proof state:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
have h := g.support.card_le_univ

Result:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
h : g.support.card ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g

Proof state:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.support.card ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h

Result:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g