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

Goal state before:
pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
·

Goal state after:
case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

pp: case inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
·

Goal state after:
case inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive s

Tactic:
rw [destruct_eq_pure H]
    apply pure

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

Goal state before:
pp: case zero.inl
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val✝ : α
h : (Corec.f f (Sum.inl val✝)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'

pp: case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h : (Corec.f f (Sum.inr b)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'

Tactic:
·

Goal state after:
case zero.inl
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val✝ : α
h : (Corec.f f (Sum.inl val✝)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inr.inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

pp: case inr.inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h✝ : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
·

Goal state after:
case inr.inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inr.inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h✝ : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
·

Goal state after:
case inr.inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h✝ : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Computation

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

pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr 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:
case inl
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inl a) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inl a with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ Stream'.IsBisimulation fun x y ↦ ∃ s s', s.val = x ∧ s'.val = y ∧ R s s'

pp: case a
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', s.val = s₁.val ∧ s'.val = s₂.val ∧ R s s'

Tactic:
·

Goal state after:
case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ Stream'.IsBisimulation fun x y ↦ ∃ s s', s.val = x ∧ s'.val = y ∧ R s s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates

pp: case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
·

Goal state after:
case mp
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
·

Goal state after:
case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil

pp: case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
·

Goal state after:
case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case left
α : 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

pp: case right
α : 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
⊢ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
·

Goal state after:
case left
α : 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
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
·

Goal state after:
case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case right
α : 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
⊢ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
·

Goal state after:
case right
α : 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
⊢ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case left
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head

pp: case right
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
·

Goal state after:
case left
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head
Module: Mathlib.Data.Stream.Init

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

Tactic:
·

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

Goal state before:
pp: case refine_1.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' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
⊢ (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail

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 (pure r').destruct a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

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 r'.think.destruct (pure a').destruct
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

pp: case refine_2.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' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail

Tactic:
·

Goal state after:
case refine_1.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' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
⊢ (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail
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 (s (n + 1)) = none

pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e✝ : α
e : s n = some e✝
a✝ : Option.map f (some e✝) = none
⊢ Option.map f (s (n + 1)) = 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 (s (n + 1)) = none
Module: Mathlib.Data.Seq.Defs

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

Tactic:
·

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e✝ : α
e : s n = some e✝
a✝ : Option.map f (some e✝) = none
⊢ Option.map f (s (n + 1)) = none
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 r').head = (pure a').head

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 r') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail

Tactic:
·

Goal state after:
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 r').head = (pure a').head
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 r') (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 r') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case cons.zero
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
h : 0 < (b :: x).length
⊢ (b :: x ++ₛ a).get 0 = (b :: x)[0]

pp: case cons.succ
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ (b :: x ++ₛ a).get (n + 1) = (b :: x)[n + 1]

Tactic:
·

Goal state after:
case cons.zero
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
h : 0 < (b :: x).length
⊢ (b :: x ++ₛ a).get 0 = (b :: x)[0]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case cons.succ
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ (b :: x ++ₛ a).get (n + 1) = (b :: x)[n + 1]

Tactic:
·

Goal state after:
case cons.succ
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ (b :: x ++ₛ a).get (n + 1) = (b :: x)[n + 1]
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 (pure r').destruct a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

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 r'.think.destruct (pure a').destruct
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

pp: case refine_2.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' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.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 (pure r').destruct a'.think.destruct
⊢ (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 r'.think.destruct (pure a').destruct
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

pp: case refine_2.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' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.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 r'.think.destruct (pure a').destruct
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.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' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail

Tactic:
·

Goal state after:
case refine_2.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' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', s.val = s₁.val ∧ s'.val = s₂.val ∧ R s s'

Tactic:
·

Goal state after:
case a
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', s.val = s₁.val ∧ s'.val = s₂.val ∧ R s s'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
s : Computation α
a : α
h : some a = s.think.val.get 0
⊢ a ∈ s

pp: case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s

Tactic:
·

Goal state after:
case zero
α : Type u
s : Computation α
a : α
h : some a = s.think.val.get 0
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s

Tactic:
·

Goal state after:
case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : s.val n = none
⊢ none = (empty α).val n

pp: case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ some val✝ = (empty α).val n

Tactic:
·

Goal state after:
case none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : s.val n = none
⊢ none = (empty α).val n
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length

Tactic:
·

Goal state after:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length

Tactic:
·

Goal state after:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a.zero
α : Type u
s : Computation α
h : s.Terminates
this : (s.think.val 0).isSome = true
⊢ s.length + 1 ≤ 0

pp: case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1

Tactic:
·

Goal state after:
case a.zero
α : Type u
s : Computation α
h : s.Terminates
this : (s.think.val 0).isSome = true
⊢ s.length + 1 ≤ 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1

Tactic:
·

Goal state after:
case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1
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

pp: case zero.think
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
⊢ s.think = (pure a).thinkN 0

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

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)
⊢ s.think = (pure a).thinkN (n + 1)

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 zero.think
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
⊢ s.think = (pure a).thinkN 0

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

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)
⊢ s.think = (pure a).thinkN (n + 1)

Tactic:
·

Goal state after:
case zero.think
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
⊢ s.think = (pure a).thinkN 0