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

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

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

Tactic:
·

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

Goal state before:
pp: case succ.pure
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
a' : α
h : (pure a').Results a (n + 1)
⊢ pure a' = (pure a).thinkN (n + 1)

pp: case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)

Tactic:
·

Goal state after:
case succ.pure
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
a' : α
h : (pure a').Results a (n + 1)
⊢ pure a' = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)

Tactic:
·

Goal state after:
case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Stream.Init

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

Tactic:
·

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

Goal state before:
pp: case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1

pp: case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
·

Goal state after:
case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Computation

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

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)) (s (n + 1)) = some b

Tactic:
·

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

Goal state before:
pp: case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
·

Goal state after:
case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none

pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none

Tactic:
·

Goal state after:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none
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)) (s (n + 1)) = 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)) (s (n + 1)) = some b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none

Tactic:
·

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
·

Goal state after:
case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
·

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
by_cases h : s.Terminates
  · simpa [length'_of_terminates h] using length_le_iff
  · simpa [length'_of_not_terminates h] using forall_not_of_not_exists h n

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

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none

pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
·

Goal state after:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
·

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

Tactic:
·

Goal state after:
case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

Tactic:
·

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case bisim
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)

pp: case r
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))

Tactic:
·

Goal state after:
case bisim
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
s : Stream' α
⊢ s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0

pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)

Tactic:
·

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

Goal state before:
pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)

Tactic:
·

Goal state after:
case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case r
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))

Tactic:
·

Goal state after:
case r
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
⊢ nats.get 0 = (0 :: map succ nats).get 0

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

Tactic:
·

Goal state after:
case zero
⊢ nats.get 0 = (0 :: map succ nats).get 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s

pp: case r
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1

Tactic:
·

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ k < k + 1 + l

Tactic:
by lia

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

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1

Tactic:
·

Goal state after:
case r
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g

pp: case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x ↦ (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x ↦ (f x).bind g) = s_1.bind fun x ↦ (f x).bind g

Tactic:
·

Goal state after:
case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x ↦ (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x ↦ (f x).bind g) = s_1.bind fun x ↦ (f x).bind g

Tactic:
·

Goal state after:
case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x ↦ (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x ↦ (f x).bind g) = s_1.bind fun x ↦ (f x).bind g
Module: Mathlib.Data.Seq.Computation

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

pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)

Tactic:
·

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

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

Tactic:
·

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.dens m = g.dens n

Tactic:
by
  simp only [den_eq_conts_b, conts_stable_of_terminated n_le_m terminatedAt_n]

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

Goal state before:
pp: case nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) 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),
    nil.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

pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (cons x✝ s✝).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) 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),
    (cons x✝ 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:
case nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) 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),
    nil.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: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (cons x✝ s✝).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) 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),
    (cons x✝ 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:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (cons x✝ s✝).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) 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),
    (cons x✝ 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.Computation

Goal state before:
pp: case zero.pure
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ ∃ a_1 m n, (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m

pp: case zero.think
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ ∃ a m n, s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

pp: case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

pp: case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
·

Goal state after:
case zero.pure
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ ∃ a_1 m n, (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m
Module: Mathlib.Data.Seq.Basic

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

pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) ((cons x✝ s✝).append nil).destruct (cons x✝ s✝).destruct

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case zero.think
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ ∃ a m n, s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

pp: case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

pp: case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
·

Goal state after:
case zero.think
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ ∃ a m n, s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim
α : Type u
s t u : Seq α
⊢ IsBisimulation fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)

pp: case r
α : Type u
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
·

Goal state after:
case bisim
α : Type u
s t u : Seq α
⊢ IsBisimulation fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

pp: case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
·

Goal state after:
case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m