awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al)
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b

Tactic:
⟨a, om, h'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al)
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b

Tactic:
exact ⟨a, om, h'⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
h : b ∈ map f s
⊢ ∃ a ∈ s, f a = b

Tactic:
match s with
  | ⟨g, al⟩ =>
    let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
    rcases o with - | a
    · injection oe
    · injection oe with h'; exact ⟨a, om, h'⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : Seq α
eq_of_bisim :
  IsBisimulation.{v} (α := β) fun (s1 s2 : Seq β) ↦
    ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
⊢ map f (s.append t) = (map f s).append (map f t)

Tactic:
apply
    eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
      ⟨s, t, rfl, rfl⟩

Premises used: Stream'.Seq.eq_of_bisim, Exists, Stream'.Seq.map, And, And.intro, Exists.intro, Stream'.Seq.append, Eq, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
s t : Seq α
nil :
  BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (append Seq.nil t)).destruct ((map f Seq.nil).append (map f t)).destruct
cons :
  ∀ (x : α) (s : Seq α),
    BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
      (map f ((Seq.cons x s).append t)).destruct ((map f (Seq.cons x s)).append (map f t)).destruct
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (s.append t)).destruct ((map f s).append (map f t)).destruct

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
simp :
  match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f t).destruct, (map f t).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
  | x, x_1 => False
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (append nil t)).destruct ((map f nil).append (map f t)).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
x : α
s_1 : Seq α
cons :
  ∃ (s : Seq α) (t_2 : Seq α),
    map f (s_1.append t) = map f (s.append t_2) ∧ (map f s_1).append (map f t) = (map f s).append (map f t_2)
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f ((Seq.cons x s_1).append t)).destruct ((map f (Seq.cons x s_1)).append (map f t)).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
nil :
  match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f Seq.nil).destruct, (map f Seq.nil).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
  | x, x_1 => False
cons :
  ∀ (x : α) (s : Seq α),
    match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f (Seq.cons x s)).destruct,
      (map f (Seq.cons x s)).destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
    | x, x_1 => False
⊢ match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f t).destruct, (map f t).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
  | x, x_1 => False

Tactic:
cases t
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
⊢ match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f nil).destruct, (map f nil).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
x : α
s_1 : Seq α
cons : ∃ (s : Seq α) (t : Seq α), map f s_1 = map f (s.append t) ∧ map f s_1 = (map f s).append (map f t)
⊢ match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f (Seq.cons x s_1)).destruct,
    (map f (Seq.cons x s_1)).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_2 : Seq α) (t : Seq α), s = map f (s_2.append t) ∧ s' = (map f s_2).append (map f t)
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
x : α
t : Seq α
⊢ ∃ (s : Seq α) (t_2 : Seq α), map f t = map f (s.append t_2) ∧ map f t = (map f s).append (map f t_2)

Tactic:
⟨nil, t, ?_, ?_⟩

Premises used: Stream'.Seq.nil, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
x : α
t : Seq α
refine_1 : map f t = map f (append nil t)
refine_2 : map f t = (map f nil).append (map f t)
⊢ ∃ (s : Seq α) (t_2 : Seq α), map f t = map f (s.append t_2) ∧ map f t = (map f s).append (map f t_2)

Tactic:
refine ⟨nil, t, ?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
x : α
t : Seq α
⊢ map f t = map f (append nil t)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
x : α
t : Seq α
⊢ map f t = (map f nil).append (map f t)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
⊢ match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f t).destruct, (map f t).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
  | x, x_1 => False

Tactic:
case nil =>
        cases t <;> simp
        case cons _ t => refine ⟨nil, t, ?_, ?_⟩ <;> simp

Premises used: Stream'.Seq.nil, Stream'.Seq.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
x : α
s : Seq α
⊢ ∃ (s_2 : Seq α) (t_2 : Seq α),
    map f (s.append t) = map f (s_2.append t_2) ∧ (map f s).append (map f t) = (map f s_2).append (map f t_2)

Tactic:
⟨s, t, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
x : α
s : Seq α
⊢ ∃ (s_2 : Seq α) (t_2 : Seq α),
    map f (s.append t) = map f (s_2.append t_2) ∧ (map f s).append (map f t) = (map f s_2).append (map f t_2)

Tactic:
exact ⟨s, t, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    s1.destruct s2.destruct

Tactic:
exact
    match s1, s2, h with
    | _, _, ⟨s, t, rfl, rfl⟩ => by
      cases s <;> simp
      case nil =>
        cases t <;> simp
        case cons _ t => refine ⟨nil, t, ?_, ?_⟩ <;> simp
      case cons _ s => exact ⟨s, t, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Seq α) (join nil) nil

Tactic:
destruct_eq_none rfl

Premises used: Stream'.Seq.destruct_eq_none, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
S : Seq (Seq1 α)
⊢ (cons (a, nil) S).join.destruct = some (a, S.join)

Tactic:
simp [join]

Premises used: Stream'.Seq.join
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (cons (a, cons b s) S).join.destruct = some (a, (cons (b, s) S).join)

Tactic:
simp [join]

Premises used: Stream'.Seq.join
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 :
  IsBisimulation.{u} (α := α) fun (s1 s2 : Seq α) ↦
    s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ (cons (a, s) S).join = cons a (s.append S.join)

Tactic:
apply
    eq_of_bisim
      (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
      _ (Or.inr ⟨a, s, S, rfl, rfl⟩)

Premises used: Stream'.Seq.eq_of_bisim, Exists, Prod.mk, Stream'.Seq.join, And, And.intro, Stream'.Seq.cons, Exists.intro, Stream'.Seq.append, Or, Eq, Or.inr, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s_1 : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h :
  s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join)
