awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : r' = a'
⊢ (pure r').head = (pure a').head
have refine_1 : (pure a').head = (pure a').head
Tactic: rw [h]
-- 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' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail
have r₁ : R (pure a') (pure a')
Tactic: rw [h] at r
Cleared hypotheses: r, h
-- 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' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (pure r').destruct a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail
have h₁ : BisimO R (Sum.inl r') (Sum.inr a')
Tactic: rw [destruct_pure, destruct_think] at h
Cleared hypotheses: h
-- 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' r' : Computation α
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
have h₁ : BisimO R (Sum.inr r') (Sum.inl a')
Tactic: rw [destruct_pure, destruct_think] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) m = some a →
    s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n = some a
have obtain : ∀ (f : Stream' (Option α)) (al : ∀ ⦃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) f al) m =
      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) f al) n =
      some a
Tactic: obtain ⟨f, al⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃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) f al) m =
      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) f al) n =
      some a
have refl : 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) f al) m =
    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) f al) m =
    some a
Tactic: induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
refl :
  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) f al) m =
      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) f al) m =
      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) f al) m =
      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) f al) n =
      some a
have step : ∀ {m_1 : ℕ},
  m.le m_1 →
    ∀
      (IH :
        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) f
                al)
              m =
            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) f
                al)
              m_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) f al)
            m =
          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) f al)
            m_1.succ =
          some a
Tactic: induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h_1 : s.Terminates
a : α
n : ℕ
h : some a = s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n
⊢ (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n).isSome = true
have rw : (some a).isSome = true
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h :
  (fun (b : Option α) ↦ some a = b)
    (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get n)
⊢ a ∈ s
have zero : ∀
  (h :
    some a =
      s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get 0),
  a ∈ s
Tactic: rcases n with - | n'
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h :
  (fun (b : Option α) ↦ some a = b)
    (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get n)
zero :
  ∀
    (h :
      some a =
        s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get 0),
    a ∈ s
⊢ a ∈ s
have succ : ∀ (n' : ℕ)
  (h :
    some a =
      s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get
        (n' + 1)),
  a ∈ s
Tactic: rcases n with - | n'
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
⊢ s = empty α
have a : s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
  (empty α).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
s : Computation α
H : ¬s.Terminates
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
have a : ∀ (n : ℕ),
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
have a : ∀ (h : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n = none),
  none = (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
Tactic: rcases h : s.val n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
a :
  ∀ (h : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n = none),
    none = (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
have a₁ : ∀ (val : α)
  (h : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n = some val),
  some val = (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
Tactic: rcases h : s.val n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val : α
h : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n = some val
⊢ some val = (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
have a : s.Terminates
Tactic: refine absurd ?_ H
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h_1 : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s
have rw : s.get ∈ s
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
a : α
p : s ~> a
⊢ a ∈ s
have obtain : ∀ (a' : α) (h : a' ∈ s), a ∈ s
Tactic: obtain ⟨a', h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results a s.length
have rw : s.Results s.get s.length
Tactic: rw [← get_eq_of_mem _ h]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ m = n
have this : s.Terminates
Tactic: haveI := h1.terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this_1 this : s.Terminates
⊢ m = n
have rw : s.length = n
Tactic: rw [← h1.length, h2.length]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this_1 this : s.Terminates
rw : s.length = n
⊢ m = n
have rw₁ : n = n
Tactic: rw [← h1.length, h2.length]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length = s.length + 1
have a : s.think.length ≤ s.length + 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
a : s.think.length ≤ s.length + 1
⊢ s.think.length = s.length + 1
have a₁ : s.length + 1 ≤ s.think.length
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length
have this : (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      s.think.length).isSome =
  true
Tactic: have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
      Nat.find_spec ((terminates_def _).1 s.think_terminates)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        s.think.length).isSome =
    true
⊢ s.length + 1 ≤ s.think.length
have a : ∀
  (this :
    (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          s.think.length).isSome =
      true),
  s.length + 1 ≤ s.think.length
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ ∀
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            s.think.length).isSome =
        true),
    s.length + 1 ≤ s.think.length
have a : ∀
  (this :
    (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0).isSome =
      true),
  s.length + 1 ≤ 0
Tactic: rcases length (think s) with - | n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
a :
  ∀
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            0).isSome =
        true),
    s.length + 1 ≤ 0
⊢ ∀
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            s.think.length).isSome =
        true),
    s.length + 1 ≤ s.think.length
have a₁ : ∀ (n : ℕ)
  (this :
    (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (n + 1)).isSome =
      true),
  s.length + 1 ≤ n + 1
Tactic: rcases length (think s) with - | n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (n + 1)).isSome =
    true
⊢ s.length + 1 ≤ n + 1
have a : s.length ≤ n
Tactic: apply Nat.succ_le_succ
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (n + 1)).isSome =
    true
