awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ drop (n % l.length) l = drop (n % l'.length) l'

Tactic:
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)

Premises used: List.append_inj
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
⊢ take (n % l.length) l = take (n % l'.length) l'

Tactic:
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)

Premises used: List.append_inj
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
rw : take (n % l.length) l ++ drop (n % l.length) l = l'
rw₁ : ℕ
rw₂ : take (n % l'.length) l' ++ drop (n % l.length) l = l'
rw₃ : take (n % l'.length) l' ++ drop (n % l'.length) l' = l'
rw₄ rw₅ : l' = l'
⊢ l = l'

Tactic:
rw [← take_append_drop _ l, ht, hd, take_append_drop]

Premises used: List.take_append_drop
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l'.rotate n ↔ l = l'

Tactic:
(rotate_injective n).eq_iff

Premises used: Function.Injective.eq_iff, List.rotate_injective
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
rw : l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]

Premises used: List.rotate_rotate, List.rotate_mod, Nat.add_mod, List.rotate_eq_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
inl :
  ∀ (hl : 0 = l'.length),
    l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
inr :
  ∀ (hl : 0 < l'.length),
    l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rcases l'.length.zero_le.eq_or_lt with hl | hl

Premises used: Nat.zero_le, LE.le.eq_or_lt, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
inl :
  l.rotate n = [] ↔
    l.rotate n =
      rotate []
        (((length.{u} (α := α) [] - n % length.{u} (α := α) []) % length.{u} (α := α) [] + n % length.{u} (α := α) []) %
          length.{u} (α := α) [])
inl₁ inl₂ : l.rotate n = [] ↔ l.rotate n = []
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]

Premises used: List.rotate_nil, List.eq_nil_of_length_eq_zero, Eq.symm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
inr :
  ∀ (hn : 0 = n % l'.length),
    l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
inr₁ :
  ∀ (hn : 0 < n % l'.length),
    l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn

Premises used: Nat.zero_le, LE.le.eq_or_lt, HMod.hMod, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 = n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
simp [← hn]
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
inr : n % l'.length ≤ l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]

Premises used: Nat.mod_self, Nat.sub_lt, Nat.mod_eq_of_lt, Nat.sub_add_cancel, List.rotate_zero
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length

Tactic:
(Nat.mod_lt _ hl).le

Premises used: LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length

Tactic:
exact (Nat.mod_lt _ hl).le

Premises used: LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
x : α
rw : l = [x].rotate ([x].length - n % [x].length) ↔ l = [x]
rw₁ rw₂ : l = [x] ↔ l = [x]
⊢ l.rotate n = [x] ↔ l = [x]

Tactic:
rw [rotate_eq_iff, rotate_singleton]

Premises used: List.rotate_singleton, List.rotate_eq_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
x : α
rw : l.rotate n = [x] ↔ [x] = l
rw₁ : l = [x] ↔ [x] = l
rw₂ rw₃ : [x] = l ↔ [x] = l
⊢ [x] = l.rotate n ↔ [x] = l

Tactic:
rw [eq_comm, rotate_eq_singleton_iff, eq_comm]

Premises used: List.rotate_eq_singleton_iff, eq_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : (l.rotate n).reverse.rotate n = l.reverse
⊢ (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)

Tactic:
rw [← length_reverse, ← rotate_eq_iff]

Premises used: List.length_reverse, List.rotate_eq_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ (l.rotate 0).reverse.rotate 0 = l.reverse

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
succ : Eq.{u + 1} (α := List α) (rotate (reverse (rotate [] (n + 1))) (n + 1)) (reverse [])
succ₁ : ∀ (hd : α) (tl : List α), ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
⊢ Eq.{u + 1} (α := List α) (rotate (reverse (rotate [] (n + 1))) (n + 1)) (reverse [])

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
succ : (tl ++ [hd]).reverse.rotate 1 = (hd :: tl).reverse
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse

Tactic:
rw [rotate_cons_succ, ← rotate_rotate, hn]

Premises used: List.rotate_cons_succ, List.rotate_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ (tl ++ [hd]).reverse.rotate 1 = (hd :: tl).reverse

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ (l : List α), (l.rotate 0).reverse.rotate 0 = l.reverse
succ :
  ∀ (n : ℕ) (hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse) (l : List α),
    (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse
⊢ (l.rotate n).reverse.rotate n = l.reverse

Tactic:
induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp

Premises used: List.rotate_cons_succ, List.rotate_rotate, Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw :
  l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse
⊢ l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Tactic:
rw [← reverse_reverse l]

Premises used: List.reverse_reverse
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
simp_rw : l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))
⊢ l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse

Tactic:
simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
    length_reverse]

Premises used: List.length_reverse, List.length_rotate, List.rotate_rotate, List.reverse_rotate, List.rotate_eq_iff, List.reverse_reverse
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw :
  l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
⊢ l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))

Tactic:
rw [← length_reverse]

Premises used: List.length_reverse
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
zero :
  ∀ (hk' : k = 0),
    l.reverse =
      l.reverse.rotate
        (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
          (l.reverse.length - n % l.reverse.length))
succ :
  ∀ (k' : ℕ) (hk' : k = k' + 1),
    l.reverse =
      l.reverse.rotate
        (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
          (l.reverse.length - n % l.reverse.length))
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
rcases hk' : k with - | k'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
hk' : k = 0
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
simp_all! [k, length_reverse, ← rotate_rotate]

Premises used: List.length_reverse, List.rotate_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
succ :
  let k := n % length.{u} (α := α) (reverse []);
  ∀ (hk' : k = k' + 1),
    Eq.{u + 1} (α := List α) (reverse [])
      (rotate (reverse [])
        (length.{u} (α := α) (reverse []) -
            (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse [])) %
              length.{u} (α := α) (reverse []) +
          (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse []))))
succ₁ :
  ∀ (x : α) (l : List α),
    let k := n % (x :: l).reverse.length;
    ∀ (hk' : k = k' + 1),
      (x :: l).reverse =
        (x :: l).reverse.rotate
          ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
            ((x :: l).reverse.length - n % (x :: l).reverse.length))
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
rcases l with - | ⟨x, l⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
k : ℕ := n % length.{u} (α := α) (reverse [])
hk' : k = k' + 1
⊢ Eq.{u + 1} (α := List α) (reverse [])
    (rotate (reverse [])
      (length.{u} (α := α) (reverse []) -
          (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse [])) % length.{u} (α := α) (reverse []) +
        (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse []))))

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
succ : (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length
succ₁ : (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]

Premises used: List.rotate_length, Nat.mod_eq_of_lt, Nat.sub_add_cancel
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

Tactic:
Nat.sub_le _ _

Premises used: Nat.sub_le
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

Tactic:
exact Nat.sub_le _ _

Premises used: Nat.sub_le
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < (x :: l).reverse.length

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < n % (x :: l).reverse.length

Tactic:
simp_all! [k]
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Tactic:
exact Nat.sub_lt (by simp) (by simp_all! [k])

Premises used: Nat.sub_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
f : α → β
l : List α
⊢ map f (l.rotate 0) = (map f l).rotate 0

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
succ : map f (rotate [] (n + 1)) = (map f []).rotate (n + 1)
succ₁ : ∀ (hd : α) (tl : List α), map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
⊢ map f (rotate [] (n + 1)) = (map f []).rotate (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)

Tactic:
simp [hn]
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
zero : ∀ (l : List α), map f (l.rotate 0) = (map f l).rotate 0
succ :
  ∀ (n : ℕ) (hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n) (l : List α),
    map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)
