awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) none with
        | none => (none, none)
        | some (a, b') => (some a, some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) none with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
s : α × β
h : f b = Option.some s
some :
  ∀ (a : α) (b' : β) (h : f b = Option.some (a, b')),
    Eq.{u + 1} (α := Option (Seq1 α))
      (Option.map
        (fun (a' : α) ↦
          (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)))
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) Option.some (a, b') with
          | none => (none, none)
          | Option.some (a, b') => (Option.some a, Option.some b'))))
      (match (motive := Option (α × β) → Option (α × Seq α)) Option.some (a, b') with
      | none => none
      | Option.some (a, b) =>
        Option.some
          (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯))
⊢ Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) Option.some s with
        | none => (none, none)
        | Option.some (a, b') => (Option.some a, Option.some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) Option.some s with
    | none => none
    | Option.some (a, b) =>
      Option.some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯))

Tactic:
obtain ⟨a, b'⟩ := s
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = Option.some (a, b')
some :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b')) ⋯
⊢ Option.some
      (a, tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)) =
    Option.some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b')) ⋯)

Tactic:
apply congr_arg fun b' => some (a, b')

Premises used: Option.some, Prod.mk, congr_arg
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = Option.some (a, b')
some :
  (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)) :
      Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b')) ⋯) :
      Stream' (Option α))
⊢ tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b')) ⋯

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = Option.some (a, b')
some : corec' (Corec.f f) (Corec.f f (Option.some b)).snd = corec' (Corec.f f) (Option.some b')
⊢ (corec' (Corec.f f) (Option.some b)).tail = corec' (Corec.f f) (Option.some b')

Tactic:
rw [Stream'.corec'_eq, Stream'.tail_cons]

Premises used: Stream'.corec'_eq, Stream'.tail_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = Option.some (a, b')
some :
  corec' (Corec.f f)
      (Prod.snd.{u, v} (α := Option α)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | Option.some (a, b') => (Option.some a, Option.some b'))) =
    corec' (Corec.f f) (Option.some b')
⊢ corec' (Corec.f f) (Corec.f f (Option.some b)).snd = corec' (Corec.f f) (Option.some b')

Tactic:
dsimp [Corec.f]

Premises used: Stream'.Seq.Corec.f
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = Option.some (a, b')
some some₁ :
  corec' (Corec.f f)
      (Prod.snd.{u, v} (α := Option α)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) Option.some (a, b') with
        | none => (none, none)
        | Option.some (a, b') => (Option.some a, Option.some b'))) =
    corec' (Corec.f f) (Option.some b')
⊢ corec' (Corec.f f)
      (Prod.snd.{u, v} (α := Option α)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | Option.some (a, b') => (Option.some a, Option.some b'))) =
    corec' (Corec.f f) (Option.some b')

Tactic:
rw [h]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
a : (corec f b).destruct = none
⊢ corec f b = nil

Tactic:
apply destruct_eq_none

Premises used: Stream'.Seq.destruct_eq_none
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ (corec f b).destruct = none

Tactic:
simp [h]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
x : α
s : β
h : f b = some (x, s)
a : (corec f b).destruct = some (x, corec f s)
⊢ corec f b = cons x (corec f s)

Tactic:
apply destruct_eq_cons

Premises used: Stream'.Seq.destruct_eq_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
x : α
s : β
h : f b = some (x, s)
⊢ (corec f b).destruct = some (x, corec f s)

Tactic:
simp [h]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
a : (↑s₁ : Stream' (Option α)) = (↑s₂ : Stream' (Option α))
⊢ s₁ = s₂

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
a :
  Stream'.IsBisimulation.{u} (α := Option α) fun (x y : Stream' (Option α)) ↦
    ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = x ∧ (↑s' : Stream' (Option α)) = y ∧ R s s'
a₁ :
  ∃ (s : Seq α),
    ∃ (s' : Seq α),
      (↑s : Stream' (Option α)) = (↑s₁ : Stream' (Option α)) ∧
        (↑s' : Stream' (Option α)) = (↑s₂ : Stream' (Option α)) ∧ R s s'
⊢ (↑s₁ : Stream' (Option α)) = (↑s₂ : Stream' (Option α))

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

Premises used: Exists, And, Stream'.eq_of_bisim, Subtype.val, Eq
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
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 : val.IsSeq)
    (r : R (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) s')
    (this :
      head (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) = s'.head ∧
        R (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) s'.tail)
    (r : R (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) s'.tail),
    (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) =
      (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)).tail
⊢ (↑s.tail : Stream' (Option α)) = (↑s : Stream' (Option α)).tail

Tactic:
cases s using Subtype.recOn
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
val : Stream' (Option α)
property : val.IsSeq
r_2 : R (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) s'
this :
  head (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) = s'.head ∧
    R (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) s'.tail
r : R (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) s'.tail
⊢ (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)).tail

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
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 : val.IsSeq)
    (r : R s (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property))
    (this :
      s.head = head (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) ∧
        R s.tail (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)))
    (r : R s.tail (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property))),
    (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) =
      (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)).tail
