-- 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)
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 : Even g.cycleType.card
⊢ IsConj (swap 0 4 * swap 1 3) g

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

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 = 1
⊢ -1 ≠ 1

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 : Even g.cycleType.card
⊢ IsConj (swap 0 4 * swap 1 3) g

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 : Even g.cycleType.card
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate g.cycleType.card 2

Tactic:
interval_cases h_1 : Multiset.card g.cycleType

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

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

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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

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

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
⊢ ↑[2] + ↑[2] = Multiset.replicate 2 2

Tactic:
simp

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 : Even g.cycleType.card
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
rw [isConj_iff_cycleType_eq, h2]

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 : Even g.cycleType.card
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate g.cycleType.card 2

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 * 2 + g.cycleType.card) = 1
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
rw [pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] 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 : Even g.cycleType.card
⊢ IsConj (swap 0 4 * swap 1 3) g

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

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

Tactic:
simp at ha

Result:
no goals

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

Tactic:
contradiction

Result:
no goals

Proof state:
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

Tactic:
rw [← Multiset.eq_replicate_card] at h2

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

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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

Tactic:
have h04 : (0 : Fin 5) ≠ 4 := by decide

Result:
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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

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)
⊢ card (Fin 5) ≤ 3 * 2

Tactic:
norm_num only [card_fin]

Result:
no goals

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

Tactic:
decide

Result:
no goals

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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

Tactic:
have h13 : (1 : Fin 5) ≠ 3 := by decide

Result:
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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

Tactic:
rw [Disjoint.cycleType, (isCycle_swap h04).cycleType, (isCycle_swap h13).cycleType,
  card_support_swap h04, card_support_swap h13]

Result:
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
⊢ ↑[2] + ↑[2] = Multiset.replicate 2 2

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
⊢ (swap 0 4).Disjoint (swap 1 3)

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
⊢ (swap 0 4).Disjoint (swap 1 3)

Tactic:
rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13]

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