awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| ≤ (↑n : ℤ)

Tactic:
exact abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n)
    (natCast_nonneg b) (ofNat_le.mpr b_le_n)

Premises used: Iff.mpr, Int.ofNat_le, abs_sub_le_of_nonneg_of_le, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
rw : |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| < (↑n : ℤ)
⊢ (HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)).natAbs < n

Tactic:
rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]

Premises used: Nat.cast_lt, Int.natCast_natAbs
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| < (↑n : ℤ)

Tactic:
abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n)
    (natCast_nonneg b) (ofNat_lt.mpr b_lt_n)

Premises used: Iff.mpr, abs_sub_lt_of_nonneg_of_lt, Int.ofNat_lt, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| < (↑n : ℤ)

Tactic:
exact abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n)
    (natCast_nonneg b) (ofNat_lt.mpr b_lt_n)

Premises used: Iff.mpr, abs_sub_lt_of_nonneg_of_lt, Int.ofNat_lt, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
⊢ StrictMonoOn natAbs (Ici 0)

Tactic:
fun _ ha _ _ hab =>
  natAbs_lt_natAbs_of_nonneg_of_lt ha hab

Premises used: Int.natAbs_lt_natAbs_of_nonneg_of_lt, StrictMonoOn
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a : ℤ
h : Membership.mem (γ := Set ℤ) (Iic 0) a
b : ℤ
hb : Membership.mem (γ := Set ℤ) (Iic 0) b
hab : a < b
⊢ b.natAbs < a.natAbs

Tactic:
simpa [Int.natAbs_neg] using
    natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)

Premises used: Iff.mpr, neg_lt_neg_iff, Int.natAbs_lt_natAbs_of_nonneg_of_lt, Right.nonneg_neg_iff, Int.natAbs_neg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
⊢ InjOn natAbs (Ici 0)

Tactic:
strictMonoOn_natAbs.injOn

Premises used: StrictMonoOn.injOn, Int.strictMonoOn_natAbs
-- Module: Mathlib.Data.Int.Lemmas
Goal:
⊢ InjOn natAbs (Iic 0)

Tactic:
strictAntiOn_natAbs.injOn

Premises used: Int.strictAntiOn_natAbs, StrictAntiOn.injOn
-- Module: Mathlib.Data.Int.Lemmas
Goal:
b : Bool
n : ℤ
rw : HDiv.hDiv (α := ℤ) (bif b then 1 else 0) 2 = 0
H : Ne (α := ℤ) 2 0
⊢ (bit b n).div2 = n

Tactic:
rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]

Premises used: zero_add, Int.add_mul_ediv_left, add_comm, Int.div2_val, Int.bit_val
-- Module: Mathlib.Data.Int.Lemmas
Goal:
b : Bool
n : ℤ
false : HDiv.hDiv (α := ℤ) (bif Bool.false then 1 else 0) 2 = 0
true : HDiv.hDiv (α := ℤ) (bif Bool.true then 1 else 0) 2 = 0
⊢ HDiv.hDiv (α := ℤ) (bif b then 1 else 0) 2 = 0

Tactic:
cases b
-- Module: Mathlib.Data.Int.Lemmas
Goal:
n : ℤ
⊢ HDiv.hDiv (α := ℤ) (bif false then 1 else 0) 2 = 0

Tactic:
decide
-- Module: Mathlib.Data.Int.Lemmas
Goal:
n : ℤ
true : ofNat 0 = 0
true₁ : 1 < 2
⊢ ofNat (1 / 2) = 0

Tactic:
rw [Nat.div_eq_of_lt]

Premises used: Nat.div_eq_of_lt
-- Module: Mathlib.Data.Int.Lemmas
Goal:
n : ℤ
⊢ ofNat 0 = 0

Tactic:
simp
-- Module: Mathlib.Data.Int.Lemmas
Goal:
n : ℤ
⊢ 1 < 2

Tactic:
simp
-- Module: Mathlib.Data.Int.Lemmas
Goal:
b : Bool
n : ℤ
⊢ Ne (α := ℤ) 2 0

Tactic:
decide
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
mp : a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|
mpr : r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
constructor
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < |b|