⊢ (↑s'.tail : Stream' (Option α)) = (↑s' : Stream' (Option α)).tail

Tactic:
cases s' using Subtype.recOn
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s : Seq α
val : Stream' (Option α)
property : val.IsSeq
r_2 : R s (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)
this :
  s.head = head (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) ∧
    R s.tail (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property))
r : R s.tail (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property))
⊢ (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)).tail

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
suffices : s.head = s'.head ∧ R s.tail s'.tail
⊢ (↑s : Stream' (Option α)).head = (↑s' : Stream' (Option α)).head ∧
    ∃ (s_1 : Seq α),
      ∃ (s'_1 : Seq α),
        (↑s_1 : Stream' (Option α)) = (↑s : Stream' (Option α)).tail ∧
          (↑s'_1 : Stream' (Option α)) = (↑s' : Stream' (Option α)).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 using Subtype.recOn; rfl,
          by cases s' using Subtype.recOn; rfl, r⟩) this
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
⊢ BisimO R s.destruct s'.destruct

Tactic:
have := bisim r
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
this : BisimO R s.destruct s'.destruct
revert : ∀ (r : R s s') (this : 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 this
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
nil :
  ∀ (r : R Seq.nil s') (this : BisimO R (destruct Seq.nil) s'.destruct),
    head Seq.nil = s'.head ∧ R (tail Seq.nil) s'.tail
cons :
  ∀ (x : α) (s : Seq α) (r : R (Seq.cons x s) s') (this : BisimO R (Seq.cons x s).destruct s'.destruct),
    (Seq.cons x s).head = s'.head ∧ R (Seq.cons x s).tail s'.tail
⊢ ∀ (r : R s s') (this : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
nil :
  ∀ (r : R Seq.nil Seq.nil) (this : BisimO R (destruct Seq.nil) (destruct Seq.nil)),
    Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil) ∧ R (tail Seq.nil) (tail Seq.nil)
nil₁ :
  ∀ (x : α) (s : Seq α) (r : R Seq.nil (cons x s)) (this : BisimO R (destruct Seq.nil) (cons x s).destruct),
    head Seq.nil = (cons x s).head ∧ R (tail Seq.nil) (cons x s).tail
⊢ ∀ (r : R Seq.nil s') (this : BisimO R (destruct Seq.nil) s'.destruct),
    head Seq.nil = s'.head ∧ R (tail Seq.nil) s'.tail

Tactic:
cases s'
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
x : α
s : Seq α
cons :
  ∀ (r : R (Seq.cons x s) nil) (this : BisimO R (Seq.cons x s).destruct (destruct nil)),
    (Seq.cons x s).head = head nil ∧ R (Seq.cons x s).tail (tail nil)
cons₁ :
  ∀ (x_1 : α) (s_1 : Seq α) (r : R (Seq.cons x s) (Seq.cons x_1 s_1))
    (this : BisimO R (Seq.cons x s).destruct (Seq.cons x_1 s_1).destruct),
    (Seq.cons x s).head = (Seq.cons x_1 s_1).head ∧ R (Seq.cons x s).tail (Seq.cons x_1 s_1).tail
⊢ ∀ (r : R (Seq.cons x s) s') (this : BisimO R (Seq.cons x s).destruct s'.destruct),
    (Seq.cons x s).head = s'.head ∧ R (Seq.cons x s).tail s'.tail

Tactic:
cases s'
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
r : R Seq.nil Seq.nil
nil :
  BisimO R (destruct Seq.nil) (destruct Seq.nil) →
    Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil) ∧ R (tail Seq.nil) (tail Seq.nil)
⊢ ∀ (this : BisimO R (destruct Seq.nil) (destruct Seq.nil)),
    Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil) ∧ R (tail Seq.nil) (tail Seq.nil)

Tactic:
_
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
r : R Seq.nil Seq.nil
this : BisimO R (destruct Seq.nil) (destruct Seq.nil)
nil : Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil)
nil₁ : R (tail Seq.nil) (tail Seq.nil)
⊢ Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil) ∧ R (tail Seq.nil) (tail Seq.nil)

