awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)
have inl : ∀ (a : α) (h : f b = Sum.inl a),
  Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inl a) with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) Sum.inl a with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry) :
      α ⊕ Computation α)
Tactic: rcases h : f b with a | b'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
inl :
  ∀ (a : α) (h : f b = Sum.inl a),
    Eq.{u + 1} (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inl a) with
        | none =>
          Sum.inr
            (tail
              (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
                (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (match (motive := α ⊕ β → α ⊕ Computation α) Sum.inl a with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
        α ⊕ Computation α)
⊢ Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)
have inr : ∀ (b' : β) (h : f b = Sum.inr b'),
  Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inr b') with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) Sum.inr b' with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry) :
      α ⊕ Computation α)
Tactic: rcases h : f b with a | b'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Eq (α := α ⊕ Computation α)
    (Sum.inr
      (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯)))
    (Sum.inr
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Stream'.corec' (Corec.f f) (Sum.inr b')) ⋯))
have inr : tail
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry) =
  Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
    (Stream'.corec' (Corec.f f) (Sum.inr b')) sorry
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ tail
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Stream'.corec' (Corec.f f) (Sum.inr b')) ⋯
have inr : (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry)).val
    (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
  Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Stream'.corec' (Corec.f f) (Sum.inr b')) sorry)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (Stream'.corec' (Corec.f f) (Sum.inr b)).tail = Stream'.corec' (Corec.f f) (Sum.inr b')
have inr : Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')
Tactic: rw [Stream'.corec'_eq, Stream'.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')
have inr : Stream'.corec' (Corec.f f) (f b) = Stream'.corec' (Corec.f f) (Sum.inr b')
Tactic: dsimp [Corec.f]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (f b) = Stream'.corec' (Corec.f f) (Sum.inr b')
have inr : Stream'.corec' (Corec.f f) (Sum.inr b') = Stream'.corec' (Corec.f f) (Sum.inr b')
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ s₁ = s₂
have a : s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
  s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
have a : Stream'.IsBisimulation.{u} (α := Option α) fun (x y : Stream' (Option α)) ↦
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = x ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = y ∧ R s s'
Tactic: apply Stream'.eq_of_bisim fun x y => ∃ s s' : Computation α, s.1 = x ∧ s'.1 = y ∧ R s s'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
a :
  Stream'.IsBisimulation.{u} (α := Option α) fun (x y : Stream' (Option α)) ↦
    ∃ (s : Computation α),
      ∃ (s' : Computation α),
        s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = x ∧
          s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = y ∧ R s s'
⊢ s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
have a₁ : ∃ (s : Computation α),
  ∃ (s' : Computation α),
    s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
        s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) ∧
      s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
          s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) ∧
        R s s'
Tactic: apply Stream'.eq_of_bisim fun x y => ∃ s s' : Computation α, s.1 = x ∧ s'.1 = y ∧ R s s'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r_2 : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s.tail.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail
have mk : ∀ (val : Stream' (Option α)) (property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a)
  (r :
    R
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
        property)
      s')
  (this :
    head
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property) =
        s'.head ∧
      R
        (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property))
        s'.tail)
  (r :
    R
      (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property))
      s'.tail),
  (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)).val
      (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property)).tail
Tactic: cases s
Cleared hypotheses: s, r_2, this, r
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r_2 : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s'.tail.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail
have mk : ∀ (val : Stream' (Option α)) (property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a)
  (r :
    R s
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
        property))
  (this :
    s.head =
        head
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property) ∧
      R s.tail
        (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)))
  (r :
    R s.tail
      (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property))),
  (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
            property)).val
      (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
    (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) val
          property)).tail
