awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S_1 : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
induction :
  BisimO.{u} (α := Option (α × WSeq α))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (Computation.destruct (destruct (join nil)))
    (Computation.destruct (Computation.bind (destruct nil) destruct_join.aux))
induction₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
      (cons x s).join.destruct.destruct ((cons x s).destruct.bind destruct_join.aux).destruct
think :
  ∀ (s : WSeq (WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
      s.think.join.destruct.destruct (s.think.destruct.bind destruct_join.aux).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    S.join.destruct.destruct (S.destruct.bind destruct_join.aux).destruct

Tactic:
induction S using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
⊢ BisimO.{u} (α := Option (α × WSeq α))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (Computation.destruct (destruct (join nil)))
    (Computation.destruct (Computation.bind (destruct nil) destruct_join.aux))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
x : WSeq α
s : WSeq (WSeq α)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (cons x s).join.destruct.destruct ((cons x s).destruct.bind destruct_join.aux).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S_1 : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ S.think.join.destruct.tail = S.join.destruct ∧
    (S.think.destruct.bind destruct_join.aux).tail = S.destruct.bind destruct_join.aux

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S_1 : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    S.think.join.destruct.destruct (S.think.destruct.bind destruct_join.aux).destruct

Tactic:
exact Or.inr ⟨S, by simp⟩

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    c1.destruct c2.destruct

Tactic:
exact
    match c1, c2, h with
    | c, _, Or.inl <| rfl => by cases c.destruct <;> simp
    | _, _, Or.inr ⟨S, rfl, rfl⟩ => by
      induction S using WSeq.recOn
      case nil | cons => simp
      case think S => exact Or.inr ⟨S, by simp⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
bisim :
  Seq.IsBisimulation.{v} (α := Option β) fun (s1 s2 : Seq (Option β)) ↦
    ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
r :
  ∃ (s : WSeq β) (S_1 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join
⊢ map f S.join = (map (map f) S).join

Tactic:
apply
    Seq.eq_of_bisim fun s1 s2 =>
      ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))

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

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

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

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
s : WSeq β
think :
  ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    s.append (map f S.join) = s_1.append (map f S_2.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_2).join
⊢ Seq.BisimO
    (fun (s1 s2 : Seq (Option β)) ↦
      ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s.think.append (map f S.join))) (Seq.destruct (s.think.append (map (map f) S).join))

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

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

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

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

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    (map f s).append (map f S.join) = s_1.append (map f S_2.join) ∧
      (map f s).append (map (map f) S).join = s_1.append (map (map f) S_2).join

Tactic:
⟨map f s, S, rfl, rfl⟩

Premises used: And.intro, Stream'.WSeq.map, Exists.intro, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    (map f s).append (map f S.join) = s_1.append (map f S_2.join) ∧
      (map f s).append (map (map f) S).join = s_1.append (map (map f) S_2).join

Tactic:
exact ⟨map f s, S, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
x : WSeq α
s : WSeq (WSeq α)
⊢ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)),
    (map f x).append (map f s.join) = s_1.append (map f S.join) ∧
      (map f x).append (map (map f) s).join = s_1.append (map (map f) S).join

Tactic:
case cons s S => exact ⟨map f s, S, rfl, rfl⟩

Premises used: Stream'.WSeq.cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
⊢ ∃ (s : WSeq β) (S_2 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_2.join) ∧ (map (map f) S).join = s.append (map (map f) S_2).join

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

Premises used: And.intro, Exists.intro, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
refine_1 : map f S.join = append nil (map f S.join)
refine_2 : (map (map f) S).join = append nil (map (map f) S).join
⊢ ∃ (s : WSeq β) (S_2 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_2.join) ∧ (map (map f) S).join = s.append (map (map f) S_2).join

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

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

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
x : β
s : WSeq β
⊢ ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    s.append (map f S.join) = s_1.append (map f S_2.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_2).join

Tactic:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
x : β
s : WSeq β
⊢ ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    s.append (map f S.join) = s_1.append (map f S_2.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_2).join

Tactic:
exact ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
s : WSeq β
⊢ ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    s.append (map f S.join) = s_1.append (map f S_2.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_2).join

Tactic:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
s : WSeq β
⊢ ∃ (s_1 : WSeq β) (S_2 : WSeq (WSeq α)),
    s.append (map f S.join) = s_1.append (map f S_2.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_2).join

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

Tactic:
exact
      match s1, s2, h with
      | _, _, ⟨s, S, rfl, rfl⟩ => by
        induction s using WSeq.recOn <;> simp
        · induction S using WSeq.recOn <;> simp
          case cons s S => exact ⟨map f s, S, rfl, rfl⟩
          case think S => refine ⟨nil, S, ?_, ?_⟩ <;> simp
        · exact ⟨_, _, rfl, rfl⟩
        · exact ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ (s : WSeq β) (S_1 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

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

Premises used: And.intro, Exists.intro, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
r : map f S.join = append nil (map f S.join)
r₁ : (map (map f) S).join = append nil (map (map f) S).join
⊢ ∃ (s : WSeq β) (S_1 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Tactic:
refine ⟨nil, S, ?_, ?_⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = append nil (map f S.join)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ (map (map f) S).join = append nil (map (map f) S).join

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
h : s.IsFinite
⊢ s.toList.Terminates

Tactic:
h.out

Premises used: Stream'.WSeq.IsFinite.out
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s : WSeq α
⊢ s.length = Computation.map List.length s.toList

Tactic:
Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨n, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some _, s') => Sum.inr (n + 1, s')) (l.length, s) ∧
            c2 = Computation.map List.length (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l, s)))
      ?_ ⟨[], s, rfl, rfl⟩

Premises used: Computation.corec, Exists, Prod.mk, And, Computation.map, And.intro, Exists.intro, Computation.eq_of_bisim, Eq, List.length, rfl, List.nil
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s : WSeq α
c1 :
  Computation.IsBisimulation (α := ℕ) fun (c1 c2 : Computation ℕ) ↦
    ∃ (l : List α) (s : WSeq α),
      c1 =
          Computation.corec
            (fun (x : ℕ × WSeq α) ↦
              match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
              | (n, s) =>
                match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                | none => Sum.inl n
                | some (none, s') => Sum.inr (n, s')
                | some (some val, s') => Sum.inr (n + 1, s'))
            (l.length, s) ∧
        c2 =
          Computation.map (α := List α) List.length
            (Computation.corec
              (fun (x : List α × WSeq α) ↦
                match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                | (l, s) =>
                  match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                  | none => Sum.inl l.reverse
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l, s))
⊢ s.length = Computation.map List.length s.toList

Tactic:
refine
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨n, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some _, s') => Sum.inr (n + 1, s')) (l.length, s) ∧
            c2 = Computation.map List.length (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l, s)))
      ?_ ⟨[], s, rfl, rfl⟩

Premises used: Computation.corec, Exists, Prod.mk, And, Computation.map, And.intro, Exists.intro, Computation.eq_of_bisim, Eq, List.length, rfl, List.nil