awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct
have rw : BisimO
  (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
  (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
Tactic: rw [h.left, h.right]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
have induction : ∀ (h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
induction :
  ∀ (h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
have induction₁ : ∀ (x : α) (s : WSeq α)
  (h : c1 = ((cons x s).append t).destruct ∧ c2 = (cons x s).destruct.bind (destruct_append.aux t)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x s).append t).destruct.destruct ((cons x s).destruct.bind (destruct_append.aux t)).destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
induction :
  ∀ (h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
induction₁ :
  ∀ (x : α) (s : WSeq α)
    (h : c1 = ((cons x s).append t).destruct ∧ c2 = (cons x s).destruct.bind (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      ((cons x s).append t).destruct.destruct ((cons x s).destruct.bind (destruct_append.aux t)).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
have think : ∀ (s : WSeq α) (h : c1 = (s.think.append t).destruct ∧ c2 = s.think.destruct.bind (destruct_append.aux t)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.think.append t).destruct.destruct (s.think.destruct.bind (destruct_append.aux t)).destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
have induction : ∀ (h : c1 = destruct (append nil nil) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux nil)),
  BisimO.{u} (α := Option (α × WSeq α))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (Computation.destruct (destruct (append nil nil)))
    (Computation.destruct (Computation.bind (destruct nil) (destruct_append.aux nil)))
Tactic: induction t using WSeq.recOn
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
induction :
  ∀ (h : c1 = destruct (append nil nil) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux nil)),
    BisimO.{u} (α := Option (α × WSeq α))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (Computation.destruct (destruct (append nil nil)))
      (Computation.destruct (Computation.bind (destruct nil) (destruct_append.aux nil)))
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
have induction₁ : ∀ (x : α) (s : WSeq α)
  (h : c1 = (append nil (cons x s)).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux (cons x s))),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil (cons x s)).destruct.destruct
    (Computation.bind (destruct nil) (destruct_append.aux (cons x s))).destruct
Tactic: induction t using WSeq.recOn
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
induction :
  ∀ (h : c1 = destruct (append nil nil) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux nil)),
    BisimO.{u} (α := Option (α × WSeq α))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (Computation.destruct (destruct (append nil nil)))
      (Computation.destruct (Computation.bind (destruct nil) (destruct_append.aux nil)))
induction₁ :
  ∀ (x : α) (s : WSeq α)
    (h : c1 = (append nil (cons x s)).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux (cons x s))),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (append nil (cons x s)).destruct.destruct
      (Computation.bind (destruct nil) (destruct_append.aux (cons x s))).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
have think : ∀ (s : WSeq α)
  (h : c1 = (append nil s.think).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux s.think)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil s.think).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux s.think)).destruct
Tactic: induction t using WSeq.recOn
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
S : WSeq (WSeq α)
⊢ S.join.destruct = S.destruct.bind destruct_join.aux
have c1 : Computation.IsBisimulation.{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
Tactic: apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux)
      _ (Or.inr ⟨S, rfl, rfl⟩)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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
c : Computation (Option (α × WSeq α))
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    c.destruct c.destruct
have inl : ∀ (val : Option (α × WSeq α)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (Sum.inl val) (Sum.inl val)
Tactic: cases c.destruct
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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
c : Computation (Option (α × WSeq α))
inl :
  ∀ (val : Option (α × WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
      (Sum.inl val) (Sum.inl val)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    c.destruct c.destruct
have inr : ∀ (val : Computation (Option (α × WSeq α))),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (Sum.inr val) (Sum.inr val)
Tactic: cases c.destruct
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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.join.destruct.destruct (S.destruct.bind destruct_join.aux).destruct
have 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))
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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))
⊢ 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
have 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
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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
⊢ 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
have 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
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = (map (map f) S).join
have 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
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))
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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
⊢ map f S.join = (map (map f) S).join
have 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
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))
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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 α)
⊢ 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))
have 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 nil (map f S.join))) (Seq.destruct (append nil (map (map f) S).join))
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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))
⊢ 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))
have 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 ((cons x s).append (map f S.join))) (Seq.destruct ((cons x s).append (map (map f) S).join))
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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 α)
⊢ 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 nil (map f S.join))) (Seq.destruct (append nil (map (map f) S).join))
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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 β
⊢ 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 ((cons x s).append (map f S.join))) (Seq.destruct ((cons x s).append (map (map f) S).join))
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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 β
⊢ 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))
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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 α)
⊢ 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
have nil : 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: induction S using WSeq.recOn
Cleared hypotheses: S