-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem isThreeCycle_sq_of_three_mem_cycleType_five {g : Perm (Fin 5)} (h : 3 ∈ cycleType g) :
    IsThreeCycle (g * g)

Proof state:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * (c * g'))).IsThreeCycle

Tactic:
rw [hd.commute.eq, ← mul_assoc g']

Result:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * g' * c)).IsThreeCycle

Proof state:
g : Perm (Fin 5)
h : 3 ∈ g.cycleType
⊢ (g * g).IsThreeCycle

Tactic:
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h

Result:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * g' * (c * g')).IsThreeCycle

Proof state:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
suffices hg' : orderOf g' ∣ 2 by
  rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
  exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq

Result:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ orderOf g' ∣ 2

Proof state:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ n ∣ 2

Tactic:
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]

Result:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ g'.support.card ≤ 2

Proof state:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]

Result:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * c).IsThreeCycle

Proof state:
case bc
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ (c * g').support.card ≤ 3 + 2

Tactic:
exact (c * g').support.card_le_univ

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ orderOf g' ∣ 2

Tactic:
rw [← lcm_cycleType, Multiset.lcm_dvd]

Result:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ ∀ b ∈ g'.cycleType, b ∣ 2

Proof state:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * g' * (c * g')).IsThreeCycle

Tactic:
simp only [mul_assoc]

Result:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * (c * g'))).IsThreeCycle

Proof state:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ ∀ b ∈ g'.cycleType, b ∣ 2

Tactic:
intro n hn

Result:
case intro.intro.intro.intro.intro
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ n ∣ 2

Proof state:
case bc
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ ?a + g'.support.card ≤ ?a + 2

case a
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ ℕ

Tactic:
rw [← hd.card_support_mul, h3]

Result:
case bc
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ (c * g').support.card ≤ 3 + 2

Proof state:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ g'.support.card ≤ 2

Tactic:
apply le_of_add_le_add_left

Result:
case bc
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ ?a + g'.support.card ≤ ?a + 2

case a
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ ℕ

Proof state:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * c).IsThreeCycle

Tactic:
exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq

Result:
no goals