awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
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 (Sum.inr r') (Sum.inl a')
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

Tactic:
exact False.elim h

Premises used: False.elim
-- Module: Mathlib.Data.Seq.Computation
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' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail

Tactic:
simp_all
-- Module: Mathlib.Data.Seq.Computation
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'
⊢ t₁.head = t₂.head ∧
    ∃ (s : Computation α),
      ∃ (s' : Computation α),
        s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₁.tail ∧
          s'.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) = t₂.tail ∧
            R s s'

Tactic:
match t₁, t₂, e with
    | _, _, ⟨s, s', rfl, rfl, r⟩ =>
      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
      have h := bisim r; revert r h
      refine recOn s ?_ ?_ <;> intro r' <;> refine recOn s' ?_ ?_ <;> intro a' r h
      · constructor <;> dsimp at h
        · rw [h]
        · rw [h] at r
          rw [tail_pure, tail_pure, h]
          assumption
      · rw [destruct_pure, destruct_think] at h
        exact False.elim h
      · rw [destruct_pure, destruct_think] at h
        exact False.elim h
      · simp_all
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ (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:
⟨s₁, s₂, rfl, rfl, r⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ (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:
exact ⟨s₁, s₂, rfl, rfl, r⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
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
⊢ 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

Tactic:
obtain ⟨f, al⟩ := s
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
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) m =
      some a

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
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) m =
      some a

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
m_1 : ℕ
h : 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:
fun h2 ↦ al (IH h2)
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
m_1 : ℕ
h : 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:
exact fun h2 ↦ al (IH h2)
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ 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:
induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)

Premises used: id, refl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a b : α
m : ℕ
ha :
  (fun (b : Option α) ↦ some a = b)
    (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get m)
n : ℕ
hb :
  (fun (b_1 : Option α) ↦ some b = b_1)
    (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get n)
⊢ a = b

Tactic:
injection
      (le_stable s (le_max_left m n) ha.symm).symm.trans (le_stable s (le_max_right m n) hb.symm)

Premises used: le_max_right, Computation.le_stable, Eq.symm, le_max_left, Eq.trans
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ Relator.LeftUnique fun (x1 : α) (x2 : Computation α) ↦ x1 ∈ x2

Tactic:
fun _ _ _ =>
  mem_unique

Premises used: Computation.mem_unique, Relator.LeftUnique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
⊢ s.Terminates ↔ ∃ (a : α), a ∈ s

Tactic:
⟨fun h => h.1, Terminates.mk⟩

Premises used: Computation.Terminates.mk, Computation.Terminates.term, Iff.intro
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
h : a ∈ s
⊢ s.Terminates

Tactic:
⟨⟨a, h⟩⟩

Premises used: Computation.Terminates.mk, Exists.intro
-- Module: Mathlib.Data.Seq.Computation
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
rw : (some a).isSome = true
⊢ (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n).isSome = true

Tactic:
rw [← h]
-- Module: Mathlib.Data.Seq.Computation
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
⊢ (some a).isSome = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Computation
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
⊢ (some a).isSome = true

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ a ∈ pure a

Tactic:
Exists.intro 0 rfl

Premises used: Computation.Mem, Exists.intro, OfNat.ofNat, rfl, Stream'.Any
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a a' : α
h : a' ∈ pure a
⊢ a' = a

Tactic:
mem_unique h (ret_mem _)

Premises used: Computation.mem_unique, Computation.ret_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a b : α
⊢ a ∈ pure b ↔ a = b

Tactic:
⟨eq_of_pure_mem, fun h => h ▸ ret_mem _⟩

Premises used: Eq.rec, Iff.intro, Computation.ret_mem, Computation.eq_of_pure_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
a : α
⊢ (pure a).Terminates

Tactic:
terminates_of_mem (ret_mem _)

Premises used: Computation.terminates_of_mem, Computation.ret_mem
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ a ∈ s

Tactic:
rcases n with - | n'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
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:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
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:
⟨n', h⟩

Premises used: Computation.Mem, Exists.intro, Stream'.Any
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
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:
exact ⟨n', h⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
h_1 : a ∈ empty α
n : ℕ
h :
  (fun (b : Option α) ↦ some a = b)
    ((empty α).val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a).get n)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ ¬(empty α).Terminates

