mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)

Tactic:
;

Goal state after:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (corecOn (s₁, s₂)
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      fun x ↦
      match x with
      | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (corecOn (s₁, s₂)
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      fun x ↦
      match x with
      | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
    Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
    Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head :: corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) (s₂, s₁.tail) = s₁.head :: s₂.head :: t

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head :: corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) (s₂, s₁.tail) = s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'
⊢ (match
        (match Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)).snd with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'

Tactic:
;

Goal state after:
case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'
⊢ (match
        (match Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)).snd with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ -1 = -1

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ -1 = -1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x ↦
            match x with
            | (s₁, snd) => s₁.head)
          (fun x ↦
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x ↦
            match x with
            | (s₁, snd) => s₁.head)
          (fun x ↦
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inl
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inl a) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inl a with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
;

Goal state after:
case inl
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inl a) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inl a with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Tactic:
;

Goal state after:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩ = ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Tactic:
;

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩ = ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct

Tactic:
;

Goal state after:
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inr
α : 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')

Tactic:
;

Goal state after:
case inr
α : 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')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s ↦ s.tail.tail) s

Tactic:
;

Goal state after:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s ↦ s.tail.tail) s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ s.get? n = none ↔ (s.get? n).isNone = true

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ s.get? n = none ↔ (s.get? n).isNone = true
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case mk
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s' : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R ⟨val✝, property✝⟩ s'
this : head ⟨val✝, property✝⟩ = s'.head ∧ R (tail ⟨val✝, property✝⟩) s'.tail
r : R (tail ⟨val✝, property✝⟩) s'.tail
⊢ (tail ⟨val✝, property✝⟩).val = ⟨val✝, property✝⟩.val.tail

Tactic:
;

Goal state after:
case mk
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s' : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R ⟨val✝, property✝⟩ s'
this : head ⟨val✝, property✝⟩ = s'.head ∧ R (tail ⟨val✝, property✝⟩) s'.tail
r : R (tail ⟨val✝, property✝⟩) s'.tail
⊢ (tail ⟨val✝, property✝⟩).val = ⟨val✝, property✝⟩.val.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case mk
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ (tail ⟨val✝, property✝⟩).val = ⟨val✝, property✝⟩.val.tail

Tactic:
;

Goal state after:
case mk
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ (tail ⟨val✝, property✝⟩).val = ⟨val✝, property✝⟩.val.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = 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

Tactic:
;

Goal state after:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = 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
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s).get k
⊢ C s

Tactic:
;

Goal state after:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s).get k
⊢ C s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
;

Goal state after:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mk
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
e : some a = ↑(cons b ⟨val✝, property✝⟩) (k + 1)
⊢ ↑(cons b ⟨val✝, property✝⟩) k.succ = ↑⟨val✝, property✝⟩ k

Tactic:
;

Goal state after:
case mk
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
e : some a = ↑(cons b ⟨val✝, property✝⟩) (k + 1)
⊢ ↑(cons b ⟨val✝, property✝⟩) k.succ = ↑⟨val✝, property✝⟩ k
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)

Tactic:
;

Goal state after:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)

Tactic:
;

Goal state after:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail

Tactic:
tail_pure,

Goal state after:
case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r') (pure a').tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r') (pure a').tail

Tactic:
tail_pure,

Goal state after:
case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r') (pure a')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n

Tactic:
;

Goal state after:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
n : ℕ
h : (x ++ₛ a).get (x.length + n) = (x ++ₛ b).get (x.length + n)
⊢ a.get n = b.get n

Tactic:
;

Goal state after:
α : Type u
x : List α
a b : Stream' α
n : ℕ
h : (x ++ₛ a).get (x.length + n) = (x ++ₛ b).get (x.length + n)
⊢ a.get n = b.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s

Tactic:
Nat.zero_min,

Goal state after:
α : Type u
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take 0 s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ some (take (n✝ + 1) s)[0] = some (s.get 0)

Tactic:
;

Goal state after:
α : Type u
s : Stream' α
n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ some (take (n✝ + 1) s)[0] = some (s.get 0)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s

Tactic:
exact ⟨n', h⟩

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
H : ¬s.Terminates
⊢ s.val = (empty α).val

Tactic:
;

Goal state after:
α : Type u
s : Computation α
H : ¬s.Terminates
⊢ s.val = (empty α).val
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : s.val n = none
⊢ none = (empty α).val n

pp: case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ some val✝ = (empty α).val n

Tactic:
;

Goal state after:
case none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : s.val n = none
⊢ none = (empty α).val n

case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ some val✝ = (empty α).val n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m

Tactic:
;

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ s.Terminates

Tactic:
;

Goal state after:
case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ s.Terminates
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s

Tactic:
;

Goal state after:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]

Tactic:
;

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s

Tactic:
;

Goal state after:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length

Tactic:
;

Goal state after:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this : s.Terminates
⊢ m = n

Tactic:
;

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

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ m = n

Tactic:
;

Goal state after:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ m = n
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val s.think.length).isSome = true → s.length + 1 ≤ s.think.length

Tactic:
;

Goal state after:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val s.think.length).isSome = true → s.length + 1 ≤ s.think.length
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n

Tactic:
;

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n