awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
R : Stream' α → Stream' α → Prop
bisim : IsBisimulation R
s₁ s₂ : Stream' α
⊢ R s₁ s₂ → s₁ = s₂

Tactic:
fun r =>
  Stream'.ext fun n => And.left (get_of_bisim R bisim n r)

Premises used: And.left, Stream'.get_of_bisim, Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁_1 s₂_1 : Stream' α
hh : s₁_1.head = s₂_1.head
ht₁ : s₁_1 = s₁_1.tail
ht₂ : s₂_1 = s₂_1.tail
s₁ s₂ : Stream' α
h : (fun (s₁ s₂ : Stream' α) ↦ s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁.head = s₂.head ∧ (fun (s₁ s₂ : Stream' α) ↦ s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁.tail s₂.tail

Tactic:
grind
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂

Tactic:
fun hh ht =>
  eq_of_bisim
    (fun s₁ s₂ =>
      head s₁ = head s₂ ∧
        ∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂))
    (fun s₁ s₂ h =>
      have h₁ : head s₁ = head s₂ := And.left h
      have h₂ : head (tail s₁) = head (tail s₂) := And.right h α (@head α) h₁
      have h₃ :
        ∀ (β : Type u) (fr : Stream' α → β),
          fr (tail s₁) = fr (tail s₂) → fr (tail (tail s₁)) = fr (tail (tail s₂)) :=
        fun β fr => And.right h β fun s => fr (tail s)
      And.intro h₁ (And.intro h₂ h₃))
    (And.intro hh ht)

Premises used: And, And.right, And.left, And.intro, Stream'.eq_of_bisim, Stream'.tail, Eq, Stream'.head
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
rw : fr (iterate id (id a)) = fr (const a)
⊢ fr (iterate id a).tail = fr (const a).tail

Tactic:
rw [tail_iterate, tail_const]

Premises used: Stream'.tail_iterate, Stream'.tail_const
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id (id a)) = fr (const a)

Tactic:
ch
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id (id a)) = fr (const a)

Tactic:
exact ch
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
h : ∀ (n : ℕ), iterate f (f a) n = map f (iterate f a) n
⊢ iterate f (f a) = map f (iterate f a)

Tactic:
funext n
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
⊢ iterate f (f a) 0 = map f (iterate f a) 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
h : f (iterate f (f a) n) = f (iterate f a (n + 1))
⊢ iterate f (f a) (n + 1) = map f (iterate f a) (n + 1)

Tactic:
unfold map iterate get

Premises used: Stream'.iterate, Stream'.get, Stream'.map
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ iterate f (f a) n = f (iterate f a n)

Tactic:
rw [map, get] at ih

Premises used: Stream'.get, Stream'.map
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
h : f (iterate f (f a) n) = f (f (iterate f a n))
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))

Tactic:
rw [iterate]

Premises used: Stream'.iterate
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (f (iterate f a n))

Tactic:
congrArg f ih

Premises used: congrArg
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (f (iterate f a n))

Tactic:
exact congrArg f ih

Premises used: congrArg
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
h : iterate f (f a) 0 = map f (iterate f a) 0
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)
⊢ iterate f (f a) n = map f (iterate f a) n

Tactic:
induction n with
  | zero => rfl
  | succ n ih =>
    unfold map iterate get
    rw [map, get] at ih
    rw [iterate]
    exact congrArg f ih

Premises used: Stream'.iterate, Stream'.get, Stream'.map, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ corec f g a = map f (iterate g a)

Tactic:
rfl

Premises used: Stream'.corec, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
rw : f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
⊢ corec f g a = f a :: corec f g (g a)

Tactic:
rw [corec_def, map_eq, head_iterate, tail_iterate]

Premises used: Stream'.corec_def, Stream'.tail_iterate, Stream'.head_iterate, Stream'.map_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
rw : map id (iterate id a) = const a
rw₁ : iterate id a = const a
rw₂ rw₃ : const a = const a
⊢ corec id id a = const a

