-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem mem_cycleType_iff {n : ℕ} {σ : Perm α} :
    n ∈ cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ c.support.card = n

Proof state:
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ l.prod.cycleType
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Tactic:
rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h

Result:
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Proof state:
case mp.mk.mk.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ c.Disjoint (l.erase c).prod

Tactic:
exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ σ.cycleType → ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ σ.cycleType
⊢ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Proof state:
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Tactic:
obtain ⟨c, cl, rfl⟩ := h

Result:
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ c_1.support.card = (Finset.card ∘ support) c

Proof state:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ σ.cycleType
⊢ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Tactic:
obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ

Result:
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ l.prod.cycleType
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Proof state:
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ c_1.support.card = (Finset.card ∘ support) c

Tactic:
rw [(List.perm_cons_erase cl).pairwise_iff @(Disjoint.symmetric)] at hld

Result:
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ c_1.support.card = (Finset.card ∘ support) c

Proof state:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : c.Disjoint t
hc : c.IsCycle
⊢ c.support.card ∈ (c * t).cycleType

Tactic:
simp [hd.cycleType, hc.cycleType]

Result:
no goals

Proof state:
case mp.mk.mk.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = c * (l.erase c).prod

Tactic:
rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ σ.cycleType ↔ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ σ.cycleType → ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n) → n ∈ σ.cycleType

Proof state:
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ c_1.support.card = (Finset.card ∘ support) c

Tactic:
refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩

Result:
case mp.mk.mk.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = c * (l.erase c).prod

case mp.mk.mk.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ c.Disjoint (l.erase c).prod

Proof state:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n) → n ∈ σ.cycleType

Tactic:
rintro ⟨c, t, rfl, hd, hc, rfl⟩

Result:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : c.Disjoint t
hc : c.IsCycle
⊢ c.support.card ∈ (c * t).cycleType