case zero
α : Type u_1
β : Type ?u.779543
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
⊢ ↑(formPerm l ^ Nat.zero) (nthLe l k hk) =
    nthLe l ((k + Nat.zero) % length l) (_ : (k + Nat.zero) % length l < length l)

case succ
α : Type u_1
β : Type ?u.779543
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
n : ℕ
hn : ↑(formPerm l ^ n) (nthLe l k hk) = nthLe l ((k + n) % length l) (_ : (k + n) % length l < length l)
⊢ ↑(formPerm l ^ Nat.succ n) (nthLe l k hk) =
    nthLe l ((k + Nat.succ n) % length l) (_ : (k + Nat.succ n) % length l < length l)
α : Type u_1
β : Type ?u.779543
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n k : ℕ
hk : k < length l
⊢ ↑(formPerm l ^ n) (nthLe l k hk) = nthLe l ((k + n) % length l) (_ : (k + n) % length l < length l)
induction' n with n hn
no goals
case zero
α : Type u_1
β : Type ?u.779543
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
⊢ ↑(formPerm l ^ Nat.zero) (nthLe l k hk) =
    nthLe l ((k + Nat.zero) % length l) (_ : (k + Nat.zero) % length l < length l)
simp [Nat.mod_eq_of_lt hk]
no goals
case succ
α : Type u_1
β : Type ?u.779543
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
n : ℕ
hn : ↑(formPerm l ^ n) (nthLe l k hk) = nthLe l ((k + n) % length l) (_ : (k + n) % length l < length l)
⊢ ↑(formPerm l ^ Nat.succ n) (nthLe l k hk) =
    nthLe l ((k + Nat.succ n) % length l) (_ : (k + Nat.succ n) % length l < length l)
simp [pow_succ, mul_apply, hn, formPerm_apply_nthLe _ h, Nat.succ_eq_add_one, ← Nat.add_assoc]