awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
xs : Stream' α
zero : (take 0 xs).dropLast = take (HSub.hSub (α := ℕ) 0 1) xs
⊢ (take n xs).dropLast = take (n - 1) xs
have succ : ∀ (n : ℕ), (take (n + 1) xs).dropLast = take (n + 1 - 1) xs
Tactic: cases n with
  | zero => simp
  | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), take n s ++ₛ drop n s = s
s : Stream' α
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s
have succ : s.head :: take n s.tail ++ₛ drop (n + 1) s = s
Tactic: rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s
have succ₁ : s.head :: take n s.tail ++ₛ drop n s.tail = s
Tactic: rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s
have succ₂ : s.head :: (take n s.tail ++ₛ drop n s.tail) = s
Tactic: rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s
have succ₃ : s.head :: s.tail = s
Tactic: rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s
have succ₄ : s = s
Tactic: rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ take n s ++ₛ drop n s = s
have zero : ∀ (s : Stream' α), take 0 s ++ₛ drop 0 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]
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 ++ₛ drop 0 s = s
⊢ take n s ++ₛ drop n s = s
have succ : ∀ (n : ℕ) (ih : ∀ (s : Stream' α), take n s ++ₛ drop n s = s) (s : Stream' α), take (n + 1) s ++ₛ drop (n + 1) 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]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ x ++ take n a = take (x.length + n) (x ++ₛ a)
have nil : [] ++ take n a = take (List.length.{u} (α := α) [] + n) ([] ++ₛ a)
Tactic: induction x
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
nil : [] ++ take n a = take (List.length.{u} (α := α) [] + n) ([] ++ₛ a)
⊢ x ++ take n a = take (x.length + n) (x ++ₛ a)
have 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)
Tactic: induction x
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h = a.get m
have nth_rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n a) m h = (take n a ++ₛ drop n a).get m
Tactic: nth_rw 2 [← append_take_drop n a]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
m n : ℕ
a : Stream' α
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
have 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
Tactic: rw [get_append_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ take n (x ++ₛ a) = List.take n x
have 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₂
Tactic: apply List.ext_getElem (by simp [h])
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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₂
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i sorry
Tactic: rw [List.getElem_take, take_get, get_append_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i ⋯
⊢ 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₂
have rw₁ : (x ++ₛ a).get i = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i sorry
Tactic: rw [List.getElem_take, take_get, get_append_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
    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 ⋯
⊢ 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₂
have rw₂ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x i sorry
Tactic: rw [List.getElem_take, take_get, get_append_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n (x ++ₛ a)) i h₁ =
    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 ⋯
⊢ 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₂
have h₁ : i < x.length
Tactic: rw [List.getElem_take, take_get, get_append_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a = take m a ++ take n (drop m a)
have h : take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)
Tactic: apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n)
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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)
⊢ take (m + n) a = take m a ++ take n (drop m a)
have hl : (take (m + n) a).length = (take m a ++ take n (drop m a)).length
Tactic: apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n)
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a <+: take n a
have rw : List.take m (take n a) <+: take n a
Tactic: rw [(by simp [h] : a.take m = (a.take n).take m)]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ List.map f (take n a) = take n (map f a)
have hl : (List.map f (take n a)).length = (take n (map f a)).length
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
hl : (List.map f (take n a)).length = (take n (map f a)).length
⊢ List.map f (take n a) = take n (map f a)
have 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₂
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
m n : ℕ
a : Stream' α
⊢ take n (drop m a) = List.drop m (take (m + n) a)
have hl : (take n (drop m a)).length = (List.drop m (take (m + n) a)).length
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
m n : ℕ
a : Stream' α
hl : (take n (drop m a)).length = (List.drop m (take (m + n) a)).length
⊢ take n (drop m a) = List.drop m (take (m + n) a)
have 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₂
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a
have obtain : ∀ (m : ℕ) (hm : x.length = n + m), drop n (x ++ₛ a) = List.drop n x ++ₛ a
Tactic: obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a
have a₁ : ∀ (k : ℕ), (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
Tactic: ext k
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
have a₁ : k < m → (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
Tactic: rcases lt_or_ge k m with _ | hk
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
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
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
have a₂ : ∀ (hk : m ≤ k), (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
Tactic: rcases lt_or_ge k m with _ | hk
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h_1 : k < m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
have a₁ : k < (List.drop n x).length
Tactic: rw [get_drop, get_append_left, get_append_left, List.getElem_drop]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : m ≤ k
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
have a₁ : ∀ (p : ℕ) (hk : m ≤ m + p), (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
Tactic: obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Stream.Init (hypothesis)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
have hm' : m = (List.drop n x).length
Tactic: have hm' : m = (x.drop n).length := by simp [hm]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
have a₁ : (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
Tactic: simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
a₁ : (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
have a₂ : (x ++ₛ a).get (n + m + p) = (List.drop n x ++ₛ a).get (m + p)
Tactic: simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
a₁ : (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
a₂ : (x ++ₛ a).get (n + m + p) = (List.drop n x ++ₛ a).get (m + p)
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
have a₃ : (x ++ₛ a).get (x.length + p) = (List.drop n x ++ₛ a).get (m + p)
Tactic: simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
a₁ : (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
a₂ : (x ++ₛ a).get (n + m + p) = (List.drop n x ++ₛ a).get (m + p)
a₃ : (x ++ₛ a).get (x.length + p) = (List.drop n x ++ₛ a).get (m + p)
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
have a₄ : a.get p = (List.drop n x ++ₛ a).get (m + p)
Tactic: simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
a₁ : (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
a₂ : (x ++ₛ a).get (n + m + p) = (List.drop n x ++ₛ a).get (m + p)
a₃ : (x ++ₛ a).get (x.length + p) = (List.drop n x ++ₛ a).get (m + p)
a₄ : a.get p = (List.drop n x ++ₛ a).get (m + p)
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
have a₅ : a.get p = (List.drop n x ++ₛ a).get ((List.drop n x).length + p)
Tactic: simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂
have a : ∀ (n : ℕ), s₁.get n = s₂.get n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : s₁.get n = s₂.get n
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ = some (s₂.get n.succ)
Tactic: rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : s₁.get n = s₂.get n
rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ = some (s₂.get n.succ)
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)
have rw₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ
Tactic: rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : s₁.get n = s₂.get n
rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ = some (s₂.get n.succ)
rw₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)
have rw₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ
Tactic: rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (hypothesis)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : s₁.get n = s₂.get n
⊢ s₁.get (n + 1) = s₂.get (n + 1)
have h₁ : some (s₁.get n.succ) = some (s₂.get n.succ)
Tactic: have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ s₁.get n = s₂.get n
have a : s₁.get 0 = s₂.get 0
Tactic: induction n with
  | zero => simpa [take] using h 1
  | succ n =>
    have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
    injection h₁
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a : s₁.get 0 = s₂.get 0
⊢ s₁.get n = s₂.get n
have a₁ : ∀ (n : ℕ), s₁.get n = s₂.get n → s₁.get (n + 1) = s₂.get (n + 1)
Tactic: induction n with
  | zero => simpa [take] using h 1
  | succ n =>
    have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
    injection h₁
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
have nil : Stream'.cycleF (a', [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', [], a, l)) =
  [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
have cons : Stream'.cycleF (a', a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
  a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Tactic: rw [corec_eq, Stream'.cycle_g_cons, ih a₁]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
l' : List α
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
have nil : ∀ (a' : α),
  corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Tactic: induction l' generalizing a' with
      | nil => rw [corec_eq]; rfl
      | cons a₁ l₁ ih => rw [corec_eq, Stream'.cycle_g_cons, ih a₁]; rfl
Cleared hypotheses: l', a'
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
l' : List α
a' : α
nil :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
have cons : ∀ (a₁ : α) (l₁ : List α)
  (ih :
    ∀ (a' : α),
      corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) =
        a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l))
  (a' : α),
  corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Tactic: induction l' generalizing a' with
      | nil => rw [corec_eq]; rfl
      | cons a₁ l₁ ih => rw [corec_eq, Stream'.cycle_g_cons, ih a₁]; rfl
Cleared hypotheses: l', a'
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ cycle l h
have rw : a ∈ l ++ₛ cycle l h
Tactic: rw [cycle_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail
have rwa : fr ([a] ++ₛ cycle [a] sorry).tail = fr (const a).tail
Tactic: rwa [cycle_eq, const_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
rwa : fr ([a] ++ₛ cycle [a] ⋯).tail = fr (const a).tail
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail
have rwa₁ : fr ([a] ++ₛ cycle [a] sorry).tail = fr (a :: const a).tail
Tactic: rwa [cycle_eq, const_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail
have rw : id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
⊢ s.tails.get (n + 1) = drop (n + 1) s.tail
have succ : s.tails.tail.get n = drop (n + 1) s.tail
Tactic: rw [get_succ, drop_succ, tails_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
succ : s.tails.tail.get n = drop (n + 1) s.tail
⊢ s.tails.get (n + 1) = drop (n + 1) s.tail
have succ₁ : s.tails.tail.get n = drop n s.tail.tail
Tactic: rw [get_succ, drop_succ, tails_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
succ : s.tails.tail.get n = drop (n + 1) s.tail
succ₁ : s.tails.tail.get n = drop n s.tail.tail
⊢ s.tails.get (n + 1) = drop (n + 1) s.tail
have succ₂ : (s.tail :: s.tail.tails).tail.get n = drop n s.tail.tail
Tactic: rw [get_succ, drop_succ, tails_eq, tail_cons, ih]