-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_of_card_le_mem_cycleType_add_two {n : ℕ} {g : Perm α}
    (hn2 : Fintype.card α < n + 2) (hng : n ∈ g.cycleType) : g.cycleType = {n}

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
g : Perm α
hn2 : Fintype.card α < n + 2
hng : n ∈ g.cycleType
⊢ g.cycleType = {n}

Tactic:
obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < c.support.card + 2
hng : c.support.card ∈ (c * g').cycleType
⊢ (c * g').cycleType = {c.support.card}

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ c.support.card + 2 ≤ Fintype.card α

Tactic:
apply le_trans _ (c * g').support.card_le_univ

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ c.support.card + 2 ≤ (c * g').support.card

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ c.support.card + 2 ≤ c.support.card + g'.support.card

Tactic:
exact add_le_add_left (two_le_card_support_of_ne_one g'1) _

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < c.support.card + 2
hng : c.support.card ∈ (c * g').cycleType
⊢ g' = 1

Tactic:
contrapose! hn2 with g'1

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ c.support.card + 2 ≤ Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ c.support.card + 2 ≤ (c * g').support.card

Tactic:
rw [hd.card_support_mul]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ c.support.card + 2 ≤ c.support.card + g'.support.card

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < c.support.card + 2
hng : c.support.card ∈ (c * g').cycleType
⊢ (c * g').cycleType = {c.support.card}

Tactic:
suffices g'1 : g' = 1 by
  rw [hd.cycleType, hc.cycleType, coe_singleton, g'1, cycleType_one, add_zero]

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < c.support.card + 2
hng : c.support.card ∈ (c * g').cycleType
⊢ g' = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < c.support.card + 2
hng : c.support.card ∈ (c * g').cycleType
g'1 : g' = 1
⊢ (c * g').cycleType = {c.support.card}

Tactic:
rw [hd.cycleType, hc.cycleType, coe_singleton, g'1, cycleType_one, add_zero]

Result:
no goals