Tactic:
⟨emod_add_mul_ediv a b, emod_nonneg _ h, emod_lt_abs _ h⟩

Premises used: Int.emod_lt_abs, Int.emod_add_mul_ediv, And.intro, Int.emod_nonneg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < |b|

Tactic:
exact ⟨emod_add_mul_ediv a b, emod_nonneg _ h, emod_lt_abs _ h⟩
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
mpr : (r + b * q) / b = q
mpr₁ : (r + b * q) % b = r
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r

Tactic:
constructor
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
mpr : 0 + q = q
⊢ (r + b * q) / b = q

Tactic:
rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]

Premises used: Int.ediv_eq_zero_of_lt_abs, Int.add_mul_ediv_left
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q

Tactic:
simp
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
mpr : r % b = r
mpr₁ : r % |b| = r
mpr₂ mpr₃ : r = r
⊢ (r + b * q) % b = r

Tactic:
rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]

Premises used: Int.emod_eq_of_lt, Int.add_mul_emod_self_left, Int.emod_abs
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
nil : Eq.{u_1 + 1} (α := List α) (foldl (flip List.cons) [] []) (reverse [])
cons :
  ∀ (head : α) (tail : List α),
    foldl (flip List.cons) [] tail = tail.reverse → foldl (flip List.cons) [] (head :: tail) = (head :: tail).reverse
⊢ foldl (flip List.cons) [] l = l.reverse

Tactic:
induction l
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
⊢ Eq.{u_1 + 1} (α := List α) (foldl (flip cons) [] []) (reverse [])

Tactic:
simp [flip, foldl_eq_foldr_reverse, -foldr_reverse]

Premises used: List.foldr_reverse, flip, List.foldl_eq_foldr_reverse
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
head : α
tail : List α
tail_ih : foldl (flip cons) [] tail = tail.reverse
⊢ foldl (flip cons) [] (head :: tail) = (head :: tail).reverse

Tactic:
simp [flip, foldl_eq_foldr_reverse, -foldr_reverse]

Premises used: List.foldr_reverse, flip, List.foldl_eq_foldr_reverse
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
rw : foldl v (v b a) l = v (foldl v b l) a
⊢ foldl v b (a :: l) = v (foldl v b l) a

Tactic:
rw [foldl_cons]

Premises used: List.foldl_cons
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
nil : ∀ {a : α} {b : β}, foldl v (v b a) [] = v (foldl v b []) a
cons :
  ∀ (head : α) (tail : List α),
    (∀ {a : α} {b : β}, foldl v (v b a) tail = v (foldl v b tail) a) →
      ∀ {a : α} {b : β}, foldl v (v b a) (head :: tail) = v (foldl v b (head :: tail)) a
⊢ foldl v (v b a) l = v (foldl v b l) a

Tactic:
induction l generalizing a b
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
a : α
b : β
⊢ foldl v (v b a) [] = v (foldl v b []) a

Tactic:
simp [*, hv.right_comm]

Premises used: RightCommutative.right_comm
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
head : α
tail : List α
tail_ih : ∀ {a : α} {b : β}, foldl v (v b a) tail = v (foldl v b tail) a
a : α
b : β
⊢ foldl v (v b a) (head :: tail) = v (foldl v b (head :: tail)) a

Tactic:
simp [*, hv.right_comm]

Premises used: RightCommutative.right_comm
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
rw : f a (foldr f b l) = foldr f (f a b) l
⊢ foldr f b (a :: l) = foldr f (f a b) l

Tactic:
rw [foldr_cons]

Premises used: List.foldr_cons
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
nil : ∀ {a : α} {b : β}, f a (foldr f b []) = foldr f (f a b) []
cons :
  ∀ (head : α) (tail : List α),
    (∀ {a : α} {b : β}, f a (foldr f b tail) = foldr f (f a b) tail) →
      ∀ {a : α} {b : β}, f a (foldr f b (head :: tail)) = foldr f (f a b) (head :: tail)
⊢ f a (foldr f b l) = foldr f (f a b) l

Tactic:
induction l generalizing a b
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
a : α
b : β
⊢ f a (foldr f b []) = foldr f (f a b) []