s : Seq α
nil :
  BisimO.{u} (α := α)
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨
        ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
    (destruct Seq.nil) (destruct Seq.nil)
cons :
  ∀ (x : α) (s : Seq α),
    BisimO
      (fun (s1 s2 : Seq α) ↦
        s1 = s2 ∨
          ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
      (Seq.cons x s).destruct (Seq.cons x s).destruct
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨
        ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
    s.destruct s.destruct

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO.{u} (α := α)
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (destruct nil) (destruct nil)

Tactic:
trivial
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h :
  s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join)
x : α
s_1 : Seq α
cons :
  BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨
        ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
    (some (x, s_1)) (some (x, s_1))
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨
        ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
    (Seq.cons x s_1).destruct (Seq.cons x s_1).destruct

Tactic:
rw [destruct_cons]

Premises used: Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x : α
s_1 : Seq α
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (some (x, s_1)) (some (x, s_1))

Tactic:
⟨rfl, Or.inl rfl⟩

Premises used: And.intro, Or.inl, Stream'.Seq.BisimO, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x : α
s_1 : Seq α
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (some (x, s_1)) (some (x, s_1))

Tactic:
exact ⟨rfl, Or.inl rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a_1 : α
s_1 : Seq α
S_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join)
a : α
s : Seq α
S : Seq (Seq1 α)
nil :
  BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨
        ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
    (Seq.cons (a, Seq.nil) S).join.destruct (Seq.cons a (append Seq.nil S.join)).destruct
cons :
  ∀ (x : α) (s : Seq α),
    BisimO
      (fun (s1 s2 : Seq α) ↦
        s1 = s2 ∨
          ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
      (Seq.cons (a, Seq.cons x s) S).join.destruct (Seq.cons a ((Seq.cons x s).append S.join)).destruct
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨
        ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (Seq.cons (a, s) S).join ∧ s2 = Seq.cons a (s.append S.join))
    (Seq.cons (a, s) S).join.destruct (Seq.cons a (s.append S.join)).destruct

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a_1 : α
s : Seq α
S_1 : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, nil) S).join.destruct (cons a (append nil S.join)).destruct

Tactic:
simp [join_cons_nil]

Premises used: Stream'.Seq.join_cons_nil
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a_1 : α
s : Seq α
S_1 : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x : α
s_1 : Seq α
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, cons x s_1) S).join.destruct (cons a ((cons x s_1).append S.join)).destruct

Tactic:
simpa only [BisimO, join_cons_cons, destruct_cons, cons_append, true_and] using
          Or.inr ⟨_, _, S, rfl, rfl⟩

Premises used: Stream'.Seq.join_cons_cons, Stream'.Seq.destruct_cons, Stream'.Seq.cons_append, Stream'.Seq.BisimO, Or.inr, true_and
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      s1 = s2 ∨ ∃ (a : α) (s : Seq α) (S : Seq (Seq1 α)), s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    s1.destruct s2.destruct

Tactic:
exact
    match s1, s2, h with
    | s, _, Or.inl <| Eq.refl s => by
      cases s; · trivial
      · rw [destruct_cons]
        exact ⟨rfl, Or.inl rfl⟩
    | _, _, Or.inr ⟨a, s, S, rfl, rfl⟩ => by
      cases s
      · simp [join_cons_nil]
      · simpa only [BisimO, join_cons_cons, destruct_cons, cons_append, true_and] using
          Or.inr ⟨_, _, S, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
bisim :
  IsBisimulation.{u} (α := α) fun (s1 s2 : Seq α) ↦
    ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
      s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
r :
  ∃ (s : Seq α) (S_1 : Seq (Seq1 α)) (T_1 : Seq (Seq1 α)),
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)
⊢ (S.append T).join = S.join.append T.join

Tactic:
apply
    eq_of_bisim fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))

Premises used: Stream'.Seq.eq_of_bisim, Exists, Stream'.Seq.join, And, Stream'.Seq.append, Eq
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : Seq α
S T : Seq (Seq1 α)
nil :
  BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (append Seq.nil (S.append T).join).destruct (append Seq.nil (S.join.append T.join)).destruct
cons :
  ∀ (x : α) (s : Seq α),
    BisimO
      (fun (s1 s2 : Seq α) ↦
        ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
          s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
      ((Seq.cons x s).append (S.append T).join).destruct ((Seq.cons x s).append (S.join.append T.join)).destruct
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (s.append (S.append T).join).destruct (s.append (S.join.append T.join)).destruct

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
simp :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (S.append T).join.destruct,
    (S.join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (append nil (S.append T).join).destruct (append nil (S.join.append T.join)).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
x : α
s : Seq α
cons :
  ∃ (s_1 : Seq α) (S_2 : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append (S.append T).join = s_1.append (S_2.append T_2).join ∧
      s.append (S.join.append T.join) = s_1.append (S_2.join.append T_2.join)
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    ((Seq.cons x s).append (S.append T).join).destruct ((Seq.cons x s).append (S.join.append T.join)).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
nil :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (append Seq.nil T).join.destruct,
    (append (join Seq.nil) T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False
cons :
  ∀ (x : Seq1 α) (s : Seq (Seq1 α)),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) ((Seq.cons x s).append T).join.destruct,
      ((Seq.cons x s).join.append T.join).destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
          s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (S.append T).join.destruct,
    (S.join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
cases S
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
simp :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) T.join.destruct, T.join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (append nil T).join.destruct,
    (append (join nil) T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
x : Seq1 α
s : Seq (Seq1 α)
cons :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons x (s.append T)).join.destruct,
    ((Seq.cons x s).join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) ((Seq.cons x s).append T).join.destruct,
    ((Seq.cons x s).join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) destruct (join nil), destruct (join nil) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
simp