case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l → n % length l = 0 ∨ l = []

case mpr
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ n % length l = 0 ∨ l = [] → rotate l n = l
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l ↔ n % length l = 0 ∨ l = []
constructor
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
⊢ n % length l = 0 ∨ l = []
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l → n % length l = 0 ∨ l = []
intro h
case mp.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 = length l
⊢ n % length l = 0 ∨ l = []

case mp.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0 ∨ l = []
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
⊢ n % length l = 0 ∨ l = []
cases' l.length.zero_le.eq_or_lt with hl' hl'
case mp.inr.h
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
case mp.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0 ∨ l = []
left
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
case mp.inr.h
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
rw [nodup_iff_nthLe_inj] at hl
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe l (n % length l) (_ : n % length l < length l) = nthLe l 0 hl'
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
refine' hl _ _ (mod_lt _ hl') hl' _
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe (rotate l n) ((length l - n % length l + n % length l) % length l)
      (_ : (length l - n % length l + n % length l) % length l < length (rotate l n)) =
    nthLe l 0 hl'
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe l (n % length l) (_ : n % length l < length l) = nthLe l 0 hl'
rw [← nthLe_rotate' _ n]
no goals
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe (rotate l n) ((length l - n % length l + n % length l) % length l)
      (_ : (length l - n % length l + n % length l) % length l < length (rotate l n)) =
    nthLe l 0 hl'
simp_rw [h, tsub_add_cancel_of_le (mod_lt _ hl').le, mod_self]
no goals
case mp.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 = length l
⊢ n % length l = 0 ∨ l = []
simp [← length_eq_zero, ← hl']
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l n = l

case mpr.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : l = []
⊢ rotate l n = l
case mpr
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ n % length l = 0 ∨ l = [] → rotate l n = l
rintro (h | h)
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l 0 = l
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l n = l
rw [← rotate_mod, h]
no goals
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l 0 = l
exact rotate_zero l
no goals
case mpr.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : l = []
⊢ rotate l n = l
simp [h]