α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
⊢ l = l'
α : Type u
n : ℕ
⊢ Injective fun l => rotate l n
rintro l l' (h : l.rotate n = l'.rotate n)
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
hle : length l = length l'
⊢ l = l'
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
⊢ l = l'
have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ l = l'
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
hle : length l = length l'
⊢ l = l'
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h
case intro
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
hd : drop (n % length l) l = drop (n % length l') l'
ht : take (n % length l) l = take (n % length l') l'
⊢ l = l'
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ l = l'
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
no goals
case intro
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
hd : drop (n % length l) l = drop (n % length l') l'
ht : take (n % length l) l = take (n % length l') l'
⊢ l = l'
rw [← take_append_drop _ l, ht, hd, take_append_drop]
no goals
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ length (drop (n % length l) l) = length (drop (n % length l') l')
simp_all