Tactic:
simp [*, hf.left_comm]

Premises used: LeftCommutative.left_comm
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
head : α
tail : List α
tail_ih : ∀ {a : α} {b : β}, f a (foldr f b tail) = foldr f (f a b) tail
a : α
b : β
⊢ f a (foldr f b (head :: tail)) = foldr f (f a b) (head :: tail)

Tactic:
simp [*, hf.left_comm]

Premises used: LeftCommutative.left_comm
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
a b : α
nil : ∀ {a : α}, f (foldl f a []) b = f a (foldr f b [])
cons :
  ∀ (head : α) (tail : List α),
    (∀ {a : α}, f (foldl f a tail) b = f a (foldr f b tail)) →
      ∀ {a : α}, f (foldl f a (head :: tail)) b = f a (foldr f b (head :: tail))
⊢ f (foldl f a l) b = f a (foldr f b l)

Tactic:
induction l generalizing a
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b a : α
⊢ f (foldl f a []) b = f a (foldr f b [])

Tactic:
simp [*, ha.assoc]

Premises used: Std.Associative.assoc
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b head : α
tail : List α
tail_ih : ∀ {a : α}, f (foldl f a tail) b = f a (foldr f b tail)
a : α
⊢ f (foldl f a (head :: tail)) b = f a (foldr f b (head :: tail))

Tactic:
simp [*, ha.assoc]

Premises used: Std.Associative.assoc
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
a : α
f : α → α → α
inst : Std.Associative f
ha : ∀ (x : α), f a x = f x a
nil : foldl f a [] = foldr f a []
cons :
  ∀ (head : α) (tail : List α), foldl f a tail = foldr f a tail → foldl f a (head :: tail) = foldr f a (head :: tail)
⊢ foldl f a l = foldr f a l

Tactic:
induction l
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
a : α
f : α → α → α
inst : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a [] = foldr f a []

Tactic:
simp [*, foldl_assoc]

Premises used: List.foldl_assoc
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
a : α
f : α → α → α
inst : Std.Associative f
ha : ∀ (x : α), f a x = f x a
head : α
tail : List α
tail_ih : foldl f a tail = foldr f a tail
⊢ foldl f a (head :: tail) = foldr f a (head :: tail)

Tactic:
simp [*, foldl_assoc]

Premises used: List.foldl_assoc
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
l : List α
a : α
f : α → α → α
hf : Std.Commutative f
inst : Std.Associative f
⊢ foldl f a l = foldr f a l

Tactic:
foldl_eq_foldr_of_commute (hf.comm a)

Premises used: List.foldl_eq_foldr_of_commute, Std.Commutative.comm
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
inst : LeftCommutative f
nil : ∀ {b : β}, foldl (flip f) b [] = foldr f b []
cons :
  ∀ (head : α) (tail : List α),
    (∀ {b : β}, foldl (flip f) b tail = foldr f b tail) →
      ∀ {b : β}, foldl (flip f) b (head :: tail) = foldr f b (head :: tail)
⊢ foldl (flip f) b l = foldr f b l

Tactic:
induction l generalizing b
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
inst : LeftCommutative f
b : β
⊢ foldl (flip f) b [] = foldr f b []

Tactic:
simp [*, flip, foldr_cons_eq_foldr_apply, -foldr_cons]

Premises used: List.foldr_cons, flip, List.foldr_cons_eq_foldr_apply
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
inst : LeftCommutative f
head : α
tail : List α
tail_ih : ∀ {b : β}, foldl (flip f) b tail = foldr f b tail
b : β
⊢ foldl (flip f) b (head :: tail) = foldr f b (head :: tail)

Tactic:
simp [*, flip, foldr_cons_eq_foldr_apply, -foldr_cons]

Premises used: List.foldr_cons, flip, List.foldr_cons_eq_foldr_apply
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst : RightCommutative v
nil : ∀ {b : β}, foldr (flip v) b [] = foldl v b []
cons :
  ∀ (head : α) (tail : List α),
    (∀ {b : β}, foldr (flip v) b tail = foldl v b tail) →
      ∀ {b : β}, foldr (flip v) b (head :: tail) = foldl v b (head :: tail)
