awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Stream.Init
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
h : 0 < (b :: x).length
⊢ (b :: x ++ₛ a).get 0 = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) 0 h

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
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 + 1 < (b :: x).length
⊢ n < x.length

Tactic:
simpa using h
-- Module: Mathlib.Data.Stream.Init
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 + 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:
simp [ih n (by simpa using h), cons_append_stream]

Premises used: Stream'.cons_append_stream
-- Module: Mathlib.Data.Stream.Init
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
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
⊢ (x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) 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]

Premises used: Stream'.cons_append_stream, Stream'.cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
nil : ([] ++ₛ a).get (List.length.{u} (α := α) [] + n) = a.get n
cons :
  ∀ (head : α) (tail : List α),
    (tail ++ₛ a).get (tail.length + n) = a.get n → (head :: tail ++ₛ a).get ((head :: tail).length + n) = a.get n
⊢ (x ++ₛ a).get (x.length + n) = a.get n

Tactic:
induction x
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ ([] ++ₛ a).get (List.length.{u} (α := α) [] + n) = a.get n

Tactic:
simp [Nat.succ_add, *, cons_append_stream]

Premises used: Stream'.cons_append_stream, Nat.succ_add
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
head : α
tail : List α
tail_ih : (tail ++ₛ a).get (tail.length + n) = a.get n
⊢ (head :: tail ++ₛ a).get ((head :: tail).length + n) = a.get n

Tactic:
simp [Nat.succ_add, *, cons_append_stream]

Premises used: Stream'.cons_append_stream, Nat.succ_add
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x : List α
a : Stream' α
⊢ (x ++ₛ a).get x.length = a.get 0

Tactic:
get_append_right 0 x a

Premises used: Stream'.get, OfNat.ofNat, Stream'.get_append_right
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
a₁ : ∀ (n : ℕ), a.get n = b.get n
⊢ a = b

Tactic:
ext n
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ 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
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x : List α
a b : Stream' α
n : ℕ
h :
  Eq.{u + 1} (α := α) ((fun (a : Stream' α) ↦ a.get (x.length + n)) (x ++ₛ a))
    ((fun (a : Stream' α) ↦ a.get (x.length + n)) (x ++ₛ b))
⊢ a.get n = b.get n

Tactic:
simpa using h
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x : List α
a b : Stream' α
⊢ a = b → x ++ₛ a = x ++ₛ b

Tactic:
simp +contextual
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
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₂
⊢ x = y

Tactic:
apply List.ext_getElem hl

Premises used: List.ext_getElem
-- Module: Mathlib.Data.Stream.Init
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' α
rw₂ : (y ++ₛ b).get i = (y ++ₛ b).get i
a₄ : Stream' α
rw₃ : (y ++ₛ b).get i = (y ++ₛ b).get i
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₂

Tactic:
rw [← get_append_left, ← get_append_left, h]

Premises used: Stream'.get_append_left
-- Module: Mathlib.Data.Stream.Init
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)
rw₄ rw₅ : f a :: (List.map f l ++ₛ map f s) = f a :: (List.map f l ++ₛ map f s)
⊢ 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]

Premises used: Stream'.cons_append_stream, List.map_cons, Stream'.map_cons
-- Module: Mathlib.Data.Stream.Init
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
rw₄ rw₅ : s = s
⊢ drop (a :: l).length (a :: l ++ₛ s) = s

Tactic:
rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]

Premises used: Stream'.cons_append_stream, List.length_cons, Stream'.drop_succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ [s.head] ++ₛ s.tail = s

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ take 0 s = []

Tactic:
rfl

Premises used: Stream'.take, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ take n.succ s = s.head :: take n s.tail

Tactic:
rfl

Premises used: Stream'.take, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
n : ℕ
s : Stream' α
⊢ take (n + 1) (a :: s) = a :: take n s

Tactic:
rfl

Premises used: Stream'.take, Stream'.get, Stream'.cons, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
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)]
rw₄ rw₅ : take n.succ s ++ [s.get (n + 1)] = take (n + 1) s ++ [s.get (n + 1)]
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]

