mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
⊢ Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a'

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
⊢ Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Tactic:
]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t

Tactic:
]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x ↦
            match x with
            | (s₁, snd) => s₁.head)
          (fun x ↦
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x ↦
            match x with
            | (s₁, snd) => s₁.head)
          (fun x ↦
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail

Tactic:
]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ

Tactic:
]

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₁.tail.get n = s₁.get n.succ

Tactic:
]

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₁.tail.get n = s₁.get n.succ
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a' →
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'

Tactic:
]

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a' →
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₂.tail.get n = s₂.get n.succ

Tactic:
]

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

Goal state before:
pp: α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₁
n : ℕ
h : (fun b ↦ a = b) (s₁.get n)
⊢ (fun b ↦ s₁.get n = b) (s₁.get n)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Sum.rec some (fun x ↦ none) (f b) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Sum.rec some (fun x ↦ none) (f b) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₂
n : ℕ
h : (fun b ↦ a = b) (s₂.get n)
⊢ (fun b ↦ s₂.get n = b) (s₂.get n)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ (s.head :: corec head (fun s ↦ s.tail.tail) s.tail.tail).tail = corec head (fun s ↦ s.tail.tail) s.tail.tail

Tactic:
]

Goal state after:
α : Type u
s : Stream' α
⊢ (s.head :: corec head (fun s ↦ s.tail.tail) s.tail.tail).tail = corec head (fun s ↦ s.tail.tail) s.tail.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct

Tactic:
]

Goal state after:
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s ↦ s.tail.tail) s

Tactic:
]

Goal state after:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s ↦ s.tail.tail) s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
]

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (Sum.inr b') = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (corec f b).destruct = rmap (corec f) (f b)

Tactic:
dsimp [corec, destruct]
  rw [show Stream'.corec' (Corec.f f) (Sum.inr b) 0 =
    Sum.rec Option.some (fun _ ↦ none) (f b) by
    dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]
    match (f b) with
    | Sum.inl x => rfl
    | Sum.inr x => rfl]
  rcases h : f b with a | b'; · rfl
  dsimp [Corec.f, destruct]
  apply congr_arg; apply Subtype.ext
  dsimp [corec, tail]
  rw [Stream'.corec'_eq, Stream'.tail_cons]
  dsimp [Corec.f]; rw [h]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
]

Goal state after:
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ none = some a✝ ↔ nil.get? n = some a✝

Tactic:
]

Goal state after:
case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ none = some a✝ ↔ nil.get? n = some a✝
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : ∃ n, some x = (↑s).get n
⊢ ∃ i, some x = s.get? i

Tactic:
]

Goal state after:
α : Type u
s : Seq α
x : α
h : ∃ n, some x = (↑s).get n
⊢ ∃ i, some x = s.get? i
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁.tail ⋈ s₂.tail).even = (s₁.tail ⋈ s₂.tail).even

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' ↦ (a', s.tail)) (some a) = some (a, s.tail)

Tactic:
]

Goal state after:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' ↦ (a', s.tail)) (some a) = some (a, s.tail)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
TH : s = cons a s.tail
⊢ C (cons a s.tail)

Tactic:
]

Goal state after:
case zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
TH : s = cons a s.tail
⊢ C (cons a s.tail)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
]

Goal state after:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Tactic:
]

Goal state after:
case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : l.length ≤ n
⊢ l.length ≤ n + 1

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : l.length ≤ n
⊢ l.length ≤ n + 1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)

Tactic:
]

Goal state after:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
a✝ : Option.map f none = none
⊢ Option.map f none = none

Tactic:
]

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
a✝ : Option.map f none = none
⊢ Option.map f none = none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)

Tactic:
]

Goal state after:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1.left
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ (pure a').head = (pure a').head

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.even
n : ℕ
h : (fun b ↦ a = b) (s.even.get n)
⊢ (fun b ↦ s.get (2 * n) = b) (s.get (2 * n))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail

Tactic:
]

Goal state after:
case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.odd
n : ℕ
h : (fun b ↦ a = b) (s.odd.get n)
⊢ (fun b ↦ s.get (2 * n + 1) = b) (s.get (2 * n + 1))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: (l₁ ++ₛ (l₂ ++ₛ s)) = a :: (l₁ ++ₛ (l₂ ++ₛ s))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')

Tactic:
]

Goal state after:
case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (Sum.inl r') (Sum.inr a')
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

Tactic:
]

Goal state after:
case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (Sum.inl r') (Sum.inr a')
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R r'.think (pure a')
h : BisimO R (Sum.inr r') (Sum.inl a')
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

Tactic:
]

Goal state after:
case refine_2.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R r'.think (pure a')
h : BisimO R (Sum.inr r') (Sum.inl a')
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : 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
⊢ (y ++ₛ b).get i✝ = (y ++ₛ ?a).get i✝

pp: case a
α : 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
⊢ Stream' α

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
⊢ f a :: (List.map f l ++ₛ map f s) = f a :: (List.map f l ++ₛ map f s)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l : List α
s : Stream' α
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ take n.succ s ++ [s.get (n + 1)] = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ [] = []

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s

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

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m : ℕ
⊢ [] = []

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m n : ℕ
⊢ s.head :: take (min n m) s.tail = s.head :: take (min n m) s.tail

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = s.val n
⊢ (some a).isSome = true

Tactic:
]

Goal state after:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = s.val n
⊢ (some a).isSome = true
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ some (s.tail.get k) = some (s.tail.get k)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ take n xs = take n xs

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), take n s ++ₛ drop n s = s
s : Stream' α
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m

Tactic:
]

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a)[m]

pp: case h
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ m < (take n a).length

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s

Tactic:
]

Goal state after:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s

Tactic:
]

Goal state after:
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : 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
⊢ x[i✝] = x[i✝]

pp: case h
α : 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
⊢ i✝ < x.length

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length

Tactic:
]

Goal state after:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ n = n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a

Tactic:
]

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
⊢ n + 1 = n + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n'

Tactic:
]

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a n
⊢ ((pure a).thinkN n).Results a n

Tactic:
]

Goal state after:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a n
⊢ ((pure a).thinkN n).Results a n
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero.pure
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a = (pure a).thinkN 0

Tactic:
]

Goal state after:
case zero.pure
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a = (pure a).thinkN 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ ((pure a).thinkN n).think = (pure a).thinkN (n + 1)

Tactic:
]

Goal state after:
case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ ((pure a).thinkN n).think = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure a).thinkN s.length)

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure a).thinkN s.length)