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

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n) → n ∈ cycleType σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
constructor
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ cycleType σ
⊢ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ cycleType σ → ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
intro h
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ cycleType (List.prod l)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, List.prod l = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ cycleType σ
⊢ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a, a ∈ l ∧ (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, List.prod l = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ cycleType (List.prod l)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, List.prod l = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ c_1 τ, List.prod l = c_1 * τ ∧ Disjoint c_1 τ ∧ IsCycle c_1 ∧ Finset.card (support c_1) = (Finset.card ∘ support) c
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a, a ∈ l ∧ (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, List.prod l = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
obtain ⟨c, cl, rfl⟩ := h
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ ∃ c_1 τ, List.prod l = c_1 * τ ∧ Disjoint c_1 τ ∧ IsCycle c_1 ∧ Finset.card (support c_1) = (Finset.card ∘ support) c
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ c_1 τ, List.prod l = c_1 * τ ∧ Disjoint c_1 τ ∧ IsCycle c_1 ∧ Finset.card (support c_1) = (Finset.card ∘ support) c
rw [(List.perm_cons_erase cl).pairwise_iff Disjoint.symmetric] at hld
case mp.mk.mk.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ List.prod l = c * List.prod (List.erase l c)

case mp.mk.mk.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ Disjoint c (List.prod (List.erase l c))
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ ∃ c_1 τ, List.prod l = c_1 * τ ∧ Disjoint c_1 τ ∧ IsCycle c_1 ∧ Finset.card (support c_1) = (Finset.card ∘ support) c
refine' ⟨c, (l.erase c).prod, _, _, hlc _ cl, rfl⟩
no goals
case mp.mk.mk.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ List.prod l = c * List.prod (List.erase l c)
rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
no goals
case mp.mk.mk.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ Disjoint c (List.prod (List.erase l c))
exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : Disjoint c t
hc : IsCycle c
⊢ Finset.card (support c) ∈ cycleType (c * t)
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n) → n ∈ cycleType σ
rintro ⟨c, t, rfl, hd, hc, rfl⟩
no goals
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : Disjoint c t
hc : IsCycle c
⊢ Finset.card (support c) ∈ cycleType (c * t)
simp [hd.cycleType, hc.cycleType]