awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
rw : (map f s).head :: (map f s).tail = f s.head :: map f s.tail
rw₁ : (map f s).head :: map f s.tail = f s.head :: map f s.tail
⊢ map f s = f s.head :: map f s.tail
have rw₂ : f s.head :: map f s.tail = f s.head :: map f s.tail
Tactic: rw [← Stream'.eta (map f s), tail_map, head_map]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ map f (a :: s) = f a :: map f s
have rw : (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s
Tactic: rw [← Stream'.eta (map f (a::s)), map_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
h_1 : a ∈ s
n : ℕ
h : (fun (b : α) ↦ a = b) (s.get n)
⊢ (fun (b : β) ↦ f a = b) ((map f s).get n)
have rw : (fun (b : β) ↦ f a = b) (f (s.get n))
Tactic: rw [get_map, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
h_1 : a ∈ s
n : ℕ
h : (fun (b : α) ↦ a = b) (s.get n)
rw : f a = f (s.get n)
⊢ f a = (map f s).get n
have rw₁ : (fun (b : β) ↦ f (s.get n) = b) (f (s.get n))
Tactic: rw [get_map, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ zip f s₁ s₂ = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
have rw : (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
Tactic: rw [← Stream'.eta (zip f s₁ s₂)]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
⊢ const a = a :: const a
have a₁ : ∀ (n : ℕ), (const a).get n = (a :: const a).get n
Tactic: apply Stream'.ext
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
n : ℕ
⊢ (const a).get n = (a :: const a).get n
have a₁ : (const a).get 0 = (a :: const a).get 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
n : ℕ
a₁ : (const a).get 0 = (a :: const a).get 0
⊢ (const a).get n = (a :: const a).get n
have a₂ : ∀ (n : ℕ), (const a).get (n + 1) = (a :: const a).get (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
this : (a :: const a).tail = const a
⊢ (const a).tail = const a
have rwa : ∀ (this : (const a).tail = const a), (const a).tail = const a
Tactic: rwa [← const_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
⊢ (iterate f a).tail = iterate f (f a)
have a₁ : ∀ (n : ℕ), (iterate f a).tail.get n = (iterate f (f a)).get n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).tail.get n = (iterate f (f a)).get n
have a₁ : (iterate f a).get (n + 1) = (iterate f (f a)).get n
Tactic: rw [get_tail]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)
have a₁ : f ((iterate f a).get (n + 1)) = (iterate f (f a)).get (n + 1)
Tactic: rw [get_succ_iterate', ih, get_succ_iterate']
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
a₁ : f ((iterate f a).get (n + 1)) = (iterate f (f a)).get (n + 1)
⊢ (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)
have a₂ : f ((iterate f (f a)).get n) = (iterate f (f a)).get (n + 1)
Tactic: rw [get_succ_iterate', ih, get_succ_iterate']
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
a₁ : f ((iterate f a).get (n + 1)) = (iterate f (f a)).get (n + 1)
a₂ : f ((iterate f (f a)).get n) = (iterate f (f a)).get (n + 1)
⊢ (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)
have a₃ : f ((iterate f (f a)).get n) = f ((iterate f (f a)).get n)
Tactic: rw [get_succ_iterate', ih, get_succ_iterate']
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).get (n + 1) = (iterate f (f a)).get n
have a₁ : (iterate f a).get (HAdd.hAdd (α := ℕ) 0 1) = (iterate f (f a)).get 0
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [get_succ_iterate', ih, get_succ_iterate']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
a₁ : (iterate f a).get (HAdd.hAdd (α := ℕ) 0 1) = (iterate f (f a)).get 0
⊢ (iterate f a).get (n + 1) = (iterate f (f a)).get n
have a₂ : ∀ (n : ℕ) (ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n),
  (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [get_succ_iterate', ih, get_succ_iterate']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)
have rw : (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)
Tactic: rw [← Stream'.eta (iterate f a)]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)
have rw : (iterate f a).head :: iterate f (f a) = a :: iterate f (f a)
Tactic: rw [tail_iterate]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
f : α → α
a : α
⊢ (iterate f a).get n.succ = (iterate f (f a)).get n
have rw : (iterate f a).tail.get n = (iterate f (f a)).get n
Tactic: rw [get_succ, tail_iterate]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
f : α → α
a : α
rw : (iterate f a).tail.get n = (iterate f (f a)).get n
⊢ (iterate f a).get n.succ = (iterate f (f a)).get n
have rw₁ : (iterate f (f a)).get n = (iterate f (f a)).get n
Tactic: rw [get_succ, tail_iterate]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id a).tail = fr (const a).tail
have rw : fr (iterate id (id a)) = fr (const a)
Tactic: rw [tail_iterate, tail_const]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
⊢ iterate f (f a) = map f (iterate f a)
have h : ∀ (n : ℕ), iterate f (f a) n = map f (iterate f a) n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ iterate f (f a) (n + 1) = map f (iterate f a) (n + 1)
have h : f (iterate f (f a) n) = f (iterate f a (n + 1))
Tactic: unfold map iterate get
-- Lean 4 proof step from Mathlib.Data.Stream.Init (hypothesis)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))
have ih₁ : iterate f (f a) n = f (iterate f a n)
Tactic: rw [map, get] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))
have h : f (iterate f (f a) n) = f (f (iterate f a n))
Tactic: rw [iterate]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
⊢ iterate f (f a) n = map f (iterate f a) n
have h : iterate f (f a) 0 = map f (iterate f a) 0
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    unfold map iterate get
    rw [map, get] at ih
    rw [iterate]
    exact congrArg f ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
f : α → α
a : α
n : ℕ
h : iterate f (f a) 0 = map f (iterate f a) 0
⊢ iterate f (f a) n = map f (iterate f a) n
have h₁ : ∀ (n : ℕ) (ih : iterate f (f a) n = map f (iterate f a) n), iterate f (f a) (n + 1) = map f (iterate f a) (n + 1)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    unfold map iterate get
    rw [map, get] at ih
    rw [iterate]
    exact congrArg f ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ corec f g a = f a :: corec f g (g a)
have rw : f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
Tactic: rw [corec_def, map_eq, head_iterate, tail_iterate]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
⊢ corec id id a = const a
have rw : map id (iterate id a) = const a
Tactic: rw [corec_def, map_id, iterate_id]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
rw : map id (iterate id a) = const a
⊢ corec id id a = const a
have rw₁ : iterate id a = const a
Tactic: rw [corec_def, map_id, iterate_id]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
rw : map id (iterate id a) = const a
rw₁ : iterate id a = const a
⊢ corec id id a = const a
have rw₂ : const a = const a
Tactic: rw [corec_def, map_id, iterate_id]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)
have rw : g a :: corec g f (f a) = g a :: corec g f (f a)
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
⊢ (unfolds head tail s).get (n + 1) = s.get (n + 1)
have succ : (unfolds head tail s).tail.get n = s.get (n + 1)
Tactic: rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
succ : (unfolds head tail s).tail.get n = s.get (n + 1)
⊢ (unfolds head tail s).get (n + 1) = s.get (n + 1)
have succ₁ : (unfolds head tail s).tail.get n = s.tail.get n
Tactic: rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
succ : (unfolds head tail s).tail.get n = s.get (n + 1)
succ₁ : (unfolds head tail s).tail.get n = s.tail.get n
⊢ (unfolds head tail s).get (n + 1) = s.get (n + 1)
have succ₂ : (s.head :: unfolds head tail s.tail).tail.get n = s.tail.get n
Tactic: rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
succ : (unfolds head tail s).tail.get n = s.get (n + 1)
succ₁ : (unfolds head tail s).tail.get n = s.tail.get n
succ₂ : (s.head :: unfolds head tail s.tail).tail.get n = s.tail.get n
⊢ (unfolds head tail s).get (n + 1) = s.get (n + 1)
have succ₃ : (unfolds head tail s.tail).get n = s.tail.get n
Tactic: rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
succ : (unfolds head tail s).tail.get n = s.get (n + 1)
succ₁ : (unfolds head tail s).tail.get n = s.tail.get n
succ₂ : (s.head :: unfolds head tail s.tail).tail.get n = s.tail.get n
succ₃ : (unfolds head tail s.tail).get n = s.tail.get n
⊢ (unfolds head tail s).get (n + 1) = s.get (n + 1)
have succ₄ : s.tail.get n = s.tail.get n
Tactic: rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ (unfolds head tail s).get n = s.get n
have zero : ∀ (s : Stream' α), (unfolds head tail s).get 0 = s.get 0
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), (unfolds head tail s).get 0 = s.get 0
⊢ (unfolds head tail s).get n = s.get n
have succ : ∀ (n : ℕ) (ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n) (s : Stream' α),
  (unfolds head tail s).get (n + 1) = s.get (n + 1)
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun (x : Stream' α × Stream' α) ↦
        match (motive := Stream' α × Stream' α → α) x with
        | (s₁, snd) => s₁.head)
      (fun (x : Stream' α × Stream' α) ↦
        match (motive := Stream' α × Stream' α → Stream' α × Stream' α) x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t
have rw : (match (motive := Stream' α × Stream' α → α) (s₁, s₂) with
    | (s₁, snd) => s₁.head) ::
    corec (α := Stream' α × Stream' α)
      (fun (x : Stream' α × Stream' α) ↦
        (match (motive := Stream' α × Stream' α → α) x with
          | (s₁, snd) => s₁.head :
          α))
      (fun (x : Stream' α × Stream' α) ↦
        (match (motive := Stream' α × Stream' α → Stream' α × Stream' α) x with
          | (s₁, s₂) => (s₂, s₁.tail) :
          Stream' α × Stream' α))
      (match (motive := Stream' α × Stream' α → Stream' α × Stream' α) (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail) :
        Stream' α × Stream' α) =
  s₁.head :: s₂.head :: t
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      corec (fun (x : Stream' α × Stream' α) ↦ x.fst.head) (fun (x : Stream' α × Stream' α) ↦ (x.snd, x.fst.tail))
        (s₂, s₁.tail) =
    s₁.head :: s₂.head :: t
have rw : s₁.head ::
    (s₂, s₁.tail).fst.head ::
      corec (fun (x : Stream' α × Stream' α) ↦ x.fst.head) (fun (x : Stream' α × Stream' α) ↦ (x.snd, x.fst.tail))
        ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
  s₁.head :: s₂.head :: t
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
⊢ Eq (α := Stream' α)
    (tail
      (corec
        (fun (x : Stream' α × Stream' α) ↦
          match (motive := Stream' α × Stream' α → α) x with
          | (s₁, snd) => s₁.head)
        (fun (x : Stream' α × Stream' α) ↦
          match (motive := Stream' α × Stream' α → Stream' α × Stream' α) x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)))
    (corec
      (fun (x : Stream' α × Stream' α) ↦
        match (motive := Stream' α × Stream' α → α) x with
        | (s₁, snd) => s₁.head)
      (fun (x : Stream' α × Stream' α) ↦
        match (motive := Stream' α × Stream' α → Stream' α × Stream' α) x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail))
have rw : Eq (α := Stream' α)
  (tail
      ((match (motive := Stream' α × Stream' α → α) (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec (α := Stream' α × Stream' α)
          (fun (x : Stream' α × Stream' α) ↦
            (match (motive := Stream' α × Stream' α → α) x with
              | (s₁, snd) => s₁.head :
              α))
          (fun (x : Stream' α × Stream' α) ↦
            (match (motive := Stream' α × Stream' α → Stream' α × Stream' α) x with
              | (s₁, s₂) => (s₂, s₁.tail) :
              Stream' α × Stream' α))
          (match (motive := Stream' α × Stream' α → Stream' α × Stream' α) (s₁, s₂) with
            | (s₁, s₂) => (s₂, s₁.tail) :
            Stream' α × Stream' α)) :
    Stream' α)
  (corec
      (fun (x : Stream' α × Stream' α) ↦
        match (motive := Stream' α × Stream' α → α) x with
        | (s₁, snd) => s₁.head)
      (fun (x : Stream' α × Stream' α) ↦
        match (motive := Stream' α × Stream' α → Stream' α × Stream' α) x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail) :
    Stream' α)
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail
have rw : s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail
Tactic: rw [interleave_eq s₁ s₂]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1)) = s₁.get (n + 1)
have change : (s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ
Tactic: change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n)
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ
have rw : (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ
Tactic: rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ
have rw : s₁.tail.get n = s₁.get n.succ
Tactic: rw [get_interleave_left n (tail s₁) (tail s₂)]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1) + 1) = s₂.get (n + 1)
have change : (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ
Tactic: change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n)
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ
have rw : s₂.tail.get n = s₂.get n.succ
Tactic: rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons,
      get_interleave_right n (tail s₁) (tail s₂)]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s₁ s₂ : Stream' α
h_1 : a ∈ s₁
n : ℕ
h : (fun (b : α) ↦ a = b) (s₁.get n)
⊢ (fun (b : α) ↦ a = b) ((s₁ ⋈ s₂).get (2 * n))
have rw : (fun (b : α) ↦ s₁.get n = b) ((s₁ ⋈ s₂).get (2 * n))
Tactic: rw [h, get_interleave_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s₁ s₂ : Stream' α
h_1 : a ∈ s₁
n : ℕ
h : (fun (b : α) ↦ a = b) (s₁.get n)
rw : s₁.get n = (s₁ ⋈ s₂).get (2 * n)
⊢ a = (s₁ ⋈ s₂).get (2 * n)
have rw₁ : (fun (b : α) ↦ s₁.get n = b) (s₁.get n)
Tactic: rw [h, get_interleave_left]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s₁ s₂ : Stream' α
h_1 : a ∈ s₂
n : ℕ
h : (fun (b : α) ↦ a = b) (s₂.get n)
⊢ (fun (b : α) ↦ a = b) ((s₁ ⋈ s₂).get (2 * n + 1))
have rw : (fun (b : α) ↦ s₂.get n = b) ((s₁ ⋈ s₂).get (2 * n + 1))
Tactic: rw [h, get_interleave_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s₁ s₂ : Stream' α
h_1 : a ∈ s₂
n : ℕ
h : (fun (b : α) ↦ a = b) (s₂.get n)
rw : s₂.get n = (s₁ ⋈ s₂).get (2 * n + 1)
⊢ a = (s₁ ⋈ s₂).get (2 * n + 1)
have rw₁ : (fun (b : α) ↦ s₂.get n = b) (s₂.get n)
Tactic: rw [h, get_interleave_right]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
⊢ (corec head (fun (s : Stream' α) ↦ s.tail.tail) s).tail = corec head (fun (s : Stream' α) ↦ s.tail.tail) s.tail.tail
have rw : (s.head :: corec head (fun (s : Stream' α) ↦ s.tail.tail) s.tail.tail).tail =
  corec head (fun (s : Stream' α) ↦ s.tail.tail) s.tail.tail
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ corec head (fun (s : Stream' α) ↦ s.tail.tail) (a₁ :: a₂ :: s) =
    a₁ :: corec head (fun (s : Stream' α) ↦ s.tail.tail) s
have rw : (a₁ :: a₂ :: s).head :: corec head (fun (s : Stream' α) ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
  a₁ :: corec head (fun (s : Stream' α) ↦ s.tail.tail) s
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁_1 s₂_1 s₁' s₁ : Stream' α
h : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ s₁'.head = s₁.head ∧ (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁'.tail s₁.tail
have rw : (s₁ ⋈ s₂).even.head = s₁.head ∧
  (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁_1 s₂_1 s₁' s₁ : Stream' α
h : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧
    (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
have left : (s₁ ⋈ s₂).even.head = s₁.head
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁_1 s₂_1 s₁' s₁ : Stream' α
h : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
left : (s₁ ⋈ s₂).even.head = s₁.head
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧
    (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
have right : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁_1 s₂_1 s₁' s₁ : Stream' α
h : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even
have rw : (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).even.tail = (s₁.tail ⋈ s₂.tail).even
Tactic: rw [interleave_eq, even_cons_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁_1 s₂_1 s₁' s₁ : Stream' α
h : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
rw : (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).even.tail = (s₁.tail ⋈ s₂.tail).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even
have rw₁ : (s₁.head :: (s₁.tail ⋈ s₂.tail).even).tail = (s₁.tail ⋈ s₂.tail).even
Tactic: rw [interleave_eq, even_cons_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁_1 s₂_1 s₁' s₁ : Stream' α
h : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
rw : (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).even.tail = (s₁.tail ⋈ s₂.tail).even
rw₁ : (s₁.head :: (s₁.tail ⋈ s₂.tail).even).tail = (s₁.tail ⋈ s₂.tail).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even
have rw₂ : (s₁.tail ⋈ s₂.tail).even = (s₁.tail ⋈ s₂.tail).even
Tactic: rw [interleave_eq, even_cons_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ s'.head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) s'.tail s.tail
have rw : (s.even ⋈ s.odd).head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
have left : (s.even ⋈ s.odd).head = s.head
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
left : (s.even ⋈ s.odd).head = s.head
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
have right : (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n.succ)
have change : s.even.get n.succ = s.get (2 * n).succ.succ
Tactic: change get (even s) (succ n) = get s (succ (succ (2 * n)))
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n).succ.succ
have rw : s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)
Tactic: rw [get_succ, get_succ, tail_even, get_even n]