awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s : WSeq α
s1 s2 : Computation ℕ
l : List α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, nil) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, nil))
⊢ Computation.BisimO
    (fun (c1 c2 : Computation ℕ) ↦
      ∃ (l : List α) (s : WSeq α),
        c1 =
            Computation.corec
              (fun (x : ℕ × WSeq α) ↦
                match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                | (n, s) =>
                  match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map (α := List α) List.length
              (Computation.corec
                (fun (x : List α × WSeq α) ↦
                  match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                  | (l, s) =>
                    match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.destruct
      (Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, nil)))
    (Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, nil))).destruct

Tactic:
simp [nil]

Premises used: Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, cons a s))
⊢ Eq (α := Computation ℕ)
    (Computation.corec
      (fun (x : ℕ × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length + 1, s))
    (Computation.corec
      (fun (x : ℕ × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      ((a :: l).length, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, cons a s))
⊢ Computation.map (α := List α) List.length
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (a :: l, s)) =
    Computation.map (α := List α) List.length
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (a :: l, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, cons a s))
⊢ Computation.BisimO
    (fun (c1 c2 : Computation ℕ) ↦
      ∃ (l : List α) (s : WSeq α),
        c1 =
            Computation.corec
              (fun (x : ℕ × WSeq α) ↦
                match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                | (n, s) =>
                  match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map (α := List α) List.length
              (Computation.corec
                (fun (x : List α × WSeq α) ↦
                  match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                  | (l, s) =>
                    match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.destruct
      (Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s)))
    (Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, cons a s))).destruct

Tactic:
simpa using ⟨a::l, s, by simp, by simp⟩
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))
⊢ Eq (α := Computation ℕ)
    (Computation.corec
      (fun (x : ℕ × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length, s))
    (Computation.corec
      (fun (x : ℕ × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))
⊢ Computation.map (α := List α) List.length
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (l, s)) =
    Computation.map (α := List α) List.length
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (l, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Defs
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))
⊢ Computation.BisimO
    (fun (c1 c2 : Computation ℕ) ↦
      ∃ (l : List α) (s : WSeq α),
        c1 =
            Computation.corec
              (fun (x : ℕ × WSeq α) ↦
                match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                | (n, s) =>
                  match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map (α := List α) List.length
              (Computation.corec
                (fun (x : List α × WSeq α) ↦
                  match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                  | (l, s) =>
                    match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.destruct
      (Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think)))
    (Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))).destruct

Tactic:
simpa using ⟨l, s, by simp, by simp⟩
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
⊢ s.Productive ↔ ∀ (n : ℕ), (s.get? n).Terminates

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

Premises used: Stream'.WSeq.Productive.mk, Stream'.WSeq.Productive.get?_terminates, Iff.intro
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
h : s.Productive
⊢ ∀ (n : ℕ), (s.get? n).Terminates

Tactic:
h.get?_terminates

Premises used: Stream'.WSeq.Productive.get?_terminates
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
⊢ s.head.Terminates

Tactic:
s.get?_terminates 0

Premises used: Stream'.WSeq.drop, Stream'.WSeq.get?, Stream'.WSeq.get?_terminates, OfNat.ofNat
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
rw : (s.get? (n + 1)).Terminates
⊢ (s.tail.get? n).Terminates

Tactic:
rw [get?_tail]

Premises used: Stream'.WSeq.get?_tail
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
⊢ (s.get? (n + 1)).Terminates

Tactic:
infer_instance
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n m : ℕ
rw : (s.get? (n + m)).Terminates
⊢ ((s.drop n).get? m).Terminates

Tactic:
rw [← get?_add]

Premises used: Stream'.WSeq.get?_add
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n m : ℕ
⊢ (s.get? (n + m)).Terminates

Tactic:
infer_instance
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
n : ℕ
rw : (Computation.pure (s.get? n)).Terminates
⊢ ((↑s : WSeq α).get? n).Terminates

