mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
⊢ ((pure a).thinkN n).Results a n

Tactic:
;

Goal state after:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
⊢ ((pure a).thinkN n).Results a n
Module: Mathlib.Data.Stream.Init

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

Tactic:
;

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

Goal state before:
pp: case inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ k < (List.drop n x).length

Tactic:
;

Goal state after:
case inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ k < (List.drop n x).length
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a' : α
⊢ Stream'.cycleF (a', [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', [], a, l)) =
    [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
;

Goal state after:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a' : α
⊢ Stream'.cycleF (a', [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', [], a, l)) =
    [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (some a) = some b

Tactic:
;

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (some a) = some b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ ∃ (h : s.Terminates), s.length h ≤ n

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ ∃ (h : s.Terminates), s.length h ≤ n
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (map f (think ⟨s, al⟩)).val = (map f ⟨s, al⟩).think.val

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (map f (think ⟨s, al⟩)).val = (map f ⟨s, al⟩).think.val
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ Stream'.cycleF (a', a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
;

Goal state after:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ Stream'.cycleF (a', a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (f val)) o) (Stream'.cons none s) =
    Stream'.cons none (Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (f val)) o) s)

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (f val)) o) (Stream'.cons none s) =
    Stream'.cons none (Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (f val)) o) s)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h

Tactic:
;

Goal state after:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail

Tactic:
;

Goal state after:
α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ (map id ⟨f, al⟩).val = ⟨f, al⟩.val

Tactic:
;

Goal state after:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ (map id ⟨f, al⟩).val = ⟨f, al⟩.val
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail

Tactic:
;

Goal state after:
α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (map (g ∘ f) ⟨s, al⟩).val = (map g (map f ⟨s, al⟩)).val

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (map (g ∘ f) ⟨s, al⟩).val = (map g (map f ⟨s, al⟩)).val
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)

Tactic:
;

Goal state after:
α : Type u
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s

Tactic:
;

Goal state after:
α : Type u
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
;

Goal state after:
α : Type u
s : Stream' α
⊢ ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n

Tactic:
;

Goal state after:
α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: ⊢ ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n

Tactic:
;

Goal state after:
⊢ ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
n✝ : ℕ
⊢ nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)

Tactic:
;

Goal state after:
case succ
n✝ : ℕ
⊢ nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
⊢ match ((f s).bind g).destruct, ((f s).bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False

Tactic:
;

Goal state after:
case pure
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
⊢ match ((f s).bind g).destruct, ((f s).bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure.pure
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
t : β
⊢ match (g t).destruct, (g t).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False

Tactic:
;

Goal state after:
case pure.pure
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
t : β
⊢ match (g t).destruct, (g t).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a✝ : α
⊢ (↑(s.toList h)).get? n = some a✝ ↔ s.get? n = some a✝

Tactic:
;

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a✝ : α
⊢ (↑(s.toList h)).get? n = some a✝ ↔ s.get? n = some a✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
i✝ : ℕ
a✝ : α
⊢ (nil.toList ⋯)[i✝]? = some a✝ ↔ [][i✝]? = some a✝

Tactic:
;

Goal state after:
α : Type u
i✝ : ℕ
a✝ : α
⊢ (nil.toList ⋯)[i✝]? = some a✝ ↔ [][i✝]? = some a✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (cons a s, t)).destruct =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))

Tactic:
;

Goal state after:
α : Type u
a : α
s t : Seq α
⊢ (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (cons a s, t)).destruct =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : s.Results a m
h2 : (f a).Results b n
this : a ∈ s
⊢ (s.bind f).Results b (n + m)

Tactic:
;

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : s.Results a m
h2 : (f a).Results b n
this : a ∈ s
⊢ (s.bind f).Results b (n + m)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ (match
      match (cons a s).destruct with
      | none =>
        match t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b)) =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))

Tactic:
;

Goal state after:
α : Type u
a : α
s t : Seq α
⊢ (match
      match (cons a s).destruct with
      | none =>
        match t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b)) =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ match
    (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (nil, s)).destruct,
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
;

Goal state after:
α : Type u
s✝ s : Seq α
⊢ match
    (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (nil, s)).destruct,
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
⊢ ∏ i ∈ Finset.range (n + 1), -1 = (-1) ^ (n + 1)

Tactic:
rw [Finset.prod_const, Finset.card_range]

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

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'

Tactic:
;

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h this : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h this : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h✝ : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h✝ : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ ((empty α).think <|> s) = (empty α <|> s)

Tactic:
;

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ ((empty α).think <|> s) = (empty α <|> s)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> (empty α).think) = (s <|> empty α)

Tactic:
;

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> (empty α).think) = (s <|> empty α)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Tactic:
;

Goal state after:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s

Tactic:
;

Goal state after:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 ↦ x1 = x2) a b
⊢ a ∈ c₂

Tactic:
;

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 ↦ x1 = x2) a b
⊢ a ∈ c₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ s'✝.append s₂
⊢ a ∈ (cons b✝ s'✝).append s₂

Tactic:
;

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ s'✝.append s₂
⊢ a ∈ (cons b✝ s'✝).append s₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ a ∈ c₁

Tactic:
;

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ a ∈ c₁
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (cons a ⟨s, al⟩)) = ↑(cons (f a) (map f ⟨s, al⟩))

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (cons a ⟨s, al⟩)) = ↑(cons (f a) (map f ⟨s, al⟩))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'