Tactic:
rw [corec_def, map_id, iterate_id]

Premises used: Stream'.corec_def, Stream'.iterate_id, Stream'.map_id
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
⊢ corec id f a = iterate f a

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, Stream'.corec, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β × α
a : α
⊢ corec' f a = (f a).fst :: corec' f (f a).snd

Tactic:
corec_eq _ _ _

Premises used: Stream'.corec_eq, Stream'.corec'
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
rw rw₁ : g a :: corec g f (f a) = g a :: corec g f (f a)
⊢ corec g f a = g a :: corec g f (f a)

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ (unfolds head tail s).get 0 = s.get 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
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
succ₄ succ₅ : s.tail.get n = s.tail.get n
⊢ (unfolds head tail s).get (n + 1) = s.get (n + 1)

Tactic:
rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]

Premises used: Stream'.get_succ, Stream'.unfolds_eq, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), (unfolds head tail s).get 0 = s.get 0
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)
⊢ (unfolds head tail s).get n = s.get n

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]

Premises used: Stream'.get_succ, Nat.zero, Stream'.unfolds_eq, Nat.succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
⊢ ∀ (s : Stream' α), unfolds head tail s = s

Tactic:
fun s =>
  Stream'.ext fun n => get_unfolds_head_tail n s

Premises used: Stream'.get_unfolds_head_tail, Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
change : s₁ ⋈ s₂ = s₁.head :: s₂.head :: t
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
change s₁ ⋈ s₂ = head s₁::head s₂::t

Premises used: Stream'.head
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
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
⊢ 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

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
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
⊢ 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

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ 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:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
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' α)
⊢ 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))

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
⊢ 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:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
rw : s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail
⊢ s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail

Tactic:
rw [interleave_eq s₁ s₂]

Premises used: Stream'.interleave_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
change : (s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ
⊢ (s₁ ⋈ s₂).get (2 * (n + 1)) = s₁.get (n + 1)

Tactic:
change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n)

Premises used: Stream'.interleave, HMul.hMul, Stream'.get, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
rw : (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ
⊢ (s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ

Tactic:
rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons]

Premises used: Stream'.get_succ, Stream'.interleave_eq, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
rw : s₁.tail.get n = s₁.get n.succ
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ

Tactic:
rw [get_interleave_left n (tail s₁) (tail s₂)]

Premises used: Stream'.tail
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₁.tail.get n = s₁.get n.succ

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
change : (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ
⊢ (s₁ ⋈ s₂).get (2 * (n + 1) + 1) = s₂.get (n + 1)

Tactic:
change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n)

Premises used: Stream'.interleave, HMul.hMul, Stream'.get, HAdd.hAdd, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
rw : s₂.tail.get n = s₂.get n.succ
⊢ (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ

Tactic:
rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons,
      get_interleave_right n (tail s₁) (tail s₂)]

Premises used: Stream'.get_succ, Stream'.interleave_eq, Stream'.tail, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₂.tail.get n = s₂.get n.succ

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
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)
rw₁ rw₂ : s₁.get n = s₁.get n
⊢ a = (s₁ ⋈ s₂).get (2 * n)

Tactic:
rw [h, get_interleave_left]

Premises used: Stream'.get_interleave_left
-- Module: Mathlib.Data.Stream.Init
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)
rw₁ rw₂ : s₂.get n = s₂.get n
⊢ a = (s₁ ⋈ s₂).get (2 * n + 1)

Tactic:
rw [h, get_interleave_right]

Premises used: Stream'.get_interleave_right
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.odd = s.tail.even

Tactic:
rfl

Premises used: rfl, Stream'.odd
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.even.head = s.head

Tactic:
rfl

