awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s_1 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
have 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)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct
    s.destruct
have 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
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ join (f a, nil) = f a
have obtain : ∀ (a : β) (s : Seq β), join ((a, s), nil) = (a, s)
Tactic: obtain ⟨a, s⟩ := f a
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
a_1 : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)
have nil : join ((a, nil), nil) = (a, nil)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
a_1 : α
f : α → Seq1 β
a : β
s : Seq β
nil : join ((a, Seq.nil), Seq.nil) = (a, Seq.nil)
⊢ join ((a, s), Seq.nil) = (a, s)
have cons : ∀ (x : β) (s : Seq β), join ((a, Seq.cons x s), Seq.nil) = (a, Seq.cons x s)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ Seq.map f S.join = (Seq.map (map f) S).join
have 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
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))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ Seq.map f S.join = (Seq.map (map f) S).join
have 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
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))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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 nil (Seq.map f S.join)).destruct (append nil (Seq.map (map f) S).join).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have 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
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 β
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
have nil : 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: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have 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
Tactic: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α)
⊢ 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
have 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
Tactic: obtain ⟨a, s⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
have r : Seq.map f S.join = append nil (Seq.map f S.join)
Tactic: refine ⟨nil, S, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
r : Seq.map f S.join = append nil (Seq.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
have r₁ : (Seq.map (map f) S).join = append nil (Seq.map (map f) S).join
Tactic: refine ⟨nil, S, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join
have nil : map f (join ((a, nil), S)) = (map (map f) ((a, nil), S)).join
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join
have cons : ∀ (x : α) (s : Seq α), map f (join ((a, Seq.cons x s), S)) = (map (map f) ((a, Seq.cons x s), S)).join
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ SS.join.join = (Seq.map join SS).join
have 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
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))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ SS.join.join = (Seq.map join SS).join
have 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
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))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α))
⊢ 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
have 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 nil SS.join.join).destruct (append nil (Seq.map join SS).join).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have 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
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α))
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α))
⊢ 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
have nil : 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: cases SS
Cleared hypotheses: SS
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ 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
have 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
Tactic: cases SS
Cleared hypotheses: SS
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
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
have cons : match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons x s).join.join.destruct,
  (Seq.cons x.join (Seq.map join 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 : Seq1 (Seq1 α)
SS : Seq (Seq1 (Seq1 α))
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons S SS).join.join.destruct,
    (Seq.cons S.join (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
have obtain : ∀ (s : Seq1 α) (S : Seq (Seq1 α)),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons (s, S) SS).join.join.destruct,
    (Seq.cons (join (s, S)) (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: obtain ⟨s, S⟩ := S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α))
s : Seq1 α
S : Seq (Seq1 α)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons (s, S) SS).join.join.destruct,
    (Seq.cons (join (s, S)) (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
have obtain : ∀ (x : α) (s : Seq α),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons ((x, s), S) SS).join.join.destruct,
    (Seq.cons (join ((x, s), S)) (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: obtain ⟨x, s⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α))
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons ((x, s), S) SS).join.join.destruct,
    (Seq.cons (join ((x, s), S)) (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
have simp : match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, s.append (S.join.append SS.join.join)),
  (Seq.cons (join ((x, s), S)) (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: simp only [Seq.join_cons, join_append, destruct_cons]