case zero
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (rotate l Nat.zero) = formPerm l

case succ
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ formPerm (rotate l (Nat.succ n)) = formPerm l
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
⊢ formPerm (rotate l n) = formPerm l
induction' n with n hn
no goals
case zero
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (rotate l Nat.zero) = formPerm l
simp
case succ.h
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ Nodup (rotate l n)
case succ
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ formPerm (rotate l (Nat.succ n)) = formPerm l
rw [Nat.succ_eq_add_one, ← rotate_rotate, formPerm_rotate_one, hn]
case succ.h
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ rotate l n ~r l
case succ.h
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ Nodup (rotate l n)
rwa [IsRotated.nodup_iff]
no goals
case succ.h
α : Type u_1
β : Type ?u.773582
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ rotate l n ~r l
exact IsRotated.forall l n