awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
n : ℕ
x y : α
hx : s.get? n = some x
hy : s.get? (n + 1) = some y
⊢ (s.drop n).head = some x

Tactic:
rw [← head_dropn] at hx

Premises used: Stream'.Seq.head_dropn
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
n : ℕ
x y : α
hx : s.get? n = some x
hy : s.get? (n + 1) = some y
hx₁ : (s.drop n).head = some x
⊢ s.get? (n + 1) = some y

Tactic:
rw [← head_dropn] at hx

Premises used: Stream'.Seq.head_dropn
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
n : ℕ
x y : α
hx : (s.drop n).head = some x
hy : s.get? (n + 1) = some y
have : ∀ (this : ∀ (n : ℕ), motive (s.drop n)), R x y
⊢ R x y

Tactic:
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right)
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
n : ℕ
x y : α
hx : (s.drop n).head = some x
hy : s.get? (n + 1) = some y
this : ∀ (n : ℕ), motive (s.drop n)
⊢ y ∈ (s.drop (n + 1)).head

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
n : ℕ
x y : α
hx : (s.drop n).head = some x
hy : s.get? (n + 1) = some y
this : ∀ (n : ℕ), motive (s.drop n)
⊢ R x y

Tactic:
exact (step x (s.drop (n + 1)) (head_eq_some hx ▸ this n)).left _ (by simpa)

Premises used: Stream'.Seq.drop, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
⊢ ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y

Tactic:
have h_succ {n} {x y} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y) : R x y := by
    rw [← head_dropn] at hx
    have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right)
    exact (step x (s.drop (n + 1)) (head_eq_some hx ▸ this n)).left _ (by simpa)
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
y : α
hy : y ∈ s.get? j
obtain : ∀ (k : ℕ) (h_ij : i < i + k + 1) (hy : y ∈ s.get? (i + k + 1)), R x y
⊢ R x y

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h_ij

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
y : α
hy : y ∈ s.get? (i + 0 + 1)
⊢ R x y

Tactic:
h_succ hx hy
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
y : α
hy : y ∈ s.get? (i + 0 + 1)
⊢ R x y

Tactic:
exact h_succ hx hy
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
k : ℕ
ih : ∀ (y : α) (hy : y ∈ s.get? (i + k + 1)), R x y
y : α
hy : y ∈ s.get? (i + (k + 1) + 1)
⊢ i + k + 1 ≤ i + (k + 1) + 1

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
k : ℕ
ih : ∀ (y : α) (hy : y ∈ s.get? (i + k + 1)), R x y
y : α
hy : y ∈ s.get? (i + (k + 1) + 1)
succ : ∀ (z : α) (hz : s.get? (i + k + 1) = some z), R x y
⊢ R x y

Tactic:
obtain ⟨z, hz⟩ := ge_stable (m := i + k + 1) _ (by lia) hy

Premises used: Stream'.Seq.ge_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
k : ℕ
ih : ∀ (y : α) (hy : y ∈ s.get? (i + k + 1)), R x y
y : α
hy : y ∈ s.get? (i + (k + 1) + 1)
z : α
hz : s.get? (i + k + 1) = some z
⊢ R x y

Tactic:
_root_.trans (ih z hz) <| h_succ hz hy

Premises used: trans
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
k : ℕ
ih : ∀ (y : α) (hy : y ∈ s.get? (i + k + 1)), R x y
y : α
hy : y ∈ s.get? (i + (k + 1) + 1)
z : α
hz : s.get? (i + k + 1) = some z
⊢ R x y

Tactic:
exact _root_.trans (ih z hz) <| h_succ hz hy

Premises used: trans
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y), R x y
i : ℕ
x : α
hx : x ∈ s.get? i
y : α
k : ℕ
hy : y ∈ s.get? (i + k + 1)
zero : ∀ (y : α) (hy : y ∈ s.get? (i + 0 + 1)), R x y
succ :
  ∀ (k : ℕ) (ih : ∀ (y : α) (hy : y ∈ s.get? (i + k + 1)), R x y) (y : α) (hy : y ∈ s.get? (i + (k + 1) + 1)), R x y
⊢ R x y

Tactic:
induction k generalizing y with
  | zero => exact h_succ hx hy
  | succ k ih =>
    obtain ⟨z, hz⟩ := ge_stable (m := i + k + 1) _ (by lia) hy
    exact _root_.trans (ih z hz) <| h_succ hz hy

Premises used: Stream'.Seq.ge_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
nil : ∀ (h : Pairwise R Seq.nil), Pairwise R (tail Seq.nil)
cons : ∀ (x : α) (s : Seq α) (h : Pairwise R (Seq.cons x s)), Pairwise R (Seq.cons x s).tail
⊢ Pairwise R s.tail

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
h : Pairwise R nil
⊢ Pairwise R (tail nil)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
x : α
s : Seq α
h : Pairwise R (cons x s)
⊢ Pairwise R (cons x s).tail

Tactic:
simp [h.cons_elim.right]