⊢ foldr (flip v) b l = foldl v b l

Tactic:
induction l generalizing b
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
v : β → α → β
inst : RightCommutative v
b : β
⊢ foldr (flip v) b [] = foldl v b []

Tactic:
simp [*, flip, foldl_cons_eq_apply_foldl, -foldl_cons]

Premises used: List.foldl_cons_eq_apply_foldl, flip, List.foldl_cons
-- Module: Mathlib.Data.List.Fold
Goal:
α : Type u_1
β : Type u_2
v : β → α → β
inst : RightCommutative v
head : α
tail : List α
tail_ih : ∀ {b : β}, foldr (flip v) b tail = foldl v b tail
b : β
⊢ foldr (flip v) b (head :: tail) = foldl v b (head :: tail)

Tactic:
simp [*, flip, foldl_cons_eq_apply_foldl, -foldl_cons]

Premises used: List.foldl_cons_eq_apply_foldl, flip, List.foldl_cons
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate (n % l.length) = l.rotate n

Tactic:
simp [rotate]

Premises used: List.rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := List α) (rotate [] n) []

Tactic:
simp [rotate]

Premises used: List.rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ l.rotate 0 = l

Tactic:
simp [rotate]

Premises used: List.rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := List α) (rotate' [] n) []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List α) (rotate' [] 0) []
cons : ∀ (head : α) (tail : List α), (head :: tail).rotate' 0 = head :: tail
⊢ l.rotate' 0 = l