Tactic:
fun ⟨⟨a, h⟩⟩ => notMem_empty a h

Premises used: False, _private.0.Computation.not_terminates_empty.match_1, Computation.notMem_empty, Not
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
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)
⊢ s = empty α

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
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
⊢ 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:
funext n
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ 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:
rcases h : s.val n

Premises used: Subtype.val
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
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:
rfl
-- Module: Mathlib.Data.Seq.Computation
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

Tactic:
absurd ?_ H

Premises used: absurd
-- Module: Mathlib.Data.Seq.Computation
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
a : s.Terminates
⊢ some val = (empty α).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n

Tactic:
refine absurd ?_ H

Premises used: absurd
-- Module: Mathlib.Data.Seq.Computation
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
⊢ s.Terminates

Tactic:
⟨⟨_, _, h.symm⟩⟩

Premises used: Computation.Terminates.mk, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Seq.Computation
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
⊢ s.Terminates

Tactic:
exact ⟨⟨_, _, h.symm⟩⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
⊢ a ∈ s → s ~> a

Tactic:
fun h _ => mem_unique h

Premises used: Computation.mem_unique, Computation.Promises
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ empty α ~> a

Tactic:
fun _ h => absurd h (notMem_empty _)

Premises used: Computation.Promises, absurd, Computation.notMem_empty
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.get ∈ s

Tactic:
Exists.intro (length s) (Option.eq_some_of_isSome _).symm

Premises used: Option.eq_some_of_isSome, Computation.Mem, Computation.length, Exists.intro, Eq.symm, Stream'.Any
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
a : α
⊢ a ∈ s → s.get = a

Tactic:
mem_unique (get_mem _)

Premises used: Computation.mem_unique, Computation.get_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h_1 : s.Terminates
a : α
h : s.get = a
rw : s.get ∈ s
⊢ a ∈ s

Tactic:
rw [← h]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h_1 : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s

Tactic:
apply get_mem

Premises used: Computation.get_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.get = s.get

Tactic:
get_eq_of_mem _ <|
    let ⟨n, h⟩ := get_mem s
    ⟨n + 1, h⟩

Premises used: Computation.think, Membership.mem, Computation.get_mem, Computation.get_eq_of_mem, _private.0.Computation.get_think.match_1, HAdd.hAdd, Exists.intro, OfNat.ofNat, Computation.get
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
⊢ (s.thinkN n).get = s.get

Tactic:
get_eq_of_mem _ <| (thinkN_mem _).2 (get_mem _)

Premises used: Iff.mpr, Computation.get_mem, Computation.thinkN_mem, Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s ~> s.get

Tactic:
fun _ => get_eq_of_mem _

Premises used: Computation.Promises, Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
a : α
p : s ~> a
obtain : ∀ (a' : α) (h : a' ∈ s), a ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨a', h⟩ := h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h rw : a' ∈ s
⊢ a ∈ s

Tactic:
rw [p h]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s

Tactic:
h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s

Tactic:
exact h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
a : α
⊢ s ~> a → s.get = a

Tactic:
get_eq_of_mem _ ∘ mem_of_promises _

Premises used: Function.comp, Computation.get_eq_of_mem, Computation.mem_of_promises
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
_T : s.Terminates
⊢ s.Results s.get s.length

Tactic:
⟨get_mem _, rfl⟩

Premises used: Computation.get_mem, Computation.Results, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
rw : s.Results s.get s.length
⊢ s.Results a s.length

Tactic:
rw [← get_eq_of_mem _ h]

Premises used: Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length

Tactic:
apply results_of_terminates

Premises used: Computation.results_of_terminates
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s.Terminates

Tactic:
terminates_of_mem h.mem

Premises used: Computation.Results.mem, Computation.terminates_of_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ a = b

Tactic:
mem_unique h1.mem h2.mem

Premises used: Computation.mem_unique, Computation.Results.mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ s.Terminates

Tactic:
haveI := h1.terminates
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this : s.Terminates
⊢ s.Terminates

Tactic:
haveI := h2.terminates