Premises used: And.right, Stream'.Seq.Pairwise.cons_elim
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
⊢ Pairwise R (s.drop 0)

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
m : ℕ
ih : Pairwise R (s.drop m)
⊢ Pairwise R (s.drop (m + 1))

Tactic:
simp [drop, Pairwise_tail ih]

Premises used: Stream'.Seq.drop, Stream'.Seq.Pairwise_tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
n : ℕ
zero : Pairwise R (s.drop 0)
succ : ∀ (m : ℕ) (ih : Pairwise R (s.drop m)), Pairwise R (s.drop (m + 1))
⊢ Pairwise R (s.drop n)

Tactic:
induction n with
  | zero => simpa
  | succ m ih => simp [drop, Pairwise_tail ih]

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
hb : b.drop 0 ≠ nil
⊢ motive (a.drop 0) (b.drop 0)

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
ih : ∀ (hb : b.drop m ≠ nil), motive (a.drop m) (b.drop m)
hb : b.drop (m + 1) ≠ nil
succ : motive (a.drop m).tail (b.drop m).tail
⊢ motive (a.drop (m + 1)) (b.drop (m + 1))

Tactic:
simp only [drop] at hb ⊢

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
ih : ∀ (hb : b.drop m ≠ nil), motive (a.drop m) (b.drop m)
hb : (b.drop m).tail ≠ nil
succ :
  ∀ (tb : Seq β) (ih : ∀ (hb : tb ≠ nil), motive (a.drop m) tb) (hb : tb.tail ≠ nil), motive (a.drop m).tail tb.tail
⊢ motive (a.drop m).tail (b.drop m).tail

Tactic:
generalize b.drop m = tb at *

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
ih : ∀ (hb : Ne.{v + 1} (α := Seq β) nil nil), motive (a.drop m) nil
hb : Ne.{v + 1} (α := Seq β) (tail nil) nil
⊢ motive (a.drop m).tail (tail nil)

Tactic:
simp at hb
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb_hd : β
tb_tl : Seq β
ih : ∀ (hb : cons tb_hd tb_tl ≠ nil), motive (a.drop m) (cons tb_hd tb_tl)
hb : (cons tb_hd tb_tl).tail ≠ nil
⊢ motive (a.drop m) (cons tb_hd tb_tl)

Tactic:
simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih

Premises used: Stream'.Seq.cons_ne_nil, ne_eq, forall_const, not_false_eq_true
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb_hd : β
tb_tl : Seq β
hb : (cons tb_hd tb_tl).tail ≠ nil
ih : motive (a.drop m) (cons tb_hd tb_tl)
succ :
  ∀ (a_hd : α) (a_tl : Seq α) (ha : a.drop m = cons a_hd a_tl) (h_tail : motive a_tl tb_tl),
    motive (a.drop m).tail (cons tb_hd tb_tl).tail
⊢ motive (a.drop m).tail (cons tb_hd tb_tl).tail

Tactic:
obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl

Premises used: Stream'.Seq.drop, Stream'.Seq.cons, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb_hd : β
tb_tl : Seq β
hb : (cons tb_hd tb_tl).tail ≠ nil
ih : motive (a.drop m) (cons tb_hd tb_tl)
a_hd : α
a_tl : Seq α
ha : a.drop m = cons a_hd a_tl
h_tail : motive a_tl tb_tl
⊢ motive (a.drop m).tail (cons tb_hd tb_tl).tail

Tactic:
simpa [ha]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb : Seq β
ih : ∀ (hb : tb ≠ nil), motive (a.drop m) tb
hb : tb.tail ≠ nil
succ :
  ∀ (ih : ∀ (hb : Ne.{v + 1} (α := Seq β) nil nil), motive (a.drop m) nil)
    (hb : Ne.{v + 1} (α := Seq β) (tail nil) nil), motive (a.drop m).tail (tail nil)
succ₁ :
  ∀ (tb_hd : β) (tb_tl : Seq β) (ih : ∀ (hb : cons tb_hd tb_tl ≠ nil), motive (a.drop m) (cons tb_hd tb_tl))
    (hb : (cons tb_hd tb_tl).tail ≠ nil), motive (a.drop m).tail (cons tb_hd tb_tl).tail
⊢ motive (a.drop m).tail tb.tail

Tactic:
cases tb with
      | nil => simp at hb
      | cons tb_hd tb_tl =>
        simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih
        obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl
        simpa [ha]

Premises used: Stream'.Seq.cons_ne_nil, ne_eq, Stream'.Seq.nil, Stream'.Seq.cons, forall_const, not_false_eq_true
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
n : ℕ
hb : b.drop n ≠ nil
zero : ∀ (hb : b.drop 0 ≠ nil), motive (a.drop 0) (b.drop 0)
succ :
  ∀ (m : ℕ) (ih : ∀ (hb : b.drop m ≠ nil), motive (a.drop m) (b.drop m)) (hb : b.drop (m + 1) ≠ nil),
    motive (a.drop (m + 1)) (b.drop (m + 1))
⊢ motive (a.drop n) (b.drop n)

Tactic:
induction n with
    | zero => simpa
    | succ m ih =>
      simp only [drop] at hb ⊢
      generalize b.drop m = tb at *
      cases tb with
      | nil => simp at hb
      | cons tb_hd tb_tl =>
        simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih
        obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl
        simpa [ha]

Premises used: Stream'.Seq.drop, Stream'.Seq.cons_ne_nil, ne_eq, Stream'.Seq.nil, Stream'.Seq.cons, forall_const, not_false_eq_true
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
⊢ ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)

Tactic:
have (n) (hb : b.drop n ≠ .nil) : motive (a.drop n) (b.drop n) := by
    induction n with
    | zero => simpa
    | succ m ih =>
      simp only [drop] at hb ⊢
      generalize b.drop m = tb at *
      cases tb with
      | nil => simp at hb
      | cons tb_hd tb_tl =>
        simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih
        obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl
        simpa [ha]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
pos : ∀ (ha : a.Terminates), b.length' ≤ a.length'
neg : ∀ (ha : ¬a.Terminates), b.length' ≤ a.length'
⊢ b.length' ≤ a.length'

Tactic:
by_cases ha : a.Terminates

Premises used: Stream'.Seq.Terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : ¬a.Terminates
⊢ b.length' ≤ a.length'

Tactic:
simp [length'_of_not_terminates ha]

Premises used: Stream'.Seq.length'_of_not_terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : a.Terminates
pos : b.TerminatedAt (a.length ha)
⊢ b.length' ≤ a.length'

Tactic:
simp only [length'_of_terminates ha, length'_le_iff]

Premises used: Stream'.Seq.length'_of_terminates, Stream'.Seq.length'_le_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : a.Terminates
pos : ∀ (hb : ¬b.TerminatedAt (a.length ha)), False
⊢ b.TerminatedAt (a.length ha)

Tactic:
by_contra hb
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb' : b.drop (a.length ha) = nil
⊢ b.TerminatedAt (a.length ha)

Tactic:
simp only [← length'_eq_zero_iff_nil, drop_length', tsub_eq_zero_iff_le, length'_le_iff] at hb'

Premises used: Stream'.Seq.length'_le_iff, Stream'.Seq.drop_length', tsub_eq_zero_iff_le, Stream'.Seq.length'_eq_zero_iff_nil
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb' : b.TerminatedAt (a.length ha)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
⊢ b.drop (a.length ha) ≠ nil

Tactic:
have hb_cons : b.drop (a.length ha) ≠ .nil := by
    intro hb'
    simp only [← length'_eq_zero_iff_nil, drop_length', tsub_eq_zero_iff_le, length'_le_iff] at hb'
    contradiction
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ) (hb : b.drop n ≠ nil), motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : b.drop (a.length ha) ≠ nil
⊢ motive (a.drop (a.length ha)) (b.drop (a.length ha))

Tactic:
specialize this (a.length ha) hb_cons

Premises used: Stream'.Seq.length
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : b.drop (a.length ha) ≠ nil
this : motive (a.drop (a.length ha)) (b.drop (a.length ha))
pos : ∀ (b' : Seq β) (hb_cons : b' ≠ nil) (this : motive (a.drop (a.length ha)) b'), False
⊢ False

Tactic:
generalize b.drop (a.length ha) = b' at *

Premises used: Stream'.Seq.drop, Stream'.Seq.length
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : Ne.{v + 1} (α := Seq β) nil nil
this : motive (a.drop (a.length ha)) nil
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
hb_cons : cons b_hd b_tl ≠ nil
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
pos : ∀ (a_hd : α) (a_tl : Seq α) (ha' : a.drop (a.length ha) = cons a_hd a_tl), motive a_tl b_tl → False
⊢ False

Tactic:
obtain ⟨a_hd, a_tl, ha', _⟩ := step _ _ this _ _ rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
hb_cons : cons b_hd b_tl ≠ nil
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
a_hd : α
a_tl : Seq α
ha' : a.drop (a.length ha) = cons a_hd a_tl
right : motive a_tl b_tl
⊢ (a.drop (a.length ha)).length' = (cons a_hd a_tl).length'

Tactic:
apply_fun length' at ha'

Premises used: Stream'.Seq.length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b →
      ∀ (b_hd : β) (b_tl : Seq β),
        b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
hb_cons : cons b_hd b_tl ≠ nil
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
a_hd : α
a_tl : Seq α
right : motive a_tl b_tl
ha' : (a.drop (a.length ha)).length' = (cons a_hd a_tl).length'
⊢ 0 = a_tl.length' + 1

Tactic:
simp only [drop_length', length'_of_terminates ha, tsub_self, length'_cons] at ha'

Premises used: Stream'.Seq.length'_of_terminates, tsub_self, Stream'.Seq.length'_cons, Stream'.Seq.drop_length'