awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
a :
  Stream'.IsBisimulation.{u} (α := Option α) fun (x y : Stream' (Option α)) ↦
    ∃ (s : Computation α),
      ∃ (s' : Computation α),
        s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = x ∧
          s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = y ∧ R s s'
a₁ :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
          s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
            s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) ∧
          R s s'
⊢ s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)

Tactic:
apply Stream'.eq_of_bisim fun x y => ∃ s s' : Computation α, s.1 = x ∧ s'.1 = y ∧ R s s'

Premises used: Exists, And, Stream'.eq_of_bisim, Subtype.val, Eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r_2 : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
mk :
  ∀ (val : Stream' (Option α)) (property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a)
    (r :
      R
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property)
        s')
    (this :
      head
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
              property) =
          s'.head ∧
        R
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
              property))
          s'.tail)
    (r :
      R
        (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property))
        s'.tail),
    (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
              property)).val
        (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
      (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)).tail
⊢ s.tail.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s' : Computation α
val : Stream' (Option α)
property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a
r_2 :
  R (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val property)
    s'
this :
  head
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property) =
      s'.head ∧
    R
      (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property))
      s'.tail
r :
  R
    (tail
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
        property))
    s'.tail
⊢ (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)).val
      (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property)).tail

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r_2 : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
mk :
  ∀ (val : Stream' (Option α)) (property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a)
    (r :
      R s
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property))
    (this :
      s.head =
          head
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
              property) ∧
        R s.tail
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
              property)))
    (r :
      R s.tail
        (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property))),
    (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
              property)).val
        (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
      (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)).tail
⊢ s'.tail.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail

Tactic:
cases s'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s : Computation α
val : Stream' (Option α)
property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a
r_2 :
  R s
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val property)
this :
  s.head =
      head
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property) ∧
    R s.tail
      (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property))
r :
  R s.tail
    (tail
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
        property))
⊢ (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)).val
      (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property)).tail

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
suffices : s.head = s'.head ∧ R s.tail s'.tail
⊢ s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).head =
      s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).head ∧
    ∃ (s_1 : Computation α),
      ∃ (s'_1 : Computation α),
        s_1.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
            s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail ∧
          s'_1.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
              s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail ∧
            R s_1 s'_1

Tactic:
suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ BisimO R s.destruct s'.destruct

Tactic:
have h := bisim r
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
h : BisimO R s.destruct s'.destruct
revert : ∀ (r : R s s') (h : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
⊢ s.head = s'.head ∧ R s.tail s'.tail

Tactic:
revert r h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
⊢ ∀ (r : R s s') (h : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail

Tactic:
recOn s ?_ ?_

Premises used: Computation.recOn
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
refine_1 :
  ∀ (a : α) (r : R (pure a) s') (h : BisimO R (pure a).destruct s'.destruct),
    (pure a).head = s'.head ∧ R (pure a).tail s'.tail
refine_2 :
  ∀ (s : Computation α) (r : R s.think s') (h : BisimO R s.think.destruct s'.destruct),
    s.think.head = s'.head ∧ R s.think.tail s'.tail
⊢ ∀ (r : R s s') (h : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail

Tactic:
refine recOn s ?_ ?_
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' : α
⊢ ∀ (r : R (pure r') s') (h : BisimO R (pure r').destruct s'.destruct),
    (pure r').head = s'.head ∧ R (pure r').tail s'.tail

Tactic:
recOn s' ?_ ?_

Premises used: Computation.recOn
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' : α
refine_1 :
  ∀ (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
refine_1₁ :
  ∀ (s : Computation α) (r : R (pure r') s.think) (h : BisimO R (pure r').destruct s.think.destruct),
    (pure r').head = s.think.head ∧ R (pure r').tail s.think.tail
⊢ ∀ (r : R (pure r') s') (h : BisimO R (pure r').destruct s'.destruct),
    (pure r').head = s'.head ∧ R (pure r').tail s'.tail

Tactic:
refine recOn s' ?_ ?_
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' r' : Computation α
⊢ ∀ (r : R r'.think s') (h : BisimO R r'.think.destruct s'.destruct), r'.think.head = s'.head ∧ R r'.think.tail s'.tail

Tactic:
recOn s' ?_ ?_

Premises used: Computation.recOn
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' r' : Computation α
refine_2 :
  ∀ (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
refine_2₁ :
  ∀ (s : Computation α) (r : R r'.think s.think) (h : BisimO R r'.think.destruct s.think.destruct),
    r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail
⊢ ∀ (r : R r'.think s') (h : BisimO R r'.think.destruct s'.destruct), r'.think.head = s'.head ∧ R r'.think.tail s'.tail

Tactic:
refine recOn s' ?_ ?_
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
refine_1 : (pure r').head = (pure a').head
refine_1₁ : R (pure r').tail (pure a').tail
⊢ (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail

Tactic:
constructor
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
refine_1 refine_1₁ : (pure a').head = (pure a').head
⊢ (pure r').head = (pure a').head

Tactic:
rw [h]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')

Tactic:
rw [h] at r
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
r₁ : R (pure a') (pure a')
⊢ r' = a'

Tactic:
rw [h] at r
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
refine_1 : R (pure a') (pure a')
⊢ R (pure r').tail (pure a').tail

Tactic:
rw [tail_pure, tail_pure, h]

Premises used: Computation.tail_pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')

Tactic:
assumption
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = 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
⊢ BisimO R (Sum.inl r') (Sum.inr a')

Tactic:
rw [destruct_pure, destruct_think] at h

Premises used: Computation.destruct_pure, Computation.destruct_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = 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:
False.elim h

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = 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:
exact False.elim h

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R r'.think (pure a')
h : BisimO R r'.think.destruct (pure a').destruct
⊢ BisimO R (Sum.inr r') (Sum.inl a')

Tactic:
rw [destruct_pure, destruct_think] at h

Premises used: Computation.destruct_pure, Computation.destruct_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = 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:
False.elim h

Premises used: False.elim