Premises used: Stream'.even, Stream'.iterate, Stream'.get, Stream'.map, Stream'.corec, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
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
⊢ (corec head (fun (s : Stream' α) ↦ s.tail.tail) s).tail = corec head (fun (s : Stream' α) ↦ s.tail.tail) s.tail.tail

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ (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:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a₁ a₂ : α
s : Stream' α
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
⊢ corec head (fun (s : Stream' α) ↦ s.tail.tail) (a₁ :: a₂ :: s) =
    a₁ :: corec head (fun (s : Stream' α) ↦ s.tail.tail) s

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (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:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.tail.even = s.odd

Tactic:
rfl

Premises used: rfl, Stream'.odd
-- Module: Mathlib.Data.Stream.Init
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₁ ⋈ s₂).even.head = s₁.head ∧
    (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
⊢ s₁'.head = s₁.head ∧ (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) s₁'.tail s₁.tail

Tactic:
rw [h₁]
-- Module: Mathlib.Data.Stream.Init
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
right : (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧
    (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
constructor
-- Module: Mathlib.Data.Stream.Init
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

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
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
rw₂ rw₃ : (s₁.tail ⋈ s₂.tail).even = (s₁.tail ⋈ s₂.tail).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even

Tactic:
rw [interleave_eq, even_cons_cons, tail_cons]

Premises used: Stream'.even_cons_cons, Stream'.interleave_eq, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
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
⊢ (fun (s₁' s₁ : Stream' α) ↦ ∃ (s₂ : Stream' α), s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
rw : (s.even ⋈ s.odd).head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
⊢ s'.head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) s'.tail s.tail

Tactic:
rw [h]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
left : (s.even ⋈ s.odd).head = s.head
right : (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
constructor
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (fun (s' s : Stream' α) ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
simp [odd_eq, odd_eq, tail_interleave, tail_even]

Premises used: Stream'.odd_eq, Stream'.tail_even, Stream'.tail_interleave
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
change : s.even.get n.succ = s.get (2 * n).succ.succ
⊢ s.even.get n.succ = s.get (2 * n.succ)

Tactic:
change get (even s) (succ n) = get s (succ (succ (2 * n)))

Premises used: HMul.hMul, Stream'.even, Stream'.get, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
rw : s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)
⊢ s.even.get n.succ = s.get (2 * n).succ.succ

Tactic:
rw [get_succ, get_succ, tail_even, get_even n]

Premises used: Stream'.get_succ, Stream'.tail_even
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
rw : s.tail.get (2 * n) = s.get (2 * n + 1)
⊢ s.odd.get n = s.get (2 * n + 1)

Tactic:
rw [odd_eq, get_even]

Premises used: Stream'.odd_eq, Stream'.get_even
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
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)
rw₁ rw₂ : s.get (2 * n) = s.get (2 * n)
⊢ a = s.get (2 * n)

Tactic:
rw [h, get_even]

Premises used: Stream'.get_even
-- Module: Mathlib.Data.Stream.Init
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)
rw₁ rw₂ : s.get (2 * n + 1) = s.get (2 * n + 1)
⊢ a = s.get (2 * n + 1)

Tactic:
rw [h, get_odd]

Premises used: Stream'.get_odd
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ [] ++ₛ s = s

Tactic:
rfl

Premises used: Stream'.appendStream', rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
s : Stream' α
⊢ a :: l ++ₛ s = a :: (l ++ₛ s)

Tactic:
rfl

Premises used: Stream'.appendStream', rfl
-- Module: Mathlib.Data.Stream.Init
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))
rw₃ rw₄ : a :: (l₁ ++ₛ (l₂ ++ₛ s)) = a :: (l₁ ++ₛ (l₂ ++ₛ s))
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]

Premises used: Stream'.cons_append_stream, List.cons_append
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : Stream' α
n : ℕ
h : n < List.length.{u} (α := α) []
⊢ ([] ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n h

Tactic:
simp at 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 < (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
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
⊢ (b :: x ++ₛ a).get n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (b :: x) n h

Tactic:
rcases n with (_ | n)