awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.odd.get n = s.get (2 * n + 1)
have rw : s.tail.get (2 * n) = s.get (2 * n + 1)
Tactic: rw [odd_eq, get_even]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s : Stream' α
h_1 : a ∈ s.even
n : ℕ
h : (fun (b : α) ↦ a = b) (s.even.get n)
⊢ (fun (b : α) ↦ a = b) (s.get (2 * n))
have rw : (fun (b : α) ↦ s.even.get n = b) (s.get (2 * n))
Tactic: rw [h, get_even]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s : Stream' α
h_1 : a ∈ s.even
n : ℕ
h : (fun (b : α) ↦ a = b) (s.even.get n)
rw : s.even.get n = s.get (2 * n)
⊢ a = s.get (2 * n)
have rw₁ : (fun (b : α) ↦ s.get (2 * n) = b) (s.get (2 * n))
Tactic: rw [h, get_even]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s : Stream' α
h_1 : a ∈ s.odd
n : ℕ
h : (fun (b : α) ↦ a = b) (s.odd.get n)
⊢ (fun (b : α) ↦ a = b) (s.get (2 * n + 1))
have rw : (fun (b : α) ↦ s.odd.get n = b) (s.get (2 * n + 1))
Tactic: rw [h, get_odd]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s : Stream' α
h_1 : a ∈ s.odd
n : ℕ
h : (fun (b : α) ↦ a = b) (s.odd.get n)
rw : s.odd.get n = s.get (2 * n + 1)
⊢ a = s.get (2 * n + 1)
have rw₁ : (fun (b : α) ↦ s.get (2 * n + 1) = b) (s.get (2 * n + 1))
Tactic: rw [h, get_odd]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
have rw : a :: (l₁ ++ l₂) ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
Tactic: rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
rw : a :: (l₁ ++ l₂) ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
have rw₁ : a :: (l₁ ++ l₂ ++ₛ s) = a :: l₁ ++ₛ (l₂ ++ₛ s)
Tactic: rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
rw : a :: (l₁ ++ l₂) ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
rw₁ : a :: (l₁ ++ l₂ ++ₛ s) = a :: l₁ ++ₛ (l₂ ++ₛ s)
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
have rw₂ : a :: (l₁ ++ l₂ ++ₛ s) = a :: (l₁ ++ₛ (l₂ ++ₛ s))
Tactic: rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
rw : a :: (l₁ ++ l₂) ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
rw₁ : a :: (l₁ ++ l₂ ++ₛ s) = a :: l₁ ++ₛ (l₂ ++ₛ s)
rw₂ : a :: (l₁ ++ l₂ ++ₛ s) = a :: (l₁ ++ₛ (l₂ ++ₛ s))
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
have rw₃ : a :: (l₁ ++ₛ (l₂ ++ₛ s)) = a :: (l₁ ++ₛ (l₂ ++ₛ s))
Tactic: rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x n h
n : ℕ
h : n < (b :: x).length
⊢ (b :: x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) n h
have cons : ∀ (h : 0 < (b :: x).length),
  (b :: x ++ₛ a).get 0 = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) 0 h
Tactic: rcases n with (_ | n)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x n h
n : ℕ
h : n < (b :: x).length
cons :
  ∀ (h : 0 < (b :: x).length),
    (b :: x ++ₛ a).get 0 = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) 0 h
⊢ (b :: x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) n h
have cons₁ : ∀ (n : ℕ) (h : n + 1 < (b :: x).length),
  (b :: x ++ₛ a).get (n + 1) = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) (n + 1) h