Premises used: Stream'.get_tail, Stream'.take_succ, List.cons_append
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), (take 0 s).length = 0
succ : ∀ (n : ℕ), (∀ (s : Stream' α), (take n s).length = n) → ∀ (s : Stream' α), (take (n + 1) s).length = n + 1
⊢ (take n s).length = n

Tactic:
induction n generalizing s
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ (take 0 s).length = 0

Tactic:
simp [*, take_succ]

Premises used: Stream'.take_succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
h : ∀ (s : Stream' α), (take n s).length = n
s : Stream' α
⊢ (take (n + 1) s).length = n + 1

Tactic:
simp [*, take_succ]

Premises used: Stream'.take_succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
rw : List.take 0 (take n s) = take 0 s
rw₁ : [] = take 0 s
rw₂ rw₃ : Eq.{u + 1} (α := List α) [] []
⊢ List.take 0 (take n s) = take (min n 0) s

Tactic:
rw [Nat.min_zero, List.take_zero, take_zero]

Premises used: List.take_zero, Stream'.take_zero, Nat.min_zero
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
m : ℕ
rw : List.take m (take 0 s) = take 0 s
rw₁ : Eq.{u + 1} (α := List α) (List.take m []) []
rw₂ rw₃ : Eq.{u + 1} (α := List α) [] []
⊢ List.take m (take 0 s) = take (min 0 m) s

Tactic:
rw [Nat.zero_min, take_zero, List.take_nil]

Premises used: List.take_nil, Stream'.take_zero, Nat.zero_min
-- Module: Mathlib.Data.Stream.Init
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
rw₄ rw₅ : s.head :: take (min n m) 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

Tactic:
rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]

Premises used: List.take_succ_cons, Stream'.take_succ, Nat.succ_min_succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ take n s ++ [s.get n] = take (n + 1) s

Tactic:
(take_succ' n).symm

Premises used: Stream'.take_succ', Eq.symm
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
h : 0 < n + 1
simp : some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) 0 ⋯) = some (s.get 0)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) 0 = some (s.get 0)

Tactic:
simp only [length_take, zero_lt_succ, List.getElem?_eq_getElem]

Premises used: Nat.zero_lt_succ, List.getElem?_eq_getElem, Stream'.length_take
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
h : 0 < n + 1
⊢ some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) 0 ⋯) = some (s.get 0)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
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))
rw₃ rw₄ : some (s.tail.get k) = some (s.tail.get k)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n + 1) s) (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]

Premises used: List.getElem?_cons_succ, Stream'.get_succ, Stream'.take_succ, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ s) n = some (s.get n)

Tactic:
getElem?_take (Nat.lt_succ_self n)

Premises used: Nat.lt_succ_self, Stream'.getElem?_take
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
xs : Stream' α
⊢ (take 0 xs).dropLast = take (HSub.hSub (α := ℕ) 0 1) xs

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
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
succ₂ succ₃ : take n xs = take n xs
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs

Tactic:
rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Stream'.take_succ', List.dropLast_concat
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
xs : Stream' α
zero : (take 0 xs).dropLast = take (HSub.hSub (α := ℕ) 0 1) xs
succ : ∀ (n : ℕ), (take (n + 1) xs).dropLast = take (n + 1 - 1) xs
⊢ (take n xs).dropLast = take (n - 1) xs

Tactic:
cases n with
  | zero => simp
  | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Stream'.take_succ', List.dropLast_concat, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ take 0 s ++ₛ drop 0 s = s

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), take n s ++ₛ drop n s = s
s : Stream' α
succ : s.head :: take n s.tail ++ₛ drop (n + 1) s = s
succ₁ : s.head :: take n s.tail ++ₛ drop n s.tail = s
succ₂ : s.head :: (take n s.tail ++ₛ drop n s.tail) = s
succ₃ : s.head :: s.tail = s
succ₄ succ₅ : s = s
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s

Tactic:
rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]

Premises used: Stream'.cons_append_stream, Stream'.drop_succ, Stream'.take_succ, Stream'.eta, Stream'.tail
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), take 0 s ++ₛ drop 0 s = s
succ :
  ∀ (n : ℕ) (ih : ∀ (s : Stream' α), take n s ++ₛ drop n s = s) (s : Stream' α), take (n + 1) s ++ₛ drop (n + 1) s = s
⊢ take n s ++ₛ drop n s = s

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]

Premises used: Stream'.cons_append_stream, Stream'.drop_succ, Stream'.take_succ, Nat.zero, Stream'.eta, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
nil : [] ++ take n a = take (List.length.{u} (α := α) [] + n) ([] ++ₛ a)
cons :
  ∀ (head : α) (tail : List α),
    tail ++ take n a = take (tail.length + n) (tail ++ₛ a) →
      head :: tail ++ take n a = take ((head :: tail).length + n) (head :: tail ++ₛ a)
⊢ x ++ take n a = take (x.length + n) (x ++ₛ a)

Tactic:
induction x
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ [] ++ take n a = take (List.length.{u} (α := α) [] + n) ([] ++ₛ a)

Tactic:
simp [take, Nat.add_comm, cons_append_stream, *]

Premises used: Stream'.take, Stream'.cons_append_stream, Nat.add_comm
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
head : α
tail : List α
tail_ih : tail ++ take n a = take (tail.length + n) (tail ++ₛ a)
⊢ head :: tail ++ take n a = take ((head :: tail).length + n) (head :: tail ++ₛ a)

Tactic:
simp [take, Nat.add_comm, cons_append_stream, *]

Premises used: Stream'.take, Stream'.cons_append_stream, Nat.add_comm
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
nth_rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h = (take n a ++ₛ drop n a).get m
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h = a.get m

