awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
inl : ∀ (hl : 0 = l.length), l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
have inr : ∀ (hl : 0 < l.length), l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
Tactic: rcases l.length.zero_le.eq_or_lt with hl | hl
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
have inr : l.rotate n = l.rotate (n % l.length)
Tactic: rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
inr : l.rotate n = l.rotate (n % l.length)
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
have inr₁ : l.rotate n = l.rotate n
Tactic: rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l
have rw : (l ++ l').rotate' l.length = l' ++ l
Tactic: rw [rotate_eq_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ (l ++ l').rotate' l.length = l' ++ l
have nil : ∀ (l' : List α), ([] ++ l').rotate' (length.{u} (α := α) []) = l' ++ []
Tactic: induction l generalizing l'
Cleared hypotheses: l, l'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
nil : ∀ (l' : List α), ([] ++ l').rotate' (length.{u} (α := α) []) = l' ++ []
⊢ (l ++ l').rotate' l.length = l' ++ l
have cons : ∀ (head : α) (tail : List α),
  (∀ (l' : List α), (tail ++ l').rotate' tail.length = l' ++ tail) →
    ∀ (l' : List α), (head :: tail ++ l').rotate' (head :: tail).length = l' ++ head :: tail
Tactic: induction l generalizing l'
Cleared hypotheses: l, l'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
⊢ (l.rotate n).rotate m = l.rotate (n + m)
have rw : (l.rotate n).rotate' m = l.rotate (n + m)
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
rw : (l.rotate n).rotate' m = l.rotate (n + m)
⊢ (l.rotate n).rotate m = l.rotate (n + m)
have rw₁ : (l.rotate' n).rotate' m = l.rotate (n + m)
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
rw : (l.rotate n).rotate' m = l.rotate (n + m)
rw₁ : (l.rotate' n).rotate' m = l.rotate (n + m)
⊢ (l.rotate n).rotate m = l.rotate (n + m)
have rw₂ : (l.rotate' n).rotate' m = l.rotate' (n + m)
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
rw : (l.rotate n).rotate' m = l.rotate (n + m)
rw₁ : (l.rotate' n).rotate' m = l.rotate (n + m)
rw₂ : (l.rotate' n).rotate' m = l.rotate' (n + m)
⊢ (l.rotate n).rotate m = l.rotate (n + m)
have rw₃ : l.rotate' (n + m) = l.rotate' (n + m)
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
⊢ l.rotate l.length = l
have rw : l.rotate' l.length = l
Tactic: rw [rotate_eq_rotate', rotate'_length]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
rw : l.rotate' l.length = l
⊢ l.rotate l.length = l
have rw₁ : l = l
Tactic: rw [rotate_eq_rotate', rotate'_length]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate (l.length * n) = l
have rw : l.rotate' (l.length * n) = l
Tactic: rw [rotate_eq_rotate', rotate'_length_mul]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate' (l.length * n) = l
⊢ l.rotate (l.length * n) = l
have rw₁ : l = l
Tactic: rw [rotate_eq_rotate', rotate'_length_mul]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l
have rw : l.rotate' n ~ l
Tactic: rw [rotate_eq_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
⊢ l.rotate' (n + 1) ~ l
have succ : Perm.{u} (α := α) (rotate' [] (n + 1)) []
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
succ : Perm.{u} (α := α) (rotate' [] (n + 1)) []
⊢ l.rotate' (n + 1) ~ l
have succ₁ : ∀ (hd : α) (tl : List α), (hd :: tl).rotate' (n + 1) ~ hd :: tl
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl
have succ : (tl ++ [hd]).rotate' n ~ hd :: tl
Tactic: rw [rotate'_cons_succ]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' n ~ l
have zero : ∀ (l : List α), l.rotate' 0 ~ l
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ (l : List α), l.rotate' 0 ~ l
⊢ l.rotate' n ~ l
have succ : ∀ (n : ℕ) (hn : ∀ (l : List α), l.rotate' n ~ l) (l : List α), l.rotate' (n + 1) ~ l
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
⊢ l.rotate (n + 1) = [] ↔ l = []
have succ : Eq.{u + 1} (α := List α) (rotate [] (n + 1)) [] ↔ Eq.{u + 1} (α := List α) [] []
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
succ : Eq.{u + 1} (α := List α) (rotate [] (n + 1)) [] ↔ Eq.{u + 1} (α := List α) [] []
⊢ l.rotate (n + 1) = [] ↔ l = []
have succ₁ : ∀ (hd : α) (tl : List α), (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ l = []
have zero : ∀ {l : List α}, l.rotate 0 = [] ↔ l = []
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [rotate_cons_succ, hn]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ {l : List α}, l.rotate 0 = [] ↔ l = []
⊢ l.rotate n = [] ↔ l = []
have succ : ∀ (n : ℕ) (hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []) {l : List α}, l.rotate (n + 1) = [] ↔ l = []
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [rotate_cons_succ, hn]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ [] = l.rotate n ↔ [] = l
have rw : l.rotate n = [] ↔ [] = l
Tactic: rw [eq_comm, rotate_eq_nil_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate n = [] ↔ [] = l
⊢ [] = l.rotate n ↔ [] = l
have rw₁ : l = [] ↔ [] = l
Tactic: rw [eq_comm, rotate_eq_nil_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate n = [] ↔ [] = l
rw₁ : l = [] ↔ [] = l
⊢ [] = l.rotate n ↔ [] = l
have rw₂ : [] = l ↔ [] = l
Tactic: rw [eq_comm, rotate_eq_nil_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)
have rw : (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
Tactic: rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod,
    rotate_eq_drop_append_take_mod, h, zipWith_append, ← drop_zipWith, ←
    take_zipWith, List.length_zipWith, h, min_self]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
have rw : l.length - n % l'.length = (drop (n % l'.length) l').length
Tactic: rw [length_drop, length_drop, h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
rw : l.length - n % l'.length = (drop (n % l'.length) l').length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
have rw₁ : l.length - n % l'.length = l'.length - n % l'.length
Tactic: rw [length_drop, length_drop, h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
rw : l.length - n % l'.length = (drop (n % l'.length) l').length
rw₁ : l.length - n % l'.length = l'.length - n % l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
have rw₂ : l'.length - n % l'.length = l'.length - n % l'.length
Tactic: rw [length_drop, length_drop, h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
Tactic: rw [rotate_eq_drop_append_take_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have inl : ∀ (hm : m < (drop (n % l.length) l).length),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
Tactic: rcases lt_or_ge m (l.drop (n % l.length)).length with hm | hm
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
inl :
  ∀ (hm : m < (drop (n % l.length) l).length),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have inr : ∀ (hm : (drop (n % l.length) l).length ≤ m),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
Tactic: rcases lt_or_ge m (l.drop (n % l.length)).length with hm | hm
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have inl : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n % l.length) % l.length)
Tactic: rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n % l.length) % l.length)
have hm₁ : m + n % l.length < l.length
Tactic: rw [length_drop, Nat.lt_sub_iff_add_lt] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n % l.length) % l.length)
have inl : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length)
Tactic: rw [mod_eq_of_lt hm, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
inl :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n % l.length) % l.length)
have inl₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length)
Tactic: rw [mod_eq_of_lt hm, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have hlt : n % l.length < l.length
Tactic: have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have inr : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m - (l.length - n % l.length)) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
Tactic: rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
inr :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m - (l.length - n % l.length)) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have inr₁ : m - (drop (n % l.length) l).length < n % l.length
Tactic: rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m - (l.length - n % l.length)) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
have inr : m - (l.length - n % l.length) = (m + n) % l.length
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length
have hm₁ : l.length - n % l.length ≤ m
Tactic: rw [length_drop] at hm
Cleared hypotheses: hm, hlt
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length
have hm' : l.length ≤ n % l.length + m
Tactic: have hm' := Nat.sub_le_iff_le_add'.1 hm
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m - l.length < l.length
have rw : n % l.length + m < l.length + l.length
Tactic: rw [Nat.sub_lt_iff_lt_add hm']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ m - (l.length - n % l.length) = (m + n) % l.length
have this : n % l.length + m - l.length < l.length
Tactic: have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
| (m + n) % l.length
have rw : n % l.length + m - l.length
Tactic: rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length
have inr : m - (l.length - n % l.length) = n % l.length + m - l.length
Tactic: conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
have inr : m < (drop (n % l.length) l).length + n % l.length
Tactic: rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
inr : m < (drop (n % l.length) l).length + n % l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
have inr₁ : m < l.length - n % l.length + n % l.length
Tactic: rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) k h =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + n) % l.length) ⋯
have rw : k < l.length
Tactic: rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n).head? = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) 0 =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
Tactic: rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) 0 =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
⊢ (l.rotate n).head? = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
have rw₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((0 + n) % l.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
Tactic: rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) 0 =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
rw₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((0 + n) % l.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
⊢ (l.rotate n).head? = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
have rw₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
Tactic: rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) 0 =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
rw₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((0 + n) % l.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
rw₂ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
⊢ (l.rotate n).head? = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
have rw₃ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
Tactic: rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) ((l.length - n % l.length + k) % l.length)
      ⋯
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l
    (((l.length - n % l.length + k) % l.length + n) % l.length) sorry
Tactic: rw [getElem_rotate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l
      (((l.length - n % l.length + k) % l.length + n) % l.length) ⋯
have refine : (↑(⟨k, hk⟩ : Fin l.length) : ℕ) = (↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, sorry⟩ : ℕ)
Tactic: refine congr_arg l.get (Fin.eq_of_val_eq ?_)