awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : (f + -g).neLocus (g + -g) = (f - g).support
⊢ f.neLocus g = (f - g).support
have rw₁ : (f + -g).neLocus 0 = (f - g).support
Tactic: rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : (f + -g).neLocus (g + -g) = (f - g).support
rw₁ : (f + -g).neLocus 0 = (f - g).support
⊢ f.neLocus g = (f - g).support
have rw₂ : (f + -g).support = (f - g).support
Tactic: rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : (f + -g).neLocus (g + -g) = (f - g).support
rw₁ : (f + -g).neLocus 0 = (f - g).support
rw₂ : (f + -g).support = (f - g).support
⊢ f.neLocus g = (f - g).support
have rw₃ : (f + -g).support = (f + -g).support
Tactic: rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = g.support
have rw : f.neLocus (f + g) = neLocus 0 g
Tactic: rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + g) = neLocus 0 g
⊢ f.neLocus (f + g) = g.support
have rw₁ : f.neLocus (f + g) = (f + 0).neLocus (f + g)
Tactic: rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + g) = neLocus 0 g
rw₁ : f.neLocus (f + g) = (f + 0).neLocus (f + g)
⊢ f.neLocus (f + g) = g.support
have rw₂ : f.neLocus (f + g) = f.neLocus (f + g)
Tactic: rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ (f + g).neLocus f = g.support
have rw : f.neLocus (f + g) = g.support
Tactic: rw [neLocus_comm, neLocus_self_add_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + g) = g.support
⊢ (f + g).neLocus f = g.support
have rw₁ : g.support = g.support
Tactic: rw [neLocus_comm, neLocus_self_add_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f - g) = g.support
have rw : f.neLocus (f + -g) = g.support
Tactic: rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + -g) = g.support
⊢ f.neLocus (f - g) = g.support
have rw₁ : (-g).support = g.support
Tactic: rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + -g) = g.support
rw₁ : (-g).support = g.support
⊢ f.neLocus (f - g) = g.support
have rw₂ : g.support = g.support
Tactic: rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ (f - g).neLocus f = g.support
have rw : f.neLocus (f - g) = g.support
Tactic: rw [neLocus_comm, neLocus_self_sub_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f - g) = g.support
⊢ (f - g).neLocus f = g.support
have rw₁ : g.support = g.support
Tactic: rw [neLocus_comm, neLocus_self_sub_right]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
have rw : a.natAbs = b.natAbs ↔ a * a = b * b
Tactic: rw [sq, sq]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2
have rw : a.natAbs < b.natAbs ↔ a * a < b * b
Tactic: rw [sq, sq]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2
have rw : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
Tactic: rw [sq, sq]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a = b
have rw : a.natAbs = b.natAbs ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
Tactic: rw [← sq_eq_sq₀ ha hb, ← natAbs_eq_iff_sq_eq]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
rw : a.natAbs = b.natAbs ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
⊢ a.natAbs = b.natAbs ↔ a = b
have rw₁ : a.natAbs = b.natAbs ↔ a.natAbs = b.natAbs
Tactic: rw [← sq_eq_sq₀ ha hb, ← natAbs_eq_iff_sq_eq]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ (HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)).natAbs ≤ n
have rw : |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| ≤ (↑n : ℤ)
Tactic: rw [← Nat.cast_le (α := ℤ), natCast_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ (HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)).natAbs < n
have rw : |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| < (↑n : ℤ)
Tactic: rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
b : Bool
n : ℤ
⊢ (bit b n).div2 = n
have rw : HDiv.hDiv (α := ℤ) (bif b then 1 else 0) 2 = 0
Tactic: rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
b : Bool
n : ℤ
rw : HDiv.hDiv (α := ℤ) (bif b then 1 else 0) 2 = 0
⊢ (bit b n).div2 = n
have H : Ne (α := ℤ) 2 0
Tactic: rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
b : Bool
n : ℤ
⊢ HDiv.hDiv (α := ℤ) (bif b then 1 else 0) 2 = 0
have false : HDiv.hDiv (α := ℤ) (bif false then 1 else 0) 2 = 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
b : Bool
n : ℤ
false : HDiv.hDiv (α := ℤ) (bif Bool.false then 1 else 0) 2 = 0
⊢ HDiv.hDiv (α := ℤ) (bif b then 1 else 0) 2 = 0
have true : HDiv.hDiv (α := ℤ) (bif true then 1 else 0) 2 = 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
n : ℤ
true : ofNat 0 = 0
⊢ ofNat (1 / 2) = 0
have true₁ : 1 < 2
Tactic: rw [Nat.div_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|
have mp : a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
mp : a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|
have mpr : r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r
have mpr : (r + b * q) / b = q
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
mpr : (r + b * q) / b = q
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r
have mpr₁ : (r + b * q) % b = r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q
have mpr : 0 + q = q
Tactic: rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r
have mpr : r % b = r
Tactic: rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
mpr : r % b = r
⊢ (r + b * q) % b = r
have mpr₁ : r % |b| = r
Tactic: rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]
-- Lean 4 proof step from Mathlib.Data.Int.Lemmas (goal)
Goal:
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
mpr : r % b = r
mpr₁ : r % |b| = r
⊢ (r + b * q) % b = r
have mpr₂ : r = r
Tactic: rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
l : List α
⊢ foldl (flip cons) [] l = l.reverse
have nil : Eq.{u_1 + 1} (α := List α) (foldl (flip cons) [] []) (reverse [])
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
l : List α
nil : Eq.{u_1 + 1} (α := List α) (foldl (flip cons) [] []) (reverse [])
⊢ foldl (flip cons) [] l = l.reverse
have cons : ∀ (head : α) (tail : List α),
  foldl (flip cons) [] tail = tail.reverse → foldl (flip cons) [] (head :: tail) = (head :: tail).reverse
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v b (a :: l) = v (foldl v b l) a
have rw : foldl v (v b a) l = v (foldl v b l) a
Tactic: rw [foldl_cons]
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v (v b a) l = v (foldl v b l) a
have nil : ∀ {a : α} {b : β}, foldl v (v b a) [] = v (foldl v b []) a
Tactic: induction l generalizing a b
Cleared hypotheses: l, a, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
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
⊢ foldl v (v b a) l = v (foldl v b l) a
have 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
Tactic: induction l generalizing a b
Cleared hypotheses: l, a, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ foldr f b (a :: l) = foldr f (f a b) l
have rw : f a (foldr f b l) = foldr f (f a b) l
Tactic: rw [foldr_cons]
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ f a (foldr f b l) = foldr f (f a b) l
have nil : ∀ {a : α} {b : β}, f a (foldr f b []) = foldr f (f a b) []
Tactic: induction l generalizing a b
Cleared hypotheses: l, a, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
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) []
⊢ f a (foldr f b l) = foldr f (f a b) l
have 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)
Tactic: induction l generalizing a b
Cleared hypotheses: l, a, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
a b : α
⊢ f (foldl f a l) b = f a (foldr f b l)
have nil : ∀ {a : α}, f (foldl f a []) b = f a (foldr f b [])
Tactic: induction l generalizing a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
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 [])
⊢ f (foldl f a l) b = f a (foldr f b l)
have 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))
Tactic: induction l generalizing a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
l : List α
a : α
f : α → α → α
inst : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a l = foldr f a l
have nil : foldl f a [] = foldr f a []
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
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 []
⊢ foldl f a l = foldr f a l
have cons : ∀ (head : α) (tail : List α), foldl f a tail = foldr f a tail → foldl f a (head :: tail) = foldr f a (head :: tail)
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
inst : LeftCommutative f
⊢ foldl (flip f) b l = foldr f b l
have nil : ∀ {b : β}, foldl (flip f) b [] = foldr f b []
Tactic: induction l generalizing b
Cleared hypotheses: l, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
inst : LeftCommutative f
nil : ∀ {b : β}, foldl (flip f) b [] = foldr f b []
⊢ foldl (flip f) b l = foldr f b l
have 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)
Tactic: induction l generalizing b
Cleared hypotheses: l, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst : RightCommutative v
⊢ foldr (flip v) b l = foldl v b l
have nil : ∀ {b : β}, foldr (flip v) b [] = foldl v b []
Tactic: induction l generalizing b
Cleared hypotheses: l, b
-- Lean 4 proof step from Mathlib.Data.List.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst : RightCommutative v
nil : ∀ {b : β}, foldr (flip v) b [] = foldl v b []
⊢ foldr (flip v) b l = foldl v b l
have 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)
Tactic: induction l generalizing b
Cleared hypotheses: l, b
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
⊢ l.rotate' 0 = l
have nil : Eq.{u + 1} (α := List α) (rotate' [] 0) []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List α) (rotate' [] 0) []
⊢ l.rotate' 0 = l
have cons : ∀ (head : α) (tail : List α), (head :: tail).rotate' 0 = head :: tail
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
l : List α
n : ℕ
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length
have rw : (l ++ [a]).length = (a :: l).length
Tactic: rw [List.rotate', length_rotate' (l ++ [a]) n]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
have hnl : n ≤ l.length
Tactic: have hnl : n ≤ l.length := le_of_succ_le_succ h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ (l ++ [a]).length
have rw : n ≤ l.length + HAdd.hAdd (α := ℕ) 0 1
Tactic: rw [length_append, length_cons, List.length]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
have hnl' : 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
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
have rw : drop n l ++ [a] ++ take n l = drop n l ++ a :: take n 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]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
l : List α
n m : ℕ
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)
have rw : ((l ++ [a]).rotate' n).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]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
l : List α
n m : ℕ
rw : ((l ++ [a]).rotate' n).rotate' m = (a :: l).rotate' (n + 1 + m)
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)
have rw₁ : (l ++ [a]).rotate' (n + 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]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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)
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)
have rw₂ : (l ++ [a]).rotate' (n + m) = (a :: l).rotate' (n + m + 1)
Tactic: rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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)
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)
have rw₃ : (a :: l).rotate' (n + m).succ = (a :: l).rotate' (n + m + 1)
Tactic: rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
⊢ l.rotate' l.length = l
have rw : drop l.length l ++ take l.length l = l
Tactic: rw [rotate'_eq_drop_append_take le_rfl]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length = l
have rw : l.rotate' (l.length * n) = l
Tactic: rw [rotate'_length, rotate'_length_mul l n]
-- 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)).rotate' (l.rotate' (l.length * n)).length = l
have rw₁ : l = l
Tactic: rw [rotate'_length, rotate'_length_mul l n]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (n % l.length) = (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length))
have rw : l.rotate' (n % l.length) = l.rotate' (n % l.length)
Tactic: rw [rotate'_length_mul]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
have rw : l.rotate' (n % l.length + (l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
Tactic: rw [rotate'_rotate', length_rotate', Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate' (n % l.length + (l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
have rw₁ : l.rotate' (n % l.length + l.length * (n / l.length)) = l.rotate' n
Tactic: rw [rotate'_rotate', length_rotate', Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
have rw₂ : l.rotate' n = l.rotate' n
Tactic: rw [rotate'_rotate', length_rotate', Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' n
have rw : l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
Tactic: rw [← rotate'_mod,
        rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n
have rw : (a :: l).rotate' (n + 1) = (l ++ [a]).rotate n
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
a : α
n : ℕ
rw : (a :: l).rotate' (n + 1) = (l ++ [a]).rotate n
⊢ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n
have rw₁ : (a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n
have rw₂ : (l ++ [a]).rotate' n = (l ++ [a]).rotate' n
Tactic: rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).length = l.length
have rw : (l.rotate' n).length = l.length
Tactic: rw [rotate_eq_rotate', length_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
rw : (l.rotate' n).length = l.length
⊢ (l.rotate n).length = l.length
have rw₁ : l.length = l.length
Tactic: rw [rotate_eq_rotate', length_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
n k : ℕ
⊢ ((replicate n a).rotate k).length = n
have rw : (replicate n a).length = n
Tactic: rw [length_rotate, length_replicate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : α
n k : ℕ
rw : (replicate n a).length = n
⊢ ((replicate n a).rotate k).length = n
have rw₁ : n = n
Tactic: rw [length_rotate, length_replicate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l
have rw : n ≤ l.length → l.rotate' n = drop n l ++ take n l
Tactic: rw [rotate_eq_rotate']
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
have inl : ∀ (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