case intro.intro
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
l : List (Perm α)
hl : List.Nodup l
hl' : List.toFinset l = cycleFactorsFinset f
⊢ p ∈ cycleFactorsFinset f ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
⊢ p ∈ cycleFactorsFinset f ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
case intro.intro
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
l : List (Perm α)
hl : List.Nodup l
hl' : List.toFinset l = cycleFactorsFinset f
⊢ p ∈ List.toFinset l ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
case intro.intro
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
l : List (Perm α)
hl : List.Nodup l
hl' : List.toFinset l = cycleFactorsFinset f
⊢ p ∈ cycleFactorsFinset f ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
rw [← hl']
case intro.intro
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
l : List (Perm α)
hl : List.Nodup l
hl' : (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = f
⊢ p ∈ List.toFinset l ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
case intro.intro
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
l : List (Perm α)
hl : List.Nodup l
hl' : List.toFinset l = cycleFactorsFinset f
⊢ p ∈ List.toFinset l ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
no goals
case intro.intro
ι : Type ?u.2735472
α : Type u_1
β : Type ?u.2735478
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f p : Perm α
l : List (Perm α)
hl : List.Nodup l
hl' : (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = f
⊢ p ∈ List.toFinset l ↔ IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
simpa [List.mem_toFinset, Ne.def, ← hl'.right.right] using
  mem_list_cycles_iff hl'.left hl'.right.left