⊢ s.length ≤ n
have a : (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n).isSome = true
Tactic: apply Nat.find_min'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
⊢ s.think.length = n + 1
have rw : s.length + 1 = n + 1
Tactic: rw [length_think, h.length]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
rw : s.length + 1 = n + 1
⊢ s.think.length = n + 1
have rw₁ : n + 1 = n + 1
Tactic: rw [length_think, h.length]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
⊢ ∃ (m : ℕ), s.Results a m ∧ n = m + 1
have this : s.Terminates
Tactic: haveI := of_think_terminates h.terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this : s.Terminates
⊢ ∃ (m : ℕ), s.Results a m ∧ n = m + 1
have this₁ : s.Results a s.length
Tactic: have := results_of_terminates' _ (of_think_mem h.mem)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
⊢ s.Results a n
have let : ∀ (n' : ℕ) (r : s.Results a n') (e : n + 1 = n' + 1), s.Results a n
Tactic: let ⟨n', r, e⟩ := of_results_think h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
e : n + 1 = n' + 1
⊢ s.Results a n
have h' : n = n'
Tactic: injection e with h'
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
a : α
n : ℕ
⊢ ((pure a).thinkN n).Results a n
have this : ((pure a).thinkN n).Results a (0 + n)
Tactic: have := results_thinkN n (results_pure a)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
⊢ ((pure a).thinkN n).Results a n
have rwa : ∀ (this : ((pure a).thinkN n).Results a n), ((pure a).thinkN n).Results a n
Tactic: rwa [Nat.zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s = (pure a).thinkN n
have zero : ∀ {s : Computation α} (h : s.Results a 0), s = (pure a).thinkN 0
Tactic: induction n generalizing s with | zero | succ n IH
Cleared hypotheses: s, n, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
zero : ∀ {s : Computation α} (h : s.Results a 0), s = (pure a).thinkN 0
⊢ s = (pure a).thinkN n
have succ : ∀ (n : ℕ) (IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n) {s : Computation α}
  (h : s.Results a (n + 1)), s = (pure a).thinkN (n + 1)
Tactic: induction n generalizing s with | zero | succ n IH
Cleared hypotheses: s, n, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
s : Computation α
h : s.Results a 0
⊢ s = (pure a).thinkN 0
have zero : ∀ (a' : α) (h : (pure a').Results a 0), pure a' = (pure a).thinkN 0
Tactic: induction s using recOn with | pure a' | think s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
s : Computation α
h : s.Results a 0
zero : ∀ (a' : α) (h : (pure a').Results a 0), pure a' = (pure a).thinkN 0
⊢ s = (pure a).thinkN 0
have zero₁ : ∀ (s : Computation α) (h : s.think.Results a 0), s.think = (pure a).thinkN 0
Tactic: induction s using recOn with | pure a' | think s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
s : Computation α
h : s.Results a (n + 1)
⊢ s = (pure a).thinkN (n + 1)
have succ : ∀ (a' : α) (h : (pure a').Results a (n + 1)), pure a' = (pure a).thinkN (n + 1)
Tactic: induction s using recOn with | pure a' | think s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
s : Computation α
h : s.Results a (n + 1)
succ : ∀ (a' : α) (h : (pure a').Results a (n + 1)), pure a' = (pure a).thinkN (n + 1)
⊢ s = (pure a).thinkN (n + 1)
have succ₁ : ∀ (s : Computation α) (h : s.think.Results a (n + 1)), s.think = (pure a).thinkN (n + 1)
Tactic: induction s using recOn with | pure a' | think s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a' = (pure a).thinkN 0
have zero : pure a = (pure a).thinkN 0
Tactic: rw [← eq_of_pure_mem h.mem]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
⊢ s.think = (pure a).thinkN 0
have zero : ∀ (n : ℕ) (h : s.Results a n ∧ 0 = n + 1), s.think = (pure a).thinkN 0
Tactic: obtain ⟨n, h⟩ := of_results_think h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
a : α
s : Computation α
h_1 : s.think.Results a 0
n : ℕ
h : s.Results a n ∧ 0 = n + 1
⊢ s.think = (pure a).thinkN 0
have left : s.Results a n
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
a : α
s : Computation α
h_1 : s.think.Results a 0
n : ℕ
h : s.Results a n ∧ 0 = n + 1
left : s.Results a n
⊢ s.think = (pure a).thinkN 0
have right : 0 = n + 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
a' : α
h : (pure a').Results a (n + 1)
⊢ pure a' = (pure a).thinkN (n + 1)
have this : n + 1 = 0
Tactic: have := h.len_unique (results_pure _)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)
have succ : ((pure a).thinkN n).think = (pure a).thinkN (n + 1)
Tactic: rw [IH (results_think_iff.1 h)]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
⊢ C s
have haveI : (T : s.Terminates) → C s
Tactic: haveI T := terminates_of_mem M
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C s
have rw : C ((pure a).thinkN s.length)
Tactic: rw [eq_thinkN' s, get_eq_of_mem s M]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure a).thinkN s.length)
have generalize : (n : ℕ) → C ((pure a).thinkN n)
Tactic: generalize length s = n