mathlib-initiative/mathlib-tactics huggingface dataset:
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⟩) = (map f ⟨s, al⟩).think

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
δ : Type w
m n : ℕ
x y : List α
a✝ b : Stream' α
a : α
⊢ [a] ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Computation α
⊢ (map f s).destruct = lmap f (rmap (map f) s.destruct)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ Option.rec none some = id

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.tails.get n = drop n s.tail

Tactic:
by

Goal state after:
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⟩ = ⟨f, al⟩

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)
x' y' : FreeCommRing ((i : ι) × G i)
i : ι
x : G i
hx :
  (of G f i) x =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      x'
j : ι
y : G j
hy :
  (of G f j) y =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      y'
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of G f k) (f i k hik x + f j k hjk y) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (x' + y')

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ (↑l).TerminatedAt l.length

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ take n nil = []

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ take 0 s = []

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
s : Seq α
⊢ take (n + 1) (cons x s) = x :: take n s

Tactic:
by

Goal state after:
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⟩ = map g (map f ⟨s, al⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
s : Seq α
⊢ (take 0 s)[n]? = if n < 0 then s.get? n else none

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
n : ℕ
l : List α
s : Stream' α
⊢ a :: (initsCore l s).get n = (initsCore (a :: l) s).get n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.inits.get n = take n.succ s

Tactic:
by

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

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
⊢ (take (k + 1) s)[n]? = if n < k + 1 then s.get? n else none

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Stream' α
⊢ zip appendStream' s.inits s.tails = const s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
c : Computation α
f : α → Computation β
⊢ (c.think.bind f).destruct = Sum.inr (c.bind f)

Tactic:
by

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

Goal state before:
pp: ⊢ nats = 0 :: map succ nats

Tactic:
by

Goal state after:
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, s.get? 0 = some y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.TerminatedAt n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partNums.get? n = some gp.a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partDens.get? n = some gp.b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
a : α
nth_partNum_eq : g.partNums.get? n = some a
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.a = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
b : α
nth_partDen_eq : g.partDens.get? n = some b
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.b = b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
A : K
nth_num_eq : g.nums n = A
⊢ ∃ conts, g.conts n = conts ∧ conts.a = A

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
B : K
nth_denom_eq : g.dens n = B
⊢ ∃ conts, g.conts n = conts ∧ conts.b = B

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs 0 = g.h

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.nums 1 = gp.b * g.h + gp.a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.dens 1 = gp.b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' 0 = g.h

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
h : s.head = none
n : ℕ
⊢ convs'Aux s (n + 1) = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
p : Pair K
h : s.head = some p
n : ℕ
⊢ convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n)

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
m n : ℕ
h_mn : m < n
x : α
h_get : s.get? m = some x
⊢ x ∈ take n s

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Computation α
⊢ s.bind pure = s

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (take n s).length ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
hle : ∀ (h : s.Terminates), n ≤ s.length h
⊢ (take n s).length = n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
n : ℕ
⊢ (s.toList h)[n]? = s.get? n

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ ↑(s.toList h) = s

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ ↑((↑l).toList ⋯) = ↑l

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ nil.toList ⋯ = []

Tactic:
by

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

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

Tactic:
by

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
⊢ g.contsAux (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
by

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

Goal state before:
pp: α : 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

Tactic:
by

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
⊢ g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
by

Goal state after:
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)
x' y' : FreeCommRing ((i : ι) × G i)
i : ι
x : G i
hx :
  (of G f i) x =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      x'
j : ι
y : G j
hy :
  (of G f j) y =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      y'
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of G f k) (f i k hik x * f j k hjk y) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (x' * y')

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_num_eq : g.nums n = ppredA
succ_nth_num_eq : g.nums (n + 1) = predA
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredA

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_den_eq : g.dens n = ppredB
succ_nth_den_eq : g.dens (n + 1) = predB
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredB

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ ((cons a s).append t).destruct = some (a, s.append t)

Tactic:
by

Goal state after:
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 : DirectLimit G f
⊢ ∃ i x, (of G f i) x = z

Tactic:
by

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.TerminatedAt n
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux m = g.contsAux (n + 1)

Tactic:
by

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

Goal state before:
pp: 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
⊢ s.tail.TerminatedAt n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s (n + 1) = convs'Aux s n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s m = convs'Aux s n

Tactic:
by

Goal state after:
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.conts m = g.conts n

Tactic:
by

Goal state after:
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.nums m = g.nums n

Tactic:
by

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

Goal state after:
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
⊢ Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) (C x) = C z

Tactic:
by

Goal state after:
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.convs m = g.convs n

Tactic:
by

Goal state after:
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.convs' m = g.convs' n

Tactic:
by

Goal state after:
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
⊢ (s.bind f).Results b (n + m)

Tactic:
by

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

Goal state before:
pp: case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
⊢ pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
change pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Goal state after:
case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ nil.append s = s

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.append nil = s

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
by

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

Goal state before:
pp: α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ u = (nil.append nil).append u

Tactic:
by

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

Goal state before:
pp: α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ u = nil.append (nil.append u)

Tactic:
by

Goal state after: