awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
hb_cons : cons b_hd b_tl ≠ nil
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
a_hd : α
a_tl : Seq α
right : motive a_tl b_tl
ha' : 0 = a_tl.length' + 1
pos : ∀ (u : ℕ∞) (ha' : 0 = u + 1), False
⊢ False

Tactic:
generalize a_tl.length' = u at ha'

Premises used: Stream'.Seq.length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
hb_cons : cons b_hd b_tl ≠ nil
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
a_hd : α
a_tl : Seq α
right : motive a_tl b_tl
u : ℕ∞
ha' : 0 = u + 1
pos : ∀ (u : ℕ) (ha' : 0 = u + 1), False
⊢ False

Tactic:
enat_to_nat
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
hb_cons : ¬cons b_hd b_tl = nil
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
a_hd : α
a_tl : Seq α
right : motive a_tl b_tl
u : ℕ
ha' : 0 = u + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b' : Seq β
hb_cons : b' ≠ nil
this : motive (a.drop (a.length ha)) b'
pos : ∀ (hb_cons : Ne.{v + 1} (α := Seq β) nil nil) (this : motive (a.drop (a.length ha)) nil), False
pos₁ :
  ∀ (b_hd : β) (b_tl : Seq β) (hb_cons : cons b_hd b_tl ≠ nil) (this : motive (a.drop (a.length ha)) (cons b_hd b_tl)),
    False
⊢ False

Tactic:
cases b' with
  | nil =>
    contradiction
  | cons b_hd b_tl =>
    obtain ⟨a_hd, a_tl, ha', _⟩ := step _ _ this _ _ rfl
    apply_fun length' at ha'
    simp only [drop_length', length'_of_terminates ha, tsub_self, length'_cons] at ha'
    generalize a_tl.length' = u at ha'
    enat_to_nat
    lia

Premises used: Stream'.Seq.length', Stream'.Seq.length'_of_terminates, tsub_self, Stream'.Seq.length'_cons, Stream'.Seq.drop_length', Stream'.Seq.nil, Stream'.Seq.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ map f (a, s) = (f a, Seq.map f s)

Tactic:
rfl

Premises used: Stream'.Seq1.map, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Seq α
⊢ map id (a, s) = (a, s)

Tactic:
simp [map]

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

Tactic:
rfl

Premises used: rfl, Stream'.Seq1.join
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
rw rw₁ :
  (match (motive := Option (Seq1 α) → Seq1 α) some (b, s) with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)
⊢ (match (motive := Option (Seq1 α) → Seq1 α) (Seq.cons b s).destruct with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)

Tactic:
rw [destruct_cons]

Premises used: Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
H :
  ∀ (s : Seq α),
    BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct
      s.destruct
⊢ (Seq.map ret s).join = s

Tactic:
apply coinduction2 s

Premises used: Stream'.Seq.coinduction2
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s_1 s : Seq α
H :
  BisimO.{u} (α := α) (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s)
    (destruct (Seq.join (Seq.map ret nil))) (destruct nil)
H₁ :
  ∀ (x : α) (s : Seq α),
    BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s)
      (Seq.map ret (Seq.cons x s)).join.destruct (Seq.cons x s).destruct
⊢ BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct
    s.destruct

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ BisimO.{u} (α := α) (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s)
    (destruct (Seq.join (Seq.map ret nil))) (destruct nil)

Tactic:
simp [ret]

Premises used: Stream'.Seq1.ret
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
x : α
s_1 : Seq α
⊢ BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s)
    (Seq.map ret (Seq.cons x s_1)).join.destruct (Seq.cons x s_1).destruct

Tactic:
simp [ret]

Premises used: Stream'.Seq1.ret
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ bind (a, s) (ret ∘ f) = map f (a, s)

Tactic:
simp [bind, map, map_comp, ret]

Premises used: Stream'.Seq1.ret, Stream'.Seq1.map, Stream'.Seq1.bind, Stream'.Seq.map_comp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : α
f : α → Seq1 β
obtain : ∀ (a : β) (s : Seq β), join ((a, s), nil) = (a, s)
⊢ join (f a, nil) = f a

Tactic:
obtain ⟨a, s⟩ := f a
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a_1 : α
f : α → Seq1 β
a : β
s : Seq β
nil : join ((a, Seq.nil), Seq.nil) = (a, Seq.nil)
cons : ∀ (x : β) (s : Seq β), join ((a, Seq.cons x s), Seq.nil) = (a, Seq.cons x s)
⊢ join ((a, s), Seq.nil) = (a, s)

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a_1 : α
f : α → Seq1 β
a : β
⊢ join ((a, nil), nil) = (a, nil)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a_1 : α
f : α → Seq1 β
a x : β
s : Seq β
⊢ join ((a, Seq.cons x s), nil) = (a, Seq.cons x s)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
bisim :
  Seq.IsBisimulation.{v} (α := β) fun (s1 s2 : Seq β) ↦
    ∃ (s : Seq β) (S : Seq (Seq1 α)), s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join
r :
  ∃ (s : Seq β) (S_1 : Seq (Seq1 α)),
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join
⊢ Seq.map f S.join = (Seq.map (map f) S).join

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

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

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

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

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

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

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

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

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

Tactic:
simpa [map] using ⟨_, _, rfl, rfl⟩

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

Tactic:
case nil =>
          cases S <;> simp
          case cons x S =>
            obtain ⟨a, s⟩ := x
            simpa [map] using ⟨_, _, rfl, rfl⟩

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

Tactic:
⟨s, S, rfl, rfl⟩

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

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

Tactic:
exact
      match s1, s2, h with
      | _, _, ⟨s, S, rfl, rfl⟩ => by
        cases s <;> simp
        case nil =>
          cases S <;> simp
          case cons x S =>
            obtain ⟨a, s⟩ := x
            simpa [map] using ⟨_, _, rfl, rfl⟩
        case cons _ s => exact ⟨s, S, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ (s : Seq β) (S_1 : Seq (Seq1 α)),
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join

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

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

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

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

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
S : Seq (Seq1 α)
nil : map f (join ((a, Seq.nil), S)) = (map (map f) ((a, Seq.nil), S)).join
cons : ∀ (x : α) (s : Seq α), map f (join ((a, Seq.cons x s), S)) = (map (map f) ((a, Seq.cons x s), S)).join
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
⊢ map f (join ((a, nil), S)) = (map (map f) ((a, nil), S)).join

Tactic:
simp [map]

Premises used: Stream'.Seq1.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ map f (join ((a, Seq.cons x s), S)) = (map (map f) ((a, Seq.cons x s), S)).join

Tactic:
simp [map]

Premises used: Stream'.Seq1.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
bisim :
  Seq.IsBisimulation.{u} (α := α) fun (s1 s2 : Seq α) ↦
    ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
r :
  ∃ (s : Seq α) (SS_1 : Seq (Seq1 (Seq1 α))),
    SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
⊢ SS.join.join = (Seq.map join SS).join

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

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

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

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
x : α
s : Seq α
cons :
  ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    s.append SS.join.join = s_1.append SS_2.join.join ∧
      s.append (Seq.map join SS).join = s_1.append (Seq.map join SS_2).join
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    ((Seq.cons x s).append SS.join.join).destruct ((Seq.cons x s).append (Seq.map join SS).join).destruct

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

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

Tactic:
simp