Tactic:
nth_rw 2 [← append_take_drop n a]

Premises used: Stream'.append_take_drop
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h
h₁ : m < (take n a).length
rw₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h
h₂ : m < (take n a).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h = (take n a ++ₛ drop n a).get m

Tactic:
rw [get_append_left]

Premises used: Stream'.get_append_left
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ (take n (x ++ₛ a)).length = (List.take n x).length

Tactic:
simp [h]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
apply :
  ∀ (i : ℕ) (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.take n x) i h₂
⊢ take n (x ++ₛ a) = List.take n x

Tactic:
apply List.ext_getElem (by simp [h])

Premises used: List.ext_getElem
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i : ℕ
_ :
  ∀ (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.take n x) i h₂
⊢ ∀ (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.take n x) i h₂

Tactic:
_
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i : ℕ
h₁ : i < (take n (x ++ₛ a)).length
_ :
  ∀ (h₂ : i < (List.take n x).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.take n x) i h₂
⊢ ∀ (h₂ : i < (List.take n x).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.take n x) i h₂

Tactic:
_
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i : ℕ
h₁_1 : i < (take n (x ++ₛ a)).length
h₂_1 : i < (List.take n x).length
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁_1 =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯
rw₁ : (x ++ₛ a).get i = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯
rw₂ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯
h₁ : i < x.length
rw₃ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯
h₂ : i < x.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁_1 =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.take n x) i h₂_1

Tactic:
rw [List.getElem_take, take_get, get_append_left]

Premises used: Stream'.take_get, List.getElem_take, Stream'.get_append_left
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)
hl : (take (m + n) a).length = (take m a ++ take n (drop m a)).length
⊢ take (m + n) a = take m a ++ take n (drop m a)

Tactic:
apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n)

Premises used: Stream'.drop, HAdd.hAdd, Stream'.append_left_injective
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)

Tactic:
simp [-drop_drop]

Premises used: Stream'.drop_drop
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
⊢ (take (m + n) a).length = (take m a ++ take n (drop m a)).length

Tactic:
simp [-drop_drop]

Premises used: Stream'.drop_drop
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a = List.take m (take n a)

Tactic:
simp [h]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
rw : List.take m (take n a) <+: take n a
⊢ take m a <+: take n a

Tactic:
rw [(by simp [h] : a.take m = (a.take n).take m)]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a

Tactic:
apply List.take_prefix

Premises used: List.take_prefix
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n

Tactic:
simpa using h.length_le

Premises used: List.IsPrefix.length_le
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
hl : (List.map f (take n a)).length = (take n (map f a)).length
h :
  ∀ (i : ℕ) (h₁ : i < (List.map f (take n a)).length) (h₂ : i < (take n (map f a)).length),
    getElem (valid := fun (as : List β) (i : ℕ) ↦ i < as.length) (List.map f (take n a)) i h₁ =
      getElem (valid := fun (as : List β) (i : ℕ) ↦ i < as.length) (take n (map f a)) i h₂
⊢ List.map f (take n a) = take n (map f a)

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ (List.map f (take n a)).length = (take n (map f a)).length

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ ∀ (i : ℕ) (h₁ : i < (List.map f (take n a)).length) (h₂ : i < (take n (map f a)).length),
    getElem (valid := fun (as : List β) (i : ℕ) ↦ i < as.length) (List.map f (take n a)) i h₁ =
      getElem (valid := fun (as : List β) (i : ℕ) ↦ i < as.length) (take n (map f a)) i h₂

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
hl : (take n (drop m a)).length = (List.drop m (take (m + n) a)).length
h :
  ∀ (i : ℕ) (h₁ : i < (take n (drop m a)).length) (h₂ : i < (List.drop m (take (m + n) a)).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (drop m a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.drop m (take (m + n) a)) i h₂
⊢ take n (drop m a) = List.drop m (take (m + n) a)

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
⊢ (take n (drop m a)).length = (List.drop m (take (m + n) a)).length

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
m n : ℕ
a : Stream' α
⊢ ∀ (i : ℕ) (h₁ : i < (take n (drop m a)).length) (h₂ : i < (List.drop m (take (m + n) a)).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (drop m a)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.drop m (take (m + n) a)) i h₂

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
obtain : ∀ (m : ℕ) (hm : x.length = n + m), drop n (x ++ₛ a) = List.drop n x ++ₛ a
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
a₁ : ∀ (k : ℕ), (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
ext k
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
a₁ : k < m → (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
a₂ : ∀ (hk : m ≤ k), (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
rcases lt_or_ge k m with _ | hk

Premises used: lt_or_ge
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h_1 : k < m
a₁ : k < (List.drop n x).length
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
rw [get_drop, get_append_left, get_append_left, List.getElem_drop]

Premises used: List.getElem_drop, Stream'.get_append_left, Stream'.get_drop
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h_1 : k < m
⊢ k < (List.drop n x).length

Tactic:
simpa [hm]