Tactic:
constructor
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
r : R nil nil
this : BisimO R (destruct nil) (destruct nil)
⊢ Eq.{u + 1} (α := Option α) (head nil) (head nil)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
r : R nil nil
this : BisimO R (destruct nil) (destruct nil)
⊢ R (tail nil) (tail nil)

Tactic:
assumption
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R nil (cons x s)
this : BisimO R (destruct nil) (cons x s).destruct
⊢ BisimO R none (some (x, s))

Tactic:
rw [destruct_nil, destruct_cons] at this

Premises used: Stream'.Seq.destruct_nil, Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R nil (cons x s)
this : BisimO R none (some (x, s))
⊢ head nil = (cons x s).head ∧ R (tail nil) (cons x s).tail

Tactic:
False.elim this

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R nil (cons x s)
this : BisimO R none (some (x, s))
⊢ head nil = (cons x s).head ∧ R (tail nil) (cons x s).tail

Tactic:
exact False.elim this

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R (cons x s) nil
this : BisimO R (cons x s).destruct (destruct nil)
⊢ BisimO R (some (x, s)) none

Tactic:
rw [destruct_nil, destruct_cons] at this

Premises used: Stream'.Seq.destruct_nil, Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R (cons x s) nil
this : BisimO R (some (x, s)) none
⊢ (cons x s).head = head nil ∧ R (cons x s).tail (tail nil)

Tactic:
False.elim this

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R (cons x s) nil
this : BisimO R (some (x, s)) none
⊢ (cons x s).head = head nil ∧ R (cons x s).tail (tail nil)

Tactic:
exact False.elim this

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
x_1 : α
s_1 : Seq α
⊢ ∀ (r : R (cons x s) (cons x_1 s_1)) (this : BisimO R (cons x s).destruct (cons x_1 s_1).destruct),
    (cons x s).head = (cons x_1 s_1).head ∧ R (cons x s).tail (cons x_1 s_1).tail

Tactic:
simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
⊢ t₁.head = t₂.head ∧
    ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁.tail ∧ (↑s' : Stream' (Option α)) = t₂.tail ∧ R s s'

Tactic:
exact
    match t₁, t₂, e with
    | _, _, ⟨s, s', rfl, rfl, r⟩ => by
      suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
          by cases s' using Subtype.recOn; rfl, r⟩) this
      have := bisim r; revert r this
      cases s <;> cases s'
      · intro r _
        constructor
        · rfl
        · assumption
      · intro _ this
        rw [destruct_nil, destruct_cons] at this
        exact False.elim this
      · intro _ this
        rw [destruct_nil, destruct_cons] at this
        exact False.elim this
      · simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ (s : Seq α),
    ∃ (s' : Seq α),
      (↑s : Stream' (Option α)) = (↑s₁ : Stream' (Option α)) ∧
        (↑s' : Stream' (Option α)) = (↑s₂ : Stream' (Option α)) ∧ R s s'

Tactic:
⟨s₁, s₂, rfl, rfl, r⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ (s : Seq α),
    ∃ (s' : Seq α),
      (↑s : Stream' (Option α)) = (↑s₁ : Stream' (Option α)) ∧
        (↑s' : Stream' (Option α)) = (↑s₂ : Stream' (Option α)) ∧ R s s'

Tactic:
exact ⟨s₁, s₂, rfl, rfl, r⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
apply : IsBisimulation motive
⊢ s₁ = s₂

Tactic:
apply eq_of_bisim motive _ base

Premises used: Stream'.Seq.eq_of_bisim
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
inl : ∀ (h_nil₁ : s₁ = nil) (h_nil₂ : s₂ = nil), BisimO motive s₁.destruct s₂.destruct
inr :
  ∀ (w : α) (w_1 w_2 : Seq α) (h₁ : s₁ = cons w w_1) (h₂ : s₂ = cons w w_2),
    motive w_1 w_2 → BisimO motive s₁.destruct s₂.destruct
⊢ BisimO motive s₁.destruct s₂.destruct

Tactic:
rcases step s₁ s₂ h with ⟨h_nil₁, h_nil₂⟩ | ⟨_, _, _, h₁, h₂, _⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
h_nil₁ : s₁ = nil
h_nil₂ : s₂ = nil
⊢ BisimO motive s₁.destruct s₂.destruct

Tactic:
simp [h_nil₁, h_nil₂]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
w : α
w_1 w_2 : Seq α
h₁ : s₁ = cons w w_1
h₂ : s₂ = cons w w_2
right : motive w_1 w_2
⊢ BisimO motive s₁.destruct s₂.destruct

Tactic:
simpa [h₁, h₂]