⊢ map f (l.rotate n) = (map f l).rotate n

Tactic:
induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [hn]

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate i = l.rotate j
⊢ l.rotate (i % l.length) = l.rotate (j % l.length)

Tactic:
rw [← rotate_mod l i, ← rotate_mod l j] at h

Premises used: List.rotate_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length

Tactic:
simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj,
    hl.getElem_inj_iff, Fin.ext_iff] using congr_arg head? h

Premises used: List.head?, Fin.ext_iff, List.Nodup.getElem_inj_iff, Nat.mod_lt, congr_arg, List.getElem?_eq_getElem, List.length_pos_of_ne_nil, List.head?_rotate, Option.some_inj
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
inl :
  ∀ (hl : Nodup.{u} (α := α) []),
    Eq.{u + 1} (α := List α) (rotate [] i) (rotate [] j) ↔
      i % length.{u} (α := α) [] = j % length.{u} (α := α) [] ∨ Eq.{u + 1} (α := List α) [] []
inr : ∀ (hn : l ≠ []), l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
rcases eq_or_ne l [] with rfl | hn

Premises used: eq_or_ne, rfl, List.nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
i j : ℕ
hl : Nodup.{u} (α := α) []
⊢ Eq.{u + 1} (α := List α) (rotate [] i) (rotate [] j) ↔
    i % length.{u} (α := α) [] = j % length.{u} (α := α) [] ∨ Eq.{u + 1} (α := List α) [] []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
inr : l.rotate i = l.rotate j ↔ i % l.length = j % l.length
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
simp only [hn, or_false]

Premises used: or_false
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length

Tactic:
⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩

Premises used: Iff.intro, List.Nodup.rotate_congr
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
inr : ∀ (h : i % l.length = j % l.length), l.rotate i = l.rotate j
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length

Tactic:
refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
inr : l.rotate (i % l.length) = l.rotate j
inr₁ : l.rotate (j % l.length) = l.rotate j
inr₂ inr₃ : l.rotate j = l.rotate j
⊢ l.rotate i = l.rotate j

Tactic:
rw [← rotate_mod, h, rotate_mod]

Premises used: List.rotate_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
rw : l.rotate n = l ↔ n % l.length = 0 % l.length ∨ l = []
rw₁ : ℕ
rw₂ : l.rotate n = l ↔ l.rotate n = l.rotate 0
rw₃ rw₄ : l.rotate n = l ↔ l.rotate n = l
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []

Tactic:
rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]

