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
⊢ x[n + k] = x[n + k]

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

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
⊢ n + k < 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.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

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.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.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
⊢ (take n.succ.succ s₂)[n.succ]? = (take n.succ.succ s₂)[n.succ]?

Tactic:
]

Goal state after:
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.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.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.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'.cons (Option.rec none (fun val ↦ some (f val)) none)
      (Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (f val)) o) s) =
    Stream'.cons none (Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (f val)) o) s)

Tactic:
]

Goal state after:
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
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr ([a] ++ₛ cycle [a] ⋯).tail = fr (a :: const a).tail

Tactic:
]

Goal state after:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr ([a] ++ₛ cycle [a] ⋯).tail = fr (a :: const a).tail
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.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
⊢ drop n s.tail.tail = drop n s.tail.tail

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ ∃ a, s.get? n = some a

Tactic:
]

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ ∃ a, s.get? n = some a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ (s.get? n).isSome = true

Tactic:
]

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ (s.get? n).isSome = true
Module: Mathlib.Data.Seq.Basic

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

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
l : List α
s : Stream' α
⊢ (match (l, s) with
      | (a, snd) => a) ::
      corec
        (fun x ↦
          match x with
          | (a, snd) => a)
        (fun p ↦
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (match (l, s) with
        | (l', s') => (l' ++ [s'.head], s'.tail)) =
    l ::
      corec
        (fun x ↦
          match x with
          | (a, snd) => a)
        (fun p ↦
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)

Tactic:
]

Goal state after:
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.Seq.Computation

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

Tactic:
apply
    eq_of_bisim fun c₁ c₂ => c₁ = bind (pure a) f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)

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₂)

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.Seq.Basic

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
]

Goal state after:
α : Type u
n k : ℕ
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then (cons x r).get? n else none

Tactic:
]

Goal state after:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then (cons x r).get? n else none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)

Tactic:
]

Goal state after:
case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
⊢ (initsCore [s.head, s.tail.head] s.tail.tail).get n = (initsCore [s.head, s.tail.head] s.tail.tail).get n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = s.head :: take n✝.succ s.tail

Tactic:
]

Goal state after:
case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = s.head :: take n✝.succ s.tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match (cons x s.tail).destruct with
    | none => []
    | some (x, r) => x :: take l r

Tactic:
]

Goal state after:
case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match (cons x s.tail).destruct with
    | none => []
    | some (x, r) => x :: take l r
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.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.s.get? n = none ↔ g.s.get? n = none

Tactic:
]

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

Goal state before:
pp: case succ
α : 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
⊢ x ∈
    match (cons y s.tail).destruct with
    | none => []
    | some (x, r) => x :: take (k + 1 + l) r

Tactic:
]

Goal state after:
case succ
α : 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
⊢ x ∈
    match (cons y s.tail).destruct with
    | none => []
    | some (x, r) => x :: take (k + 1 + l) r
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : 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
⊢ s.get? (k + 1) = some x

Tactic:
]

Goal state after:
case succ
α : 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
⊢ s.get? (k + 1) = some x
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1

Tactic:
]

Goal state after:
case succ
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (match (fun a' ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r).length =
    n + 1

Tactic:
]

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (match (fun a' ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r).length =
    n + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
⊢ n = n

pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
⊢ ∀ (h : s.tail.Terminates), n ≤ s.tail.length h

Tactic:
]

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
⊢ ∀ (h : s.tail.Terminates), n ≤ s.tail.length h
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: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s).get (m + 1) = none
this : ∃ a, a ∈ none
⊢ False

Tactic:
]

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s).get (m + 1) = none
this : ∃ a, a ∈ none
⊢ False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ s.length h = s.length h

pp: α : Type u
s : Seq α
h : s.Terminates
⊢ ∀ (h_1 : s.Terminates), s.length h ≤ s.length h_1

Tactic:
]

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
⊢ ∀ (h_1 : s.Terminates), s.length h ≤ s.length h_1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ s.get? (s.length h - 1) = s.get? (s.length h - 1)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b } =
    { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
]

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

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ omap
      (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))
      (match (cons a s, t).1.destruct with
      | none =>
        match (cons a s, t).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)) =
    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 α
⊢ omap
      (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))
      (match (cons a s, t).1.destruct with
      | none =>
        match (cons a s, t).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)) =
    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.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
⊢ { a := gp.b * predConts.a + gp.a * ppredConts.a, b := gp.b * predConts.b + gp.a * ppredConts.b }.a =
    gp.b * predConts.a + gp.a * ppredConts.a

Tactic:
]

Goal state after:
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✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).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✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).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
m✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).Results b (n + 0)

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✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).Results b (n + 0)
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
⊢ { a := gp.b * predConts.a + gp.a * ppredConts.a, b := gp.b * predConts.b + gp.a * ppredConts.b }.b =
    gp.b * predConts.b + gp.a * ppredConts.b

Tactic:
]

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

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ (match
      match some (a, s) 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:
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? n = none
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
]

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? n = none
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this :
  (match s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
]

Goal state after:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this :
  (match s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
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 α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
⊢ (s✝.bind f).think.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 α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
⊢ (s✝.bind f).think.Results b (n + m✝)
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 ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ C z = C z

Tactic:
]

Goal state after: