awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
none :
  ∀ (h : f b = Option.none),
    Eq.{u + 1} (α := Option (Seq1 α))
      (Option.map
        (fun (a' : α) ↦
          (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) Option.none with
          | Option.none => (Option.none, Option.none)
          | some (a, b') => (some a, some b'))))
      (match (motive := Option (α × β) → Option (α × Seq α)) Option.none with
      | Option.none => Option.none
      | some (a, b) =>
        some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))
⊢ Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | Option.none => (Option.none, Option.none)
        | some (a, b') => (some a, some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) f b with
    | Option.none => Option.none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))
have some : ∀ (s : α × β) (h : f b = some s),
  Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some s with
        | Option.none => (Option.none, Option.none)
        | some (a, b') => (some a, some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) some s with
    | Option.none => Option.none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry))
Tactic: rcases h : f b with - | s
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
s : α × β
h : f b = some s
⊢ Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some s with
        | none => (none, none)
        | some (a, b') => (some a, some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) some s with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))
have some : ∀ (a : α) (b' : β) (h : f b = some (a, b')),
  Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some (a, b') with
        | none => (none, none)
        | some (a, b') => (some a, some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) some (a, b') with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry))
Tactic: obtain ⟨a, b'⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ some (a, tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)) =
    some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b')) ⋯)
have some : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry) =
  Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b')) sorry