Tactic:
cases l
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α) (rotate' [] 0) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
head : α
tail : List α
⊢ (head :: tail).rotate' 0 = head :: tail

Tactic:
rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' n.succ = (l ++ [a]).rotate' n

Tactic:
simp [rotate']

Premises used: List.rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
x : ℕ
⊢ length.{u} (α := α) (rotate' [] x) = length.{u} (α := α) []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
rw : (l ++ [a]).length = (a :: l).length
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length

Tactic:
rw [List.rotate', length_rotate' (l ++ [a]) n]

Premises used: List.cons, List.rotate', HAppend.hAppend, List.nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
h : n ≤ length.{u} (α := α) []
⊢ rotate' [] n = HAppend.hAppend (α := List α) (drop n []) (take n [])

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
h : 0 ≤ l.length
⊢ l.rotate' 0 = drop 0 l ++ take 0 l

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
⊢ n ≤ l.length

Tactic:
have hnl : n ≤ l.length := le_of_succ_le_succ h
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
rw : n ≤ l.length + HAdd.hAdd (α := ℕ) 0 1
⊢ n ≤ (l ++ [a]).length

Tactic:
rw [length_append, length_cons, List.length]

Premises used: List.length_cons, List.length_append, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + HAdd.hAdd (α := ℕ) 0 1

Tactic:
le_of_succ_le h

Premises used: Nat.le_of_succ_le
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + HAdd.hAdd (α := ℕ) 0 1

Tactic:
exact le_of_succ_le h

Premises used: Nat.le_of_succ_le
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ (l ++ [a]).length

Tactic:
have hnl' : n ≤ (l ++ [a]).length := by
      rw [length_append, length_cons, List.length]; exact le_of_succ_le h
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
rw : drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take,
        drop_append_of_le_length hnl, take_append_of_le_length hnl]

Premises used: List.rotate'_cons_succ, List.take_append_of_le_length, List.drop_append_of_le_length, List.drop, List.take
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l

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

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n m : ℕ
⊢ Eq.{u + 1} (α := List α) (rotate' (rotate' [] n) m) (rotate' [] (n + m))

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
n m : ℕ
rw : ((l ++ [a]).rotate' n).rotate' m = (a :: l).rotate' (n + 1 + m)
rw₁ : (l ++ [a]).rotate' (n + m) = (a :: l).rotate' (n + 1 + m)
rw₂ : (l ++ [a]).rotate' (n + m) = (a :: l).rotate' (n + m + 1)
rw₃ : (a :: l).rotate' (n + m).succ = (a :: l).rotate' (n + m + 1)
rw₄ rw₅ : (a :: l).rotate' (n + m + 1) = (a :: l).rotate' (n + m + 1)
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)

Tactic:
rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]

Premises used: List.rotate'_cons_succ, Nat.succ_eq_add_one, Nat.add_right_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
rw : drop l.length l ++ take l.length l = l
⊢ l.rotate' l.length = l

Tactic:
rw [rotate'_eq_drop_append_take le_rfl]

Premises used: le_rfl, List.rotate'_eq_drop_append_take
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ drop l.length l ++ take l.length l = l

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

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

Tactic:
simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']

Premises used: Nat.mul_succ, List.rotate'_rotate', List.rotate'_length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate' (l.length * n) = l
rw₁ rw₂ : l = l
⊢ (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length = l

Tactic:
rw [rotate'_length, rotate'_length_mul l n]

Premises used: List.rotate'_length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw rw₁ : l.rotate' (n % l.length) = l.rotate' (n % l.length)
⊢ l.rotate' (n % l.length) = (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length))

Tactic:
rw [rotate'_length_mul]

Premises used: List.rotate'_length_mul
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate' (n % l.length + (l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
rw₁ : l.rotate' (n % l.length + l.length * (n / l.length)) = l.rotate' n
rw₂ rw₃ : l.rotate' n = l.rotate' n
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n

Tactic:
rw [rotate'_rotate', length_rotate', Nat.mod_add_div]

Premises used: List.length_rotate', List.rotate'_rotate', Nat.mod_add_div
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
h : l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
simp_all [length_eq_zero_iff]

Premises used: List.length_eq_zero_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
rw : l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
⊢ l.rotate n = l.rotate' n

Tactic:
rw [← rotate'_mod,
        rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]

Premises used: List.rotate'_mod, le_of_lt, List.rotate'_eq_drop_append_take, Nat.mod_lt, Nat.pos_of_ne_zero
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
simp [rotate]

Premises used: List.rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
a : α
n : ℕ
rw : (a :: l).rotate' (n + 1) = (l ++ [a]).rotate n
rw₁ : (a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n
rw₂ rw₃ : (l ++ [a]).rotate' n = (l ++ [a]).rotate' n
⊢ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n

Tactic:
rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]

Premises used: List.rotate'_cons_succ, List.rotate_eq_rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
x : α
n : ℕ
⊢ Membership.mem (γ := List α) (rotate [] n) x ↔ Membership.mem (γ := List α) [] x

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
x : α
⊢ x ∈ (a :: l).rotate 0 ↔ x ∈ a :: l

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
x : α
n : ℕ
⊢ x ∈ (a :: l).rotate (n + 1) ↔ x ∈ a :: l

Tactic:
simp [rotate_cons_succ, mem_rotate, or_comm]

Premises used: List.rotate_cons_succ, or_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : (l.rotate' n).length = l.length
rw₁ rw₂ : l.length = l.length
⊢ (l.rotate n).length = l.length

Tactic:
rw [rotate_eq_rotate', length_rotate']

Premises used: List.rotate_eq_rotate', List.length_rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
n k : ℕ
rw : (replicate n a).length = n
rw₁ rw₂ : n = n
⊢ ((replicate n a).rotate k).length = n

Tactic:
rw [length_rotate, length_replicate]

Premises used: List.length_rotate, List.length_replicate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : n ≤ l.length → l.rotate' n = drop n l ++ take n l
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
rw [rotate_eq_rotate']

Premises used: List.rotate_eq_rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l

Tactic:
rotate'_eq_drop_append_take

Premises used: List.rotate'_eq_drop_append_take
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l

Tactic:
exact rotate'_eq_drop_append_take

Premises used: List.rotate'_eq_drop_append_take
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
inl : ∀ (hl : 0 = l.length), l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
inr : ∀ (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

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 : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
simp [eq_nil_of_length_eq_zero hl.symm]

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

Tactic:
rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

Premises used: List.rotate_mod, LT.lt.le, Nat.mod_lt, List.rotate_eq_drop_append_take
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
rw : (l ++ l').rotate' l.length = l' ++ l
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
rw [rotate_eq_rotate']

Premises used: List.rotate_eq_rotate'