Tactic:
rw [get?_ofSeq]

Premises used: Stream'.WSeq.get?_ofSeq
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (Computation.pure (s.get? n)).Terminates

Tactic:
infer_instance
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
simp : (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates
⊢ s.Productive ↔ t.Productive

Tactic:
simp only [productive_iff]

Premises used: Stream'.WSeq.productive_iff
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates

Tactic:
forall_congr' fun n => terminates_congr <| get?_congr h _

Premises used: Stream'.WSeq.get?_congr, forall_congr', Computation.terminates_congr
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates

Tactic:
exact forall_congr' fun n => terminates_congr <| get?_congr h _

Premises used: Stream'.WSeq.get?_congr, forall_congr', Computation.terminates_congr
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) n) Option.none
none :
  ∀ (e : (s.get? (n + 1)).get = Option.none),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) Option.none
some :
  ∀ (val : α) (e : (s.get? (n + 1)).get = Option.some val),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) Option.none
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) Option.none

Tactic:
cases e : Computation.get (get? s (n + 1))

Premises used: Stream'.WSeq.get?, HAdd.hAdd, OfNat.ofNat, Computation.get
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) n) none
e : (s.get? (n + 1)).get = none
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none

Tactic:
assumption
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) n) none
val : α
e : (s.get? (n + 1)).get = some val
⊢ some val ∈ s.get? (n + 1)

Tactic:
have := Computation.mem_of_get_eq _ e
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val : α
e : (s.get? (n + 1)).get = Option.some val
this : Option.some val ∈ (s.drop (n + 1)).head
some :
  ∀ (a' : α) (h' : Option.some a' ∈ (s.drop n).head),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none

Tactic:
obtain ⟨a', h'⟩ := head_some_of_head_tail_some this

Premises used: Stream'.WSeq.head_some_of_head_tail_some
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val : α
e : (s.get? (n + 1)).get = some val
this : some val ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
⊢ some a' = none

Tactic:
have := mem_unique h' (@Computation.mem_of_get_eq _ _ _ _ h)
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val : α
e : (s.get? (n + 1)).get = some val
this_1 : some val ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
this : some a' = none
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none

Tactic:
contradiction
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
a : (↑(↑s : WSeq α).toSeq : Stream' (Option α)) = (↑s : Stream' (Option α))
⊢ (↑s : WSeq α).toSeq = s

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
a : ∀ (n : ℕ), (↑(↑s : WSeq α).toSeq : Stream' (Option α)) n = (↑s : Stream' (Option α)) n
⊢ (↑(↑s : WSeq α).toSeq : Stream' (Option α)) = (↑s : Stream' (Option α))

Tactic:
funext n
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
n : ℕ
a : s.get? n ∈ (↑s : WSeq α).get? n
⊢ ((↑s : WSeq α).get? n).get = s.get? n

Tactic:
apply get_eq_of_mem

Premises used: Computation.get_eq_of_mem
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
n : ℕ
a : s.get? n ∈ Computation.pure (s.get? n)
⊢ s.get? n ∈ (↑s : WSeq α).get? n

Tactic:
rw [get?_ofSeq]

Premises used: Stream'.WSeq.get?_ofSeq
-- Module: Mathlib.Data.WSeq.Productive
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n ∈ Computation.pure (s.get? n)

Tactic:
apply ret_mem

Premises used: Computation.ret_mem
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C D : WSeq α → WSeq β → Prop
H : ∀ (s : WSeq α) (t : WSeq β), C s t → D s t
o : Option (α × WSeq α)
p : Option (β × WSeq β)
⊢ LiftRelO R C o p → LiftRelO R D o p

Tactic:
LiftRelO.imp (fun _ _ => id) H

Premises used: id, Stream'.WSeq.LiftRelO.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
h :
  ∀ (x : Option (β × WSeq β)) (y : Option (α × WSeq α)),
    Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) x y =
      LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) x y
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C)

Tactic:
funext x y