Tactic: apply congr_arg fun b' => some (a, b')
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b')) ⋯
have some : (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry)) :
    Stream' (Option α)) =
  (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b')) sorry) : Stream' (Option α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ (corec' (Corec.f f) (some b)).tail = corec' (Corec.f f) (some b')
have some : corec' (Corec.f f) (Corec.f f (some b)).snd = corec' (Corec.f f) (some b')
Tactic: rw [Stream'.corec'_eq, Stream'.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f) (Corec.f f (some b)).snd = corec' (Corec.f f) (some b')
have some : corec' (Corec.f f)
    (Prod.snd.{u, v} (α := Option α)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
      | none => (none, none)
      | some (a, b') => (some a, some b'))) =
  corec' (Corec.f f) (some b')
Tactic: dsimp [Corec.f]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f)
      (Prod.snd.{u, v} (α := Option α)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b'))) =
    corec' (Corec.f f) (some b')
have some : corec' (Corec.f f)
    (Prod.snd.{u, v} (α := Option α)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some (a, b') with
      | none => (none, none)
      | some (a, b') => (some a, some b'))) =
  corec' (Corec.f f) (some b')
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ corec f b = nil
have a : (corec f b).destruct = none
Tactic: apply destruct_eq_none
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
x : α
s : β
h : f b = some (x, s)
⊢ corec f b = cons x (corec f s)
have a : (corec f b).destruct = some (x, corec f s)
Tactic: apply destruct_eq_cons
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ s₁ = s₂
have a : (↑s₁ : Stream' (Option α)) = (↑s₂ : Stream' (Option α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ (↑s₁ : Stream' (Option α)) = (↑s₂ : Stream' (Option α))
have a : Stream'.IsBisimulation.{u} (α := Option α) fun (x y : Stream' (Option α)) ↦
  ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = x ∧ (↑s' : Stream' (Option α)) = y ∧ R s s'
Tactic: apply Stream'.eq_of_bisim fun x y => ∃ s s' : Seq α, s.1 = x ∧ s'.1 = y ∧ R s s'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
a :
  Stream'.IsBisimulation.{u} (α := Option α) fun (x y : Stream' (Option α)) ↦
    ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = x ∧ (↑s' : Stream' (Option α)) = y ∧ R s s'
⊢ (↑s₁ : Stream' (Option α)) = (↑s₂ : Stream' (Option α))
have a₁ : ∃ (s : Seq α),
  ∃ (s' : Seq α),
    (↑s : Stream' (Option α)) = (↑s₁ : Stream' (Option α)) ∧
      (↑s' : Stream' (Option α)) = (↑s₂ : Stream' (Option α)) ∧ R s s'
Tactic: apply Stream'.eq_of_bisim fun x y => ∃ s s' : Seq α, s.1 = x ∧ s'.1 = y ∧ R s s'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r_2 : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ (↑s.tail : Stream' (Option α)) = (↑s : Stream' (Option α)).tail
have mk : ∀ (val : Stream' (Option α)) (property : val.IsSeq)
  (r : R (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) s')
  (this :
    head (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) = s'.head ∧
      R (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) s'.tail)
  (r : R (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) s'.tail),
  (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)).tail
Tactic: cases s using Subtype.recOn
Cleared hypotheses: s, r_2, this, r
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r_2 : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ (↑s'.tail : Stream' (Option α)) = (↑s' : Stream' (Option α)).tail
have mk : ∀ (val : Stream' (Option α)) (property : val.IsSeq)
  (r : R s (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property))
  (this :
    s.head = head (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) ∧
      R s.tail (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)))
  (r : R s.tail (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property))),
  (↑(tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)).tail
Tactic: cases s' using Subtype.recOn
Cleared hypotheses: s', r_2, this, r
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
⊢ (↑s : Stream' (Option α)).head = (↑s' : Stream' (Option α)).head ∧
    ∃ (s_1 : Seq α),
      ∃ (s'_1 : Seq α),
        (↑s_1 : Stream' (Option α)) = (↑s : Stream' (Option α)).tail ∧
          (↑s'_1 : Stream' (Option α)) = (↑s' : Stream' (Option α)).tail ∧ R s_1 s'_1
have suffices : s.head = s'.head ∧ R s.tail s'.tail
Tactic: suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
          by cases s' using Subtype.recOn; rfl, r⟩) this
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
⊢ s.head = s'.head ∧ R s.tail s'.tail
have this : BisimO R s.destruct s'.destruct
Tactic: have := bisim r
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
this : BisimO R s.destruct s'.destruct
⊢ s.head = s'.head ∧ R s.tail s'.tail
have revert : ∀ (r : R s s') (this : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
Tactic: revert r this
Cleared hypotheses: r, this
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
⊢ ∀ (r : R s s') (this : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
have nil : ∀ (r : R nil s') (this : BisimO R (destruct nil) s'.destruct), head nil = s'.head ∧ R (tail nil) s'.tail
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s s' : Seq α
nil :
  ∀ (r : R Seq.nil s') (this : BisimO R (destruct Seq.nil) s'.destruct),
    head Seq.nil = s'.head ∧ R (tail Seq.nil) s'.tail
⊢ ∀ (r : R s s') (this : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
have cons : ∀ (x : α) (s : Seq α) (r : R (cons x s) s') (this : BisimO R (cons x s).destruct s'.destruct),
  (cons x s).head = s'.head ∧ R (cons x s).tail s'.tail
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
⊢ ∀ (r : R nil s') (this : BisimO R (destruct nil) s'.destruct), head nil = s'.head ∧ R (tail nil) s'.tail
have nil : ∀ (r : R nil nil) (this : BisimO R (destruct nil) (destruct nil)),
  Eq.{u + 1} (α := Option α) (head nil) (head nil) ∧ R (tail nil) (tail nil)
Tactic: cases s'
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
nil :
  ∀ (r : R Seq.nil Seq.nil) (this : BisimO R (destruct Seq.nil) (destruct Seq.nil)),
    Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil) ∧ R (tail Seq.nil) (tail Seq.nil)
⊢ ∀ (r : R Seq.nil s') (this : BisimO R (destruct Seq.nil) s'.destruct),
    head Seq.nil = s'.head ∧ R (tail Seq.nil) s'.tail
have nil₁ : ∀ (x : α) (s : Seq α) (r : R Seq.nil (cons x s)) (this : BisimO R (destruct Seq.nil) (cons x s).destruct),
  head Seq.nil = (cons x s).head ∧ R (tail Seq.nil) (cons x s).tail
Tactic: cases s'
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
x : α
s : Seq α
⊢ ∀ (r : R (cons x s) s') (this : BisimO R (cons x s).destruct s'.destruct),
    (cons x s).head = s'.head ∧ R (cons x s).tail s'.tail
have cons : ∀ (r : R (cons x s) nil) (this : BisimO R (cons x s).destruct (destruct nil)),
  (cons x s).head = head nil ∧ R (cons x s).tail (tail nil)
Tactic: cases s'
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
s' : Seq α
x : α
s : Seq α
cons :
  ∀ (r : R (Seq.cons x s) nil) (this : BisimO R (Seq.cons x s).destruct (destruct nil)),
    (Seq.cons x s).head = head nil ∧ R (Seq.cons x s).tail (tail nil)
⊢ ∀ (r : R (Seq.cons x s) s') (this : BisimO R (Seq.cons x s).destruct s'.destruct),
    (Seq.cons x s).head = s'.head ∧ R (Seq.cons x s).tail s'.tail
have cons₁ : ∀ (x_1 : α) (s_1 : Seq α) (r : R (Seq.cons x s) (Seq.cons x_1 s_1))
  (this : BisimO R (Seq.cons x s).destruct (Seq.cons x_1 s_1).destruct),
  (Seq.cons x s).head = (Seq.cons x_1 s_1).head ∧ R (Seq.cons x s).tail (Seq.cons x_1 s_1).tail
Tactic: cases s'
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
r : R nil nil
this : BisimO R (destruct nil) (destruct nil)
⊢ Eq.{u + 1} (α := Option α) (head nil) (head nil) ∧ R (tail nil) (tail nil)
have nil : Eq.{u + 1} (α := Option α) (head nil) (head nil)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
r : R Seq.nil Seq.nil
this : BisimO R (destruct Seq.nil) (destruct Seq.nil)
nil : Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil)
⊢ Eq.{u + 1} (α := Option α) (head Seq.nil) (head Seq.nil) ∧ R (tail Seq.nil) (tail Seq.nil)
have nil₁ : R (tail Seq.nil) (tail Seq.nil)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R nil (cons x s)
this : BisimO R (destruct nil) (cons x s).destruct
⊢ head nil = (cons x s).head ∧ R (tail nil) (cons x s).tail
have this₁ : BisimO R none (some (x, s))
Tactic: rw [destruct_nil, destruct_cons] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ (s : Seq α), ∃ (s' : Seq α), (↑s : Stream' (Option α)) = t₁ ∧ (↑s' : Stream' (Option α)) = t₂ ∧ R s s'
x : α
s : Seq α
r_1 : R (cons x s) nil
this : BisimO R (cons x s).destruct (destruct nil)
⊢ (cons x s).head = head nil ∧ R (cons x s).tail (tail nil)
have this₁ : BisimO R (some (x, s)) none
Tactic: rw [destruct_nil, destruct_cons] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ s₁ = s₂
have apply : IsBisimulation motive
Tactic: apply eq_of_bisim motive _ base
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
⊢ BisimO motive s₁.destruct s₂.destruct
have inl : ∀ (h_nil₁ : s₁ = nil) (h_nil₂ : s₂ = nil), BisimO motive s₁.destruct s₂.destruct
Tactic: rcases step s₁ s₂ h with ⟨h_nil₁, h_nil₂⟩ | ⟨_, _, _, h₁, h₂, _⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
inl : ∀ (h_nil₁ : s₁ = nil) (h_nil₂ : s₂ = nil), BisimO motive s₁.destruct s₂.destruct
⊢ BisimO motive s₁.destruct s₂.destruct
have inr : ∀ (w : α) (w_1 w_2 : Seq α) (h₁ : s₁ = cons w w_1) (h₂ : s₂ = cons w w_2),
  motive w_1 w_2 → BisimO motive s₁.destruct s₂.destruct
Tactic: rcases step s₁ s₂ h with ⟨h_nil₁, h_nil₂⟩ | ⟨_, _, _, h₁, h₂, _⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
⊢ s₁ = s₂
have apply : ∀ (s₁ s₂ : Seq α),
  motive' s₁ s₂ →
    s₁ = nil ∧ s₂ = nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'
Tactic: apply eq_of_bisim' motive' (by grind)
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : s₁ = s₂ ∨ motive s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inl : s₁ = nil ∧ s₁ = nil ∨
  ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: rcases ih with (rfl | ih)
Cleared hypotheses: s₂, ih
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : s₁ = s₂ ∨ motive s₁ s₂
inl :
  s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inr : ∀ (ih : motive s₁ s₂),
  s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: rcases ih with (rfl | ih)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inl : Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
  ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: cases s₁
Cleared hypotheses: s₁