case intro.intro.intro.intro.intro
α : Type ?u.96658
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'))
α : Type ?u.96658
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h : 3 ∈ cycleType g
⊢ IsThreeCycle (g * g)
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
case intro.intro.intro.intro.intro
α : Type ?u.96658
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')))
case intro.intro.intro.intro.intro
α : Type ?u.96658
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'))
simp only [mul_assoc]
case intro.intro.intro.intro.intro
α : Type ?u.96658
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))
case intro.intro.intro.intro.intro
α : Type ?u.96658
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')))
rw [hd.commute.eq, ← mul_assoc g']
case intro.intro.intro.intro.intro
α : Type ?u.96658
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))

case hg'
α : Type ?u.96658
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
case intro.intro.intro.intro.intro
α : Type ?u.96658
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))
suffices hg' : orderOf g' ∣ 2
case hg'
α : Type ?u.96658
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
case hg'
α : Type ?u.96658
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
rw [← lcm_cycleType, Multiset.lcm_dvd]
case hg'
α : Type ?u.96658
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
case hg'
α : Type ?u.96658
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
intro n hn
α : Type ?u.96658
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
case hg'
α : Type ?u.96658
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
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
case bc
α : Type ?u.96658
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.96658
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'
⊢ ℕ
α : Type ?u.96658
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
apply le_of_add_le_add_left
case bc
α : Type ?u.96658
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
case bc
α : Type ?u.96658
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.96658
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'
⊢ ℕ
rw [← hd.card_support_mul, h3]
no goals
case bc
α : Type ?u.96658
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
exact (c * g').support.card_le_univ
case intro.intro.intro.intro.intro
α : Type ?u.96658
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)
case intro.intro.intro.intro.intro
α : Type ?u.96658
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))
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
no goals
case intro.intro.intro.intro.intro
α : Type ?u.96658
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)
exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq