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 (pure r') (pure a) →
      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' : α
⊢ ∀ (s : Computation α),
    R (pure r') s.think →
      BisimO R (pure r').destruct s.think.destruct → (pure r').head = s.think.head ∧ R (pure r').tail s.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'.think (pure a) →
      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' : Computation α
⊢ ∀ (s : Computation α),
    R r'.think s.think →
      BisimO R r'.think.destruct s.think.destruct → r'.think.head = s.think.head ∧ R r'.think.tail s.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 (pure r') (pure a) →
      BisimO R (pure r').destruct (pure a).destruct → (pure r').head = (pure a).head ∧ R (pure r').tail (pure a).tail

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' : α
⊢ ∀ (s : Computation α),
    R (pure r') s.think →
      BisimO R (pure r').destruct s.think.destruct → (pure r').head = s.think.head ∧ R (pure r').tail s.think.tail

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

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' : Computation α
⊢ ∀ (s : Computation α),
    R r'.think s.think →
      BisimO R r'.think.destruct s.think.destruct → r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail