awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
have nil : 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: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have cons : ∀ (x : α) (s : Seq α),
  match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f (cons x s)).destruct,
    (map f (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
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α
⊢ match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f (cons x s_1)).destruct,
    (map f (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
have 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)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
have refine_1 : map f t = map f (append nil t)
Tactic: refine ⟨nil, t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ ∃ (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)
have refine_2 : map f t = (map f nil).append (map f t)
Tactic: refine ⟨nil, t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ (cons (a, s) S).join = cons a (s.append S.join)
have 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)
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⟩)
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s_1 : 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)
s : 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))
    s.destruct s.destruct
have nil : 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: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s_1 : 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)
s : Seq α
nil :
  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 Seq.nil) (destruct Seq.nil)
⊢ 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))
    s.destruct s.destruct
have cons : ∀ (x : α) (s : 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 x s).destruct (cons x s).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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))
    (cons x s_1).destruct (cons x s_1).destruct
have cons : 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: rw [destruct_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
s : Seq α
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, s) S).join.destruct (cons a (s.append S.join)).destruct
have nil : 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: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 = (cons (a, s) S).join ∧ s2 = 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 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, Seq.nil) S).join.destruct (cons a (append Seq.nil S.join)).destruct
⊢ 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, s) S).join.destruct (cons a (s.append S.join)).destruct
have cons : ∀ (x : α) (s : 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) S).join.destruct (cons a ((cons x s).append S.join)).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = S.join.append T.join
have 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)
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))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ (S.append T).join = S.join.append T.join
have 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)
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))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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 nil (S.append T).join).destruct (append nil (S.join.append T.join)).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have 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))
    ((cons x s).append (S.append T).join).destruct ((cons x s).append (S.join.append T.join)).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α
⊢ 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))
    ((cons x s).append (S.append T).join).destruct ((cons x s).append (S.join.append T.join)).destruct
have 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)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have nil : 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: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have cons : ∀ (x : Seq1 α) (s : Seq (Seq1 α)),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) ((cons x s).append T).join.destruct,
    ((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: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) ((cons x s).append T).join.destruct,
    ((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
have cons : match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons x (s.append T)).join.destruct,
  ((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
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
s : Seq1 α
T : Seq (Seq1 α)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons s T).join.destruct, (cons s 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
have cons : ∀ (a : α) (s : Seq α),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons (a, s) T).join.destruct,
    (cons (a, s) 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: obtain ⟨a, s⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
a : α
s : Seq α
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons (a, s) T).join.destruct,
    (cons (a, s) 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
have cons : ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
  s.append T.join = s_1.append (S.append T_2).join ∧ s.append T.join = s_1.append (S.join.append T_2.join)
Tactic: simp only [join_cons, destruct_cons, true_and]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
a : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append T.join = s_1.append (S.append T_2).join ∧ s.append T.join = s_1.append (S.join.append T_2.join)
have cons : s.append T.join = s.append (append nil T).join
Tactic: refine ⟨s, nil, T, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
a : α
s : Seq α
cons : s.append T.join = s.append (append nil T).join
⊢ ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append T.join = s_1.append (S.append T_2).join ∧ s.append T.join = s_1.append (S.join.append T_2.join)
have cons₁ : s.append T.join = s.append (append (join nil) T.join)
Tactic: refine ⟨s, nil, T, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have nil : 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: cases T with
            | nil => simp
            | cons s T =>
              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
              refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
nil :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) destruct (join Seq.nil), destruct (join Seq.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
⊢ 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
have cons : ∀ (s : Seq1 α) (T : Seq (Seq1 α)),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons s T).join.destruct, (cons s 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 T with
            | nil => simp
            | cons s T =>
              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
              refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
T : Seq (Seq1 α)
s : Seq1 α
S : Seq (Seq1 α)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons s (S.append T)).join.destruct,
    ((cons s 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
have obtain : ∀ (a : α) (s : Seq α),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons (a, s) (S.append T)).join.destruct,
    ((cons (a, s) 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: obtain ⟨a, s⟩ := s
Cleared hypotheses: s