α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (rotate l n) m = get? l ((m + n) % length l)
rw [rotate_eq_drop_append_take_mod]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)

case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
rcases lt_or_le m (l.drop (n % l.length)).length with hm | hm
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
rw [get?_append hm, get?_drop, add_comm m, ← mod_add_mod]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm✝ : m < length l - n % length l
hm : n % length l + m < length l
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
rw [length_drop, lt_tsub_iff_left] at hm
no goals
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm✝ : m < length l - n % length l
hm : n % length l + m < length l
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
rw [mod_eq_of_lt hm]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? l (m - (length l - n % length l)) = get? l ((m + n) % length l)

case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - length (drop (n % length l) l) < n % length l
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
rw [get?_append_right hm, get?_take, length_drop]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? l (m - (length l - n % length l)) = get? l ((m + n) % length l)
congr 1
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
rw [length_drop] at hm
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ m - (length l - n % length l) = (m + n) % length l
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
have hm' := tsub_le_iff_left.1 hm
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m - length l < length l

case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ m - (length l - n % length l) = (m + n) % length l
have : n % length l + m - length l < length l
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = n % length l + m - length l
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
conv_rhs => rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l ≤ n % length l + m

case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ n % length l ≤ length l

case inr.e_a.h
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l - n % length l ≤ m
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = n % length l + m - length l
rw [← add_right_inj l.length, ← add_tsub_assoc_of_le, add_tsub_tsub_cancel,
  add_tsub_cancel_of_le, add_comm]
no goals
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l ≤ n % length l + m

case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ n % length l ≤ length l

case inr.e_a.h
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l - n % length l ≤ m
exacts [hm', hlt.le, hm]
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m < length l + length l
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m - length l < length l
rw [tsub_lt_iff_left hm']
no goals
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m < length l + length l
exact Nat.add_lt_add hlt hml
no goals
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - length (drop (n % length l) l) < n % length l
rwa [tsub_lt_iff_left hm, length_drop, tsub_add_cancel_of_le hlt.le]