ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha : a ∈ {a | a ∈ l}
b : α
hb : b ∈ {a | a ∈ l}
⊢ SameCycle (List.formPerm l) a b
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
⊢ IsCycleOn (List.formPerm l) {a | a ∈ l}
refine' ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => _⟩
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ SameCycle (List.formPerm l) a b
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha : a ∈ {a | a ∈ l}
b : α
hb : b ∈ {a | a ∈ l}
⊢ SameCycle (List.formPerm l) a b
rw [Set.mem_setOf, ← List.indexOf_lt_length] at ha hb
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ SameCycle (List.formPerm l) (List.get l { val := List.indexOf a l, isLt := ha })
    (List.get l { val := List.indexOf b l, isLt := hb })
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ SameCycle (List.formPerm l) a b
rw [← List.indexOf_get ha, ← List.indexOf_get hb]
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ ↑(List.formPerm l ^ (↑(List.indexOf b l) - ↑(List.indexOf a l)))
      (List.get l { val := List.indexOf a l, isLt := ha }) =
    List.get l { val := List.indexOf b l, isLt := hb }
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ SameCycle (List.formPerm l) (List.get l { val := List.indexOf a l, isLt := ha })
    (List.get l { val := List.indexOf b l, isLt := hb })
refine' ⟨l.indexOf b - l.indexOf a, _⟩
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ List.nthLe l ((List.indexOf a l + List.indexOf b l) % List.length l)
      (_ : (List.indexOf a l + List.indexOf b l) % List.length l < List.length l) =
    List.nthLe l ((List.indexOf b l + List.indexOf a l) % List.length l)
      (_ : (List.indexOf b l + List.indexOf a l) % List.length l < List.length l)
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ ↑(List.formPerm l ^ (↑(List.indexOf b l) - ↑(List.indexOf a l)))
      (List.get l { val := List.indexOf a l, isLt := ha }) =
    List.get l { val := List.indexOf b l, isLt := hb }
simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_ofNat,
  Equiv.Perm.coe_mul, ← List.nthLe_eq, List.formPerm_pow_apply_nthLe _ h, Function.comp]
no goals
ι : Type ?u.3063559
α : Type u_1
β : Type ?u.3063565
inst✝¹ inst✝ : DecidableEq α
l : List α
h : List.Nodup l
a : α
ha✝ : a ∈ l
ha : List.indexOf a l < List.length l
b : α
hb✝ : b ∈ l
hb : List.indexOf b l < List.length l
⊢ List.nthLe l ((List.indexOf a l + List.indexOf b l) % List.length l)
      (_ : (List.indexOf a l + List.indexOf b l) % List.length l < List.length l) =
    List.nthLe l ((List.indexOf b l + List.indexOf a l) % List.length l)
      (_ : (List.indexOf b l + List.indexOf a l) % List.length l < List.length l)
rw [add_comm]