case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
⊢ cycleType (c * g') = {Finset.card (support c)}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
g : Perm α
hn2 : Fintype.card α < n + 2
hng : n ∈ cycleType g
⊢ cycleType g = {n}
obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : g' = 1
⊢ cycleType (c * g') = {Finset.card (support c)}

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
⊢ cycleType (c * g') = {Finset.card (support c)}
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
⊢ cycleType (c * g') = {Finset.card (support c)}
by_cases g'1 : g' = 1
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Fintype.card α
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
⊢ cycleType (c * g') = {Finset.card (support c)}
contrapose! hn2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Finset.card (support (c * g'))
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Fintype.card α
apply le_trans _ (c * g').support.card_le_univ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Finset.card (support c) + Finset.card (support g')
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Finset.card (support (c * g'))
rw [hd.card_support_mul]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Finset.card (support c) + Finset.card (support g')
exact add_le_add_left (two_le_card_support_of_ne_one g'1) _
no goals
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : g' = 1
⊢ cycleType (c * g') = {Finset.card (support c)}
rw [hd.cycleType, hc.cycleType, coe_singleton, g'1, cycleType_one, add_zero]