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

Goal state before:
pp: case zero.inl
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val✝ : α
⊢ (Corec.f f (Sum.inl val✝)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'

pp: case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
⊢ (Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'

Tactic:
<;>

Goal state after:
case zero.inl
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val✝ : α
⊢ (Corec.f f (Sum.inl val✝)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'

case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
⊢ (Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inr.inl.nil
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
ih : motive nil nil
⊢ nil = nil ∧ nil = nil ∨ ∃ x s₁' s₂', nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

pp: case inr.inl.cons
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
x✝ : α
s✝ : Seq α
ih : motive (cons x✝ s✝) (cons x✝ s✝)
⊢ cons x✝ s✝ = nil ∧ cons x✝ s✝ = nil ∨
    ∃ x s₁' s₂', cons x✝ s✝ = cons x s₁' ∧ cons x✝ s✝ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
<;>

Goal state after:
case inr.inl.nil
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
ih : motive nil nil
⊢ nil = nil ∧ nil = nil ∨ ∃ x s₁' s₂', nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

case inr.inl.cons
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
x✝ : α
s✝ : Seq α
ih : motive (cons x✝ s✝) (cons x✝ s✝)
⊢ cons x✝ s✝ = nil ∧ cons x✝ s✝ = nil ∨
    ∃ x s₁' s₂', cons x✝ s✝ = cons x s₁' ∧ cons x✝ s✝ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Computation

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

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

Tactic:
<;>

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

case h_2
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'
x✝ : α ⊕ β
val✝ : β
heq✝ :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).snd =
    Sum.inr val✝
⊢ (match f val✝ with
        | Sum.inl a => some a
        | Sum.inr val => none,
        f val✝).fst =
    some a'
Module: Mathlib.Data.Stream.Init

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

Tactic:
by
    change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n)
    rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons]
    rw [get_interleave_left n (tail s₁) (tail s₂)]
    rfl

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

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

pp: case some
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
val✝ : α
⊢ some val✝ = none ↔ (some val✝).isNone = true

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ none = none ↔ none.isNone = true

case some
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
val✝ : α
⊢ some val✝ = none ↔ (some val✝).isNone = true
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates → s.Terminates

pp: case mpr
α : Type u
x : α
s : Seq α
⊢ s.Terminates → (cons x s).Terminates

Tactic:
<;>

Goal state after:
case mp
α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates → s.Terminates

case mpr
α : Type u
x : α
s : Seq α
⊢ s.Terminates → (cons x s).Terminates
Module: Mathlib.Data.Seq.Computation

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

pp: case refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
⊢ ∀ (s : Computation α),
    R s.think s' → BisimO R s.think.destruct s'.destruct → s.think.head = s'.head ∧ R s.think.tail s'.tail

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
⊢ ∀ (a : α), R (pure a) s' → BisimO R (pure a).destruct s'.destruct → (pure a).head = s'.head ∧ R (pure a).tail s'.tail

case refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
⊢ ∀ (s : Computation α),
    R s.think s' → BisimO R s.think.destruct s'.destruct → s.think.head = s'.head ∧ R s.think.tail s'.tail
Module: Mathlib.Data.Seq.Computation

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

pp: case refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
⊢ R r'.think s' → BisimO R r'.think.destruct s'.destruct → r'.think.head = s'.head ∧ R r'.think.tail s'.tail

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
⊢ R (pure r') s' → BisimO R (pure r').destruct s'.destruct → (pure r').head = s'.head ∧ R (pure r').tail s'.tail

case refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
⊢ R r'.think s' → BisimO R r'.think.destruct s'.destruct → r'.think.head = s'.head ∧ R r'.think.tail s'.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
a : α
l : List α
⊢ (↑(a :: l)).get? 0 = (cons a ↑l).get? 0

pp: case succ
α : Type u
a : α
l : List α
n : ℕ
⊢ (↑(a :: l)).get? (n + 1) = (cons a ↑l).get? (n + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
l : List α
⊢ (↑(a :: l)).get? 0 = (cons a ↑l).get? 0

case succ
α : Type u
a : α
l : List α
n : ℕ
⊢ (↑(a :: l)).get? (n + 1) = (cons a ↑l).get? (n + 1)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
⊢ Option.map f none = none → Option.map f (s (n + 1)) = none

pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e✝ : α
e : s n = some e✝
⊢ Option.map f (some e✝) = none → Option.map f (s (n + 1)) = none

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
⊢ Option.map f none = none → Option.map f (s (n + 1)) = none

case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e✝ : α
e : s n = some e✝
⊢ Option.map f (some e✝) = none → Option.map f (s (n + 1)) = none
Module: Mathlib.Data.Seq.Computation

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case pos
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : i = n
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none

pp: case neg
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : ¬i = n
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : i = n
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none

case neg
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : ¬i = n
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none
Module: Mathlib.Tactic.ENatToNat

Goal state before:
pp: case top
⊢ ¬⊤ < ⊤

pp: case coe
a✝ : ℕ
⊢ ¬⊤ < ↑a✝

Tactic:
<;>

Goal state after:
case top
⊢ ¬⊤ < ⊤

case coe
a✝ : ℕ
⊢ ¬⊤ < ↑a✝
Module: Mathlib.Data.Stream.Init

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

pp: case cons
α : Type u
n : ℕ
x : List α
a : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : (tail✝ ++ₛ a).get (tail✝.length + n) = a.get n
⊢ (head✝ :: tail✝ ++ₛ a).get ((head✝ :: tail✝).length + n) = a.get n

Tactic:
<;>

Goal state after:
case nil
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ ([] ++ₛ a).get ([].length + n) = a.get n

case cons
α : Type u
n : ℕ
x : List α
a : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : (tail✝ ++ₛ a).get (tail✝.length + n) = a.get n
⊢ (head✝ :: tail✝ ++ₛ a).get ((head✝ :: tail✝).length + n) = a.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
s : Stream' α
⊢ (take 0 s).length = 0

pp: case succ
α : Type u
n✝ : ℕ
a✝ : ∀ (s : Stream' α), (take n✝ s).length = n✝
s : Stream' α
⊢ (take (n✝ + 1) s).length = n✝ + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u
s : Stream' α
⊢ (take 0 s).length = 0

case succ
α : Type u
n✝ : ℕ
a✝ : ∀ (s : Stream' α), (take n✝ s).length = n✝
s : Stream' α
⊢ (take (n✝ + 1) s).length = n✝ + 1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case nil
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ [] ++ take n a = take ([].length + n) ([] ++ₛ a)

pp: case cons
α : Type u
n : ℕ
x : List α
a : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ++ take n a = take (tail✝.length + n) (tail✝ ++ₛ a)
⊢ head✝ :: tail✝ ++ take n a = take ((head✝ :: tail✝).length + n) (head✝ :: tail✝ ++ₛ a)

Tactic:
<;>

Goal state after:
case nil
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ [] ++ take n a = take ([].length + n) ([] ++ₛ a)

case cons
α : Type u
n : ℕ
x : List α
a : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ++ take n a = take (tail✝.length + n) (tail✝ ++ₛ a)
⊢ head✝ :: tail✝ ++ take n a = take ((head✝ :: tail✝).length + n) (head✝ :: tail✝ ++ₛ a)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case h
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)

pp: case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take (m + n) a).length = (take m a ++ take n (drop m a)).length

Tactic:
<;>

Goal state after:
case h
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)

case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take (m + n) a).length = (take m a ++ take n (drop m a)).length
Module: Mathlib.Data.Seq.Computation

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

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

Tactic:
<;>

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

case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
⊢ (s.think.val (n + 1)).isSome = true → s.length + 1 ≤ n + 1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case hl
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ (List.map f (take n a)).length = (take n (map f a)).length

pp: case h
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ ∀ (i : ℕ) (h₁ : i < (List.map f (take n a)).length) (h₂ : i < (take n (map f a)).length),
    (List.map f (take n a))[i] = (take n (map f a))[i]

Tactic:
<;>

Goal state after:
case hl
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ (List.map f (take n a)).length = (take n (map f a)).length

case h
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ ∀ (i : ℕ) (h₁ : i < (List.map f (take n a)).length) (h₂ : i < (take n (map f a)).length),
    (List.map f (take n a))[i] = (take n (map f a))[i]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take n (drop m a)).length = (List.drop m (take (m + n) a)).length

pp: case h
α : Type u
m n : ℕ
a : Stream' α
⊢ ∀ (i : ℕ) (h₁ : i < (take n (drop m a)).length) (h₂ : i < (List.drop m (take (m + n) a)).length),
    (take n (drop m a))[i] = (List.drop m (take (m + n) a))[i]

Tactic:
<;>

Goal state after:
case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take n (drop m a)).length = (List.drop m (take (m + n) a)).length

case h
α : Type u
m n : ℕ
a : Stream' α
⊢ ∀ (i : ℕ) (h₁ : i < (take n (drop m a)).length) (h₂ : i < (List.drop m (take (m + n) a)).length),
    (take n (drop m a))[i] = (List.drop m (take (m + n) a))[i]
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
a : α
s : Computation α
h : s.Results a 0
⊢ s = (pure a).thinkN 0

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

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
s : Computation α
h : s.Results a 0
⊢ s = (pure a).thinkN 0

case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.Results a (n + 1)
⊢ s = (pure a).thinkN (n + 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
⊢ 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
⊢ 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
⊢ Option.rec none (fun val ↦ some (f val)) none = some b → Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b

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
⊢ 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 pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1

pp: case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x 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
⊢ (cons x s).length' = s.length' + 1

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case nil
α : Type u
⊢ nil.length' = 0 ↔ nil = nil

pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' = 0 ↔ cons x✝ s✝ = nil

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ nil.length' = 0 ↔ nil = nil

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' = 0 ↔ cons x✝ s✝ = nil
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
⊢ nil.length' ≠ 0 ↔ ∃ x s', nil = cons x s'

pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' ≠ 0 ↔ ∃ x s', cons x✝ s✝ = cons x s'

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ nil.length' ≠ 0 ↔ ∃ x s', nil = cons x s'

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' ≠ 0 ↔ ∃ x s', cons x✝ s✝ = cons x s'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
β : Type v
f : α → β
a✝ : α
⊢ (map f (pure a✝)).destruct = lmap f (rmap (map f) (pure a✝).destruct)

pp: case think
α : Type u
β : Type v
f : α → β
s✝ : Computation α
⊢ (map f s✝.think).destruct = lmap f (rmap (map f) s✝.think.destruct)

Tactic:
<;>

Goal state after:
case pure
α : Type u
β : Type v
f : α → β
a✝ : α
⊢ (map f (pure a✝)).destruct = lmap f (rmap (map f) (pure a✝).destruct)

case think
α : Type u
β : Type v
f : α → β
s✝ : Computation α
⊢ (map f s✝.think).destruct = lmap f (rmap (map f) s✝.think.destruct)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
a✝ : α
⊢ Option.rec none some none = some a✝ ↔ id none = some a✝

pp: case some
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
val✝ a✝ : α
⊢ Option.rec none some (some val✝) = some a✝ ↔ id (some val✝) = some a✝

Tactic:
<;>

Goal state after:
case none
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
a✝ : α
⊢ Option.rec none some none = some a✝ ↔ id none = some a✝

case some
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
val✝ a✝ : α
⊢ Option.rec none some (some val✝) = some a✝ ↔ id (some val✝) = some a✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
⊢ take 0 nil = []

pp: case succ
α : Type u
n✝ : ℕ
⊢ take (n✝ + 1) nil = []

Tactic:
<;>

Goal state after:
case zero
α : Type u
⊢ take 0 nil = []

case succ
α : Type u
n✝ : ℕ
⊢ take (n✝ + 1) nil = []