Tactic: rcases n with (_ | n)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n < x.length
⊢ (x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x n h
have nil : ∀ (n : ℕ) (h : n < List.length.{u} (α := α) []),
  ([] ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n h
Tactic: induction x generalizing n with
  | nil => simp at h
  | cons b x ih =>
    rcases n with (_ | n)
    · simp
    · simp [ih n (by simpa using h), cons_append_stream]
Cleared hypotheses: n, x, h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n < x.length
nil :
  ∀ (n : ℕ) (h : n < List.length.{u} (α := α) []),
    ([] ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n h
⊢ (x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x n h
have cons : ∀ (b : α) (x : List α)
  (ih :
    ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x n h)
  (n : ℕ) (h : n < (b :: x).length),
  (b :: x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) n h
Tactic: induction x generalizing n with
  | nil => simp at h
  | cons b x ih =>
    rcases n with (_ | n)
    · simp
    · simp [ih n (by simpa using h), cons_append_stream]
Cleared hypotheses: n, x, h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ (x ++ₛ a).get (x.length + n) = a.get n
have nil : ([] ++ₛ a).get (List.length.{u} (α := α) [] + n) = a.get n
Tactic: induction x
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
nil : ([] ++ₛ a).get (List.length.{u} (α := α) [] + n) = a.get n
⊢ (x ++ₛ a).get (x.length + n) = a.get n
have cons : ∀ (head : α) (tail : List α),
  (tail ++ₛ a).get (tail.length + n) = a.get n → (head :: tail ++ₛ a).get ((head :: tail).length + n) = a.get n
Tactic: induction x
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
⊢ a = b
have a₁ : ∀ (n : ℕ), a.get n = b.get n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (hypothesis)
Goal:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n
have h₁ : Eq.{u + 1} (α := α) ((fun (a : Stream' α) ↦ a.get (x.length + n)) (x ++ₛ a))
  ((fun (a : Stream' α) ↦ a.get (x.length + n)) (x ++ₛ b))
Tactic: replace h := congr_arg (fun a ↦ a.get (x.length + n)) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ x = y
have apply : ∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
Tactic: apply List.ext_getElem hl
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
i : ℕ
h₁ : i < x.length
h₂ : i < y.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
have rw : (x ++ₛ a).get i = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
Tactic: rw [← get_append_left, ← get_append_left, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
i : ℕ
h₁ : i < x.length
h₂ : i < y.length
rw : (x ++ₛ a).get i = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
a₁ : Stream' α
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
have rw₁ : (x ++ₛ a).get i = (y ++ₛ b).get i
Tactic: rw [← get_append_left, ← get_append_left, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
i : ℕ
h₁ : i < x.length
h₂ : i < y.length
rw : (x ++ₛ a).get i = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
a₁ : Stream' α
rw₁ : (x ++ₛ a).get i = (y ++ₛ b).get i
a₂ a₃ : Stream' α
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y i h₂
have rw₂ : (y ++ₛ b).get i = (y ++ₛ b).get i
Tactic: rw [← get_append_left, ← get_append_left, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
have rw : map f (a :: (l ++ₛ s)) = List.map f (a :: l) ++ₛ map f s
Tactic: rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
rw : map f (a :: (l ++ₛ s)) = List.map f (a :: l) ++ₛ map f s
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
have rw₁ : map f (a :: (l ++ₛ s)) = f a :: List.map f l ++ₛ map f s
Tactic: rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
rw : map f (a :: (l ++ₛ s)) = List.map f (a :: l) ++ₛ map f s
rw₁ : map f (a :: (l ++ₛ s)) = f a :: List.map f l ++ₛ map f s
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
have rw₂ : f a :: map f (l ++ₛ s) = f a :: List.map f l ++ₛ map f s
Tactic: rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
rw : map f (a :: (l ++ₛ s)) = List.map f (a :: l) ++ₛ map f s
rw₁ : map f (a :: (l ++ₛ s)) = f a :: List.map f l ++ₛ map f s
rw₂ : f a :: map f (l ++ₛ s) = f a :: List.map f l ++ₛ map f s
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
have rw₃ : f a :: map f (l ++ₛ s) = f a :: (List.map f l ++ₛ map f s)
Tactic: rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
rw : map f (a :: (l ++ₛ s)) = List.map f (a :: l) ++ₛ map f s
rw₁ : map f (a :: (l ++ₛ s)) = f a :: List.map f l ++ₛ map f s
rw₂ : f a :: map f (l ++ₛ s) = f a :: List.map f l ++ₛ map f s
rw₃ : f a :: map f (l ++ₛ s) = f a :: (List.map f l ++ₛ map f s)
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
have rw₄ : f a :: (List.map f l ++ₛ map f s) = f a :: (List.map f l ++ₛ map f s)
Tactic: rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
s : Stream' α
⊢ drop (a :: l).length (a :: l ++ₛ s) = s
have rw : drop (l.length + 1) (a :: l ++ₛ s) = s
Tactic: rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
s : Stream' α
rw : drop (l.length + 1) (a :: l ++ₛ s) = s
⊢ drop (a :: l).length (a :: l ++ₛ s) = s
have rw₁ : drop l.length (a :: l ++ₛ s).tail = s
Tactic: rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
s : Stream' α
rw : drop (l.length + 1) (a :: l ++ₛ s) = s
rw₁ : drop l.length (a :: l ++ₛ s).tail = s
⊢ drop (a :: l).length (a :: l ++ₛ s) = s
have rw₂ : drop l.length (a :: (l ++ₛ s)).tail = s
Tactic: rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
s : Stream' α
rw : drop (l.length + 1) (a :: l ++ₛ s) = s
rw₁ : drop l.length (a :: l ++ₛ s).tail = s
rw₂ : drop l.length (a :: (l ++ₛ s)).tail = s
⊢ drop (a :: l).length (a :: l ++ₛ s) = s
have rw₃ : drop l.length (l ++ₛ s) = s
Tactic: rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
s : Stream' α
rw : drop (l.length + 1) (a :: l ++ₛ s) = s
rw₁ : drop l.length (a :: l ++ₛ s).tail = s
rw₂ : drop l.length (a :: (l ++ₛ s)).tail = s
rw₃ : drop l.length (l ++ₛ s) = s
⊢ drop (a :: l).length (a :: l ++ₛ s) = s
have rw₄ : s = s
Tactic: rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]
have rw : s.head :: take (n + 1) s.tail = take (n + 1) s ++ [s.get (n + 1)]
Tactic: rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : s.head :: take (n + 1) s.tail = take (n + 1) s ++ [s.get (n + 1)]
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]
have rw₁ : s.head :: (take n s.tail ++ [s.tail.get n]) = take (n + 1) s ++ [s.get (n + 1)]
Tactic: rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : s.head :: take (n + 1) s.tail = take (n + 1) s ++ [s.get (n + 1)]
rw₁ : s.head :: (take n s.tail ++ [s.tail.get n]) = take (n + 1) s ++ [s.get (n + 1)]
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]
have rw₂ : s.head :: take n s.tail ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
Tactic: rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : s.head :: take (n + 1) s.tail = take (n + 1) s ++ [s.get (n + 1)]
rw₁ : s.head :: (take n s.tail ++ [s.tail.get n]) = take (n + 1) s ++ [s.get (n + 1)]
rw₂ : s.head :: take n s.tail ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]
have rw₃ : take n.succ s ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
Tactic: rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : s.head :: take (n + 1) s.tail = take (n + 1) s ++ [s.get (n + 1)]
rw₁ : s.head :: (take n s.tail ++ [s.tail.get n]) = take (n + 1) s ++ [s.get (n + 1)]
rw₂ : s.head :: take n s.tail ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
rw₃ : take n.succ s ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]
have rw₄ : take n.succ s ++ [s.get (n + 1)] = take (n + 1) s ++ [s.get (n + 1)]
Tactic: rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ (take n s).length = n
have zero : ∀ (s : Stream' α), (take 0 s).length = 0
Tactic: induction n generalizing s
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), (take 0 s).length = 0
⊢ (take n s).length = n
have succ : ∀ (n : ℕ), (∀ (s : Stream' α), (take n s).length = n) → ∀ (s : Stream' α), (take (n + 1) s).length = n + 1
Tactic: induction n generalizing s
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s
have rw : List.take 0 (take n s) = take 0 s
Tactic: rw [Nat.min_zero, List.take_zero, take_zero]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : List.take 0 (take n s) = take 0 s
⊢ List.take 0 (take n s) = take (min n 0) s
have rw₁ : [] = take 0 s
Tactic: rw [Nat.min_zero, List.take_zero, take_zero]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : List.take 0 (take n s) = take 0 s
rw₁ : [] = take 0 s
⊢ List.take 0 (take n s) = take (min n 0) s
have rw₂ : Eq.{u + 1} (α := List α) [] []
Tactic: rw [Nat.min_zero, List.take_zero, take_zero]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s
have rw : List.take m (take 0 s) = take 0 s
Tactic: rw [Nat.zero_min, take_zero, List.take_nil]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m : ℕ
rw : List.take m (take 0 s) = take 0 s
⊢ List.take m (take 0 s) = take (min 0 m) s
have rw₁ : Eq.{u + 1} (α := List α) (List.take m []) []
Tactic: rw [Nat.zero_min, take_zero, List.take_nil]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m : ℕ
rw : List.take m (take 0 s) = take 0 s
rw₁ : Eq.{u + 1} (α := List α) (List.take m []) []
⊢ List.take m (take 0 s) = take (min 0 m) s
have rw₂ : Eq.{u + 1} (α := List α) [] []
Tactic: rw [Nat.zero_min, take_zero, List.take_nil]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m n : ℕ
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
have rw : List.take (m + 1) (s.head :: take n s.tail) = take (min (n + 1) (m + 1)) s
Tactic: rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m n : ℕ
rw : List.take (m + 1) (s.head :: take n s.tail) = take (min (n + 1) (m + 1)) s
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
have rw₁ : s.head :: List.take m (take n s.tail) = take (min (n + 1) (m + 1)) s
Tactic: rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m n : ℕ
rw : List.take (m + 1) (s.head :: take n s.tail) = take (min (n + 1) (m + 1)) s
rw₁ : s.head :: List.take m (take n s.tail) = take (min (n + 1) (m + 1)) s
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
have rw₂ : s.head :: List.take m (take n s.tail) = take (min n m).succ s
Tactic: rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m n : ℕ
rw : List.take (m + 1) (s.head :: take n s.tail) = take (min (n + 1) (m + 1)) s
rw₁ : s.head :: List.take m (take n s.tail) = take (min (n + 1) (m + 1)) s
rw₂ : s.head :: List.take m (take n s.tail) = take (min n m).succ s
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
have rw₃ : s.head :: List.take m (take n s.tail) = s.head :: take (min n m) s.tail
Tactic: rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
m n : ℕ
rw : List.take (m + 1) (s.head :: take n s.tail) = take (min (n + 1) (m + 1)) s
rw₁ : s.head :: List.take m (take n s.tail) = take (min (n + 1) (m + 1)) s
rw₂ : s.head :: List.take m (take n s.tail) = take (min n m).succ s
rw₃ : s.head :: List.take m (take n s.tail) = s.head :: take (min n m) s.tail
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
have rw₄ : s.head :: take (min n m) s.tail = s.head :: take (min n m) s.tail
Tactic: rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
h : 0 < n + 1
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) 0 = some (s.get 0)
have simp : some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) 0 sorry) = some (s.get 0)
Tactic: simp only [length_take, zero_lt_succ, List.getElem?_eq_getElem]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) (k + 1) = some (s.get (k + 1))
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.head :: take n s.tail) (k + 1) = some (s.get (k + 1))
Tactic: rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.head :: take n s.tail) (k + 1) = some (s.get (k + 1))
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) (k + 1) = some (s.get (k + 1))
have rw₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n s.tail) k = some (s.get (k + 1))
Tactic: rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.head :: take n s.tail) (k + 1) = some (s.get (k + 1))
rw₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n s.tail) k = some (s.get (k + 1))
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) (k + 1) = some (s.get (k + 1))
have rw₂ : some (s.tail.get k) = some (s.get (k + 1))
Tactic: rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.head :: take n s.tail) (k + 1) = some (s.get (k + 1))
rw₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n s.tail) k = some (s.get (k + 1))
rw₂ : some (s.tail.get k) = some (s.get (k + 1))
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) (k + 1) = some (s.get (k + 1))
have rw₃ : some (s.tail.get k) = some (s.tail.get k)
Tactic: rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
xs : Stream' α
n : ℕ
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs
have succ : (take n xs ++ [xs.get n]).dropLast = take (n + 1 - 1) xs
Tactic: rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
xs : Stream' α
n : ℕ
succ : (take n xs ++ [xs.get n]).dropLast = take (n + 1 - 1) xs
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs
have succ₁ : take n xs = take (n + 1 - 1) xs
Tactic: rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
xs : Stream' α
n : ℕ
succ : (take n xs ++ [xs.get n]).dropLast = take (n + 1 - 1) xs
succ₁ : take n xs = take (n + 1 - 1) xs
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs
have succ₂ : take n xs = take n xs
Tactic: rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
xs : Stream' α
⊢ (take n xs).dropLast = take (n - 1) xs
have zero : (take 0 xs).dropLast = take (HSub.hSub (α := ℕ) 0 1) xs
Tactic: cases n with
  | zero => simp
  | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]
Cleared hypotheses: n