α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
key : Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
⊢ toCycle f hf = ↑(toList f x)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ toCycle f hf = ↑(toList f x)
have key : (Finset.univ : Finset α).val = x ::ₘ Finset.univ.val.erase x := by simp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
key : Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
⊢ Multiset.recOn (x ::ₘ Multiset.erase Finset.univ.val x) (Quot.mk Setoid.r [])
      (fun x x_1 l => if ↑f x = x then l else ↑(toList f x))
      (_ :
        ∀ (x y : α),
          Multiset α →
            ∀ (s : Cycle α),
              HEq (if ↑f x = x then if ↑f y = y then s else ↑(toList f y) else ↑(toList f x))
                (if ↑f y = y then if ↑f x = x then s else ↑(toList f x) else ↑(toList f y))) =
    ↑(toList f x)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
key : Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
⊢ toCycle f hf = ↑(toList f x)
rw [toCycle, key]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
key : Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
⊢ Multiset.recOn (x ::ₘ Multiset.erase Finset.univ.val x) (Quot.mk Setoid.r [])
      (fun x x_1 l => if ↑f x = x then l else ↑(toList f x))
      (_ :
        ∀ (x y : α),
          Multiset α →
            ∀ (s : Cycle α),
              HEq (if ↑f x = x then if ↑f y = y then s else ↑(toList f y) else ↑(toList f x))
                (if ↑f y = y then if ↑f x = x then s else ↑(toList f x) else ↑(toList f y))) =
    ↑(toList f x)
simp [hx]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
simp