Premises used: List.Nodup.rotate_congr_iff, List.rotate_zero, Nat.zero_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ l.rotate 0 = l

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
obtain : ∀ (n : ℕ), l.rotate n ~r l
⊢ l' ~r l

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
nil : IsRotated.{u} (α := α) (rotate [] n) []
cons : ∀ (hd : α) (tl : List α), (hd :: tl).rotate n ~r hd :: tl
⊢ l.rotate n ~r l

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
nil nil₁ : Eq.{u + 1} (α := List α) (rotate (rotate [] n) 0) []
⊢ IsRotated.{u} (α := α) (rotate [] n) []

Tactic:
exists 0
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
h : ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl
⊢ (hd :: tl).rotate n ~r hd :: tl

Tactic:
use (hd :: tl).length * n - n

Premises used: List.cons, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
h : n ≤ (hd :: tl).length * n
⊢ ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl

Tactic:
rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]

Premises used: List.rotate_rotate, List.rotate_length_mul, Nat.add_sub_cancel'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < (hd :: tl).length

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n

Tactic:
exact Nat.le_mul_of_pos_left _ (by simp)

Premises used: Nat.le_mul_of_pos_left
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ~r l

Tactic:
⟨IsRotated.symm, IsRotated.symm⟩

Premises used: List.IsRotated.symm, Iff.intro
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~r l

Tactic:
IsRotated.symm ⟨n, rfl⟩

Premises used: List.IsRotated.symm, Exists.intro, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
rw rw₁ : l.rotate (n + m) = l.rotate (n + m)
⊢ l.rotate (n + m) = (l.rotate n).rotate m

Tactic:
rw [rotate_rotate]

Premises used: List.rotate_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
⊢ Equivalence.{u + 1} (α := List α) IsRotated

Tactic:
Equivalence.mk IsRotated.refl IsRotated.symm IsRotated.trans

Premises used: List.IsRotated.refl, List.IsRotated.trans, List.IsRotated.symm, Equivalence.mk
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
⊢ l ~ l'

Tactic:
Exists.elim h fun _ hl => hl ▸ (rotate_perm _ _).symm

Premises used: List.rotate_perm, Eq.rec, List.Perm.symm, Exists.elim
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
⊢ l.Nodup ↔ l'.Nodup

Tactic:
h.perm.nodup_iff

Premises used: List.Perm.nodup_iff, List.IsRotated.perm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
a : α
⊢ a ∈ l ↔ a ∈ l'

Tactic:
h.perm.mem_iff

Premises used: List.IsRotated.perm, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
h : l ~r []
n : ℕ
hn : l.rotate n = []
⊢ l = []

Tactic:
simpa using hn
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
h : l = []
⊢ l ~r l

Tactic:
rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
rw : l ~r [] ↔ [] = l
rw₁ : l = [] ↔ [] = l
rw₂ rw₃ : [] = l ↔ [] = l
⊢ [] ~r l ↔ [] = l

Tactic:
rw [isRotated_comm, isRotated_nil_iff, eq_comm]

Premises used: List.isRotated_comm, eq_comm, List.isRotated_nil_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
x : α
h : l ~r [x]
n : ℕ
hn : l.rotate n = [x]
⊢ l = [x]

Tactic:
simpa using hn
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
x : α
h : l = [x]
⊢ l ~r l

Tactic:
rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
x : α
rw : l ~r [x] ↔ [x] = l
rw₁ : l = [x] ↔ [x] = l
rw₂ rw₃ : [x] = l ↔ [x] = l
⊢ [x] ~r l ↔ [x] = l

Tactic:
rw [isRotated_comm, isRotated_singleton_iff, eq_comm]

Premises used: List.isRotated_comm, eq_comm, List.isRotated_singleton_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hd : α
tl : List α
⊢ (hd :: tl).rotate 1 = tl ++ [hd]

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
obtain : ∀ (n : ℕ), l.reverse ~r (l.rotate n).reverse
⊢ l.reverse ~r l'.reverse

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.reverse ~r (l.rotate n).reverse

Tactic:
⟨_, (reverse_rotate _ _).symm⟩

Premises used: List.reverse_rotate, List.IsRotated, Exists.intro, Eq.symm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.reverse ~r (l.rotate n).reverse

Tactic:
exact ⟨_, (reverse_rotate _ _).symm⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
mp : l.reverse ~r l' → l ~r l'.reverse
mpr : l ~r l'.reverse → l.reverse ~r l'
⊢ l.reverse ~r l' ↔ l ~r l'.reverse

Tactic:
constructor
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l.reverse ~r l'
⊢ l ~r l'.reverse

Tactic:
simpa using h.reverse

Premises used: List.IsRotated.reverse
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'

Tactic:
simpa using h.reverse

Premises used: List.IsRotated.reverse
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ l.reverse ~r l'.reverse ↔ l ~r l'

Tactic:
simp [isRotated_reverse_comm_iff]

Premises used: List.isRotated_reverse_comm_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'

Tactic:
⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩

Premises used: List.IsRotated, Iff.intro, Exists.intro, _private.0.List.isRotated_iff_mod.match_1