Tactic: cases s'
Cleared hypotheses: s', r_2, this, r
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).head =
      s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).head ∧
    ∃ (s_1 : Computation α),
      ∃ (s'_1 : Computation α),
        s_1.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
            s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).tail ∧
          s'_1.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) =
              s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).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; rfl, by cases s'; rfl, r⟩) this
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ s.head = s'.head ∧ R s.tail s'.tail
have h : BisimO R s.destruct s'.destruct
Tactic: have h := bisim r
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
h : BisimO R s.destruct s'.destruct
⊢ s.head = s'.head ∧ R s.tail s'.tail
have revert : ∀ (r : R s s') (h : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
Tactic: revert r h
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
⊢ ∀ (r : R s s') (h : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
have refine_1 : ∀ (a : α) (r : R (pure a) s') (h : BisimO R (pure a).destruct s'.destruct),
  (pure a).head = s'.head ∧ R (pure a).tail s'.tail
Tactic: refine recOn s ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
refine_1 :
  ∀ (a : α) (r : R (pure a) s') (h : BisimO R (pure a).destruct s'.destruct),
    (pure a).head = s'.head ∧ R (pure a).tail s'.tail
⊢ ∀ (r : R s s') (h : BisimO R s.destruct s'.destruct), s.head = s'.head ∧ R s.tail s'.tail
have refine_2 : ∀ (s : Computation α) (r : R s.think s') (h : BisimO R s.think.destruct s'.destruct),
  s.think.head = s'.head ∧ R s.think.tail s'.tail
Tactic: refine recOn s ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' : α
⊢ ∀ (r : R (pure r') s') (h : BisimO R (pure r').destruct s'.destruct),
    (pure r').head = s'.head ∧ R (pure r').tail s'.tail
have refine_1 : ∀ (a : α) (r : R (pure r') (pure a)) (h : BisimO R (pure r').destruct (pure a).destruct),
  (pure r').head = (pure a).head ∧ R (pure r').tail (pure a).tail
Tactic: refine recOn s' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' : α
refine_1 :
  ∀ (a : α) (r : R (pure r') (pure a)) (h : BisimO R (pure r').destruct (pure a).destruct),
    (pure r').head = (pure a).head ∧ R (pure r').tail (pure a).tail
⊢ ∀ (r : R (pure r') s') (h : BisimO R (pure r').destruct s'.destruct),
    (pure r').head = s'.head ∧ R (pure r').tail s'.tail
have refine_1₁ : ∀ (s : Computation α) (r : R (pure r') s.think) (h : BisimO R (pure r').destruct s.think.destruct),
  (pure r').head = s.think.head ∧ R (pure r').tail s.think.tail
Tactic: refine recOn s' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' r' : Computation α
⊢ ∀ (r : R r'.think s') (h : BisimO R r'.think.destruct s'.destruct), r'.think.head = s'.head ∧ R r'.think.tail s'.tail
have refine_2 : ∀ (a : α) (r : R r'.think (pure a)) (h : BisimO R r'.think.destruct (pure a).destruct),
  r'.think.head = (pure a).head ∧ R r'.think.tail (pure a).tail
Tactic: refine recOn s' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' r' : Computation α
refine_2 :
  ∀ (a : α) (r : R r'.think (pure a)) (h : BisimO R r'.think.destruct (pure a).destruct),
    r'.think.head = (pure a).head ∧ R r'.think.tail (pure a).tail
⊢ ∀ (r : R r'.think s') (h : BisimO R r'.think.destruct s'.destruct), r'.think.head = s'.head ∧ R r'.think.tail s'.tail
have refine_2₁ : ∀ (s : Computation α) (r : R r'.think s.think) (h : BisimO R r'.think.destruct s.think.destruct),
  r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail
Tactic: refine recOn s' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
⊢ (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail
have refine_1 : (pure r').head = (pure a').head
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r_1 : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e :
  ∃ (s : Computation α),
    ∃ (s' : Computation α),
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁ ∧
        s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
refine_1 : (pure r').head = (pure a').head
⊢ (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail
have refine_1₁ : R (pure r').tail (pure a').tail
Tactic: constructor