awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : Seq1 α
T : Seq (Seq1 α)
cons :
  ∀ (a : α) (s : Seq α),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons (a, s) T).join.destruct,
      (Seq.cons (a, s) T).join.destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
          s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons s T).join.destruct,
    (Seq.cons s T).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
obtain ⟨a, s⟩ := s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
cons :
  ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append T.join = s_1.append (S.append T_2).join ∧ s.append T.join = s_1.append (S.join.append T_2.join)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons (a, s) T).join.destruct,
    (Seq.cons (a, s) T).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
simp only [join_cons, destruct_cons, true_and]

Premises used: Stream'.Seq.join_cons, Stream'.Seq.destruct_cons, true_and
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append T.join = s_1.append (S.append T_2).join ∧ s.append T.join = s_1.append (S.join.append T_2.join)

Tactic:
⟨s, nil, T, ?_, ?_⟩

Premises used: Stream'.Seq.nil, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
cons : s.append T.join = s.append (append nil T).join
cons₁ : s.append T.join = s.append (append (join nil) T.join)
⊢ ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append T.join = s_1.append (S.append T_2).join ∧ s.append T.join = s_1.append (S.join.append T_2.join)

Tactic:
refine ⟨s, nil, T, ?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
⊢ s.append T.join = s.append (append nil T).join

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
⊢ s.append T.join = s.append (append (join nil) T.join)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
nil :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) destruct (join Seq.nil), destruct (join Seq.nil) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False
cons :
  ∀ (s : Seq1 α) (T : Seq (Seq1 α)),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons s T).join.destruct,
      (Seq.cons s T).join.destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
          s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) T.join.destruct, T.join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
cases T with
            | nil => simp
            | cons s T =>
              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
              refine ⟨s, nil, T, ?_, ?_⟩ <;> simp

Premises used: Stream'.Seq.nil, Stream'.Seq.join_cons, Stream'.Seq.cons, Stream'.Seq.destruct_cons, true_and
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) T.join.destruct, T.join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
case nil =>
            cases T with
            | nil => simp
            | cons s T =>
              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
              refine ⟨s, nil, T, ?_, ?_⟩ <;> simp

Premises used: Stream'.Seq.nil, Stream'.Seq.join_cons, Stream'.Seq.cons, Stream'.Seq.destruct_cons, true_and
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
s : Seq1 α
S : Seq (Seq1 α)
obtain :
  ∀ (a : α) (s : Seq α),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons (a, s) (S.append T)).join.destruct,
      ((cons (a, s) S).join.append T.join).destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
          s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons s (S.append T)).join.destruct,
    ((cons s S).join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
obtain ⟨a, s⟩ := s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : Seq (Seq1 α)
a : α
s : Seq α
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (cons (a, s) (S.append T)).join.destruct,
    ((cons (a, s) S).join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (S.append T).join.destruct,
    (S.join.append T.join).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s = s_1.append (S.append T).join ∧ s' = s_1.append (S.join.append T.join)
  | x, x_1 => False

Tactic:
case nil =>
          cases S <;> simp
          case nil =>
            cases T with
            | nil => simp
            | cons s T =>
              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
              refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
          case cons s S =>
            obtain ⟨a, s⟩ := s
            simpa using ⟨s, S, T, rfl, rfl⟩

Premises used: Stream'.Seq.nil, Stream'.Seq.join_cons, Stream'.Seq.cons, Stream'.Seq.destruct_cons, true_and
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
x : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (S_2 : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append (S.append T).join = s_1.append (S_2.append T_2).join ∧
      s.append (S.join.append T.join) = s_1.append (S_2.join.append T_2.join)

Tactic:
⟨s, S, T, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S_1 T_1 : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
x : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (S_2 : Seq (Seq1 α)) (T_2 : Seq (Seq1 α)),
    s.append (S.append T).join = s_1.append (S_2.append T_2).join ∧
      s.append (S.join.append T.join) = s_1.append (S_2.join.append T_2.join)

Tactic:
exact ⟨s, S, T, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
s1 s2 : Seq α
h :
  ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (S : Seq (Seq1 α)) (T : Seq (Seq1 α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    s1.destruct s2.destruct

Tactic:
exact
      match s1, s2, h with
      | _, _, ⟨s, S, T, rfl, rfl⟩ => by
        cases s <;> simp
        case nil =>
          cases S <;> simp
          case nil =>
            cases T with
            | nil => simp
            | cons s T =>
              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
              refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
          case cons s S =>
            obtain ⟨a, s⟩ := s
            simpa using ⟨s, S, T, rfl, rfl⟩
        case cons _ s => exact ⟨s, S, T, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
⊢ ∃ (s : Seq α) (S_1 : Seq (Seq1 α)) (T_1 : Seq (Seq1 α)),
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)

Tactic:
⟨nil, S, T, ?_, ?_⟩

Premises used: Stream'.Seq.nil, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
r : (S.append T).join = append nil (S.append T).join
r₁ : S.join.append T.join = append nil (S.join.append T.join)
⊢ ∃ (s : Seq α) (S_1 : Seq (Seq1 α)) (T_1 : Seq (Seq1 α)),
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)

Tactic:
refine ⟨nil, S, T, ?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = append nil (S.append T).join

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
S T : Seq (Seq1 α)
⊢ S.join.append T.join = append nil (S.join.append T.join)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
m : ℕ
⊢ (s.drop 0).get? m = s.get? (0 + m)

Tactic:
simp [drop]

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
succ : (s.drop k).get? (m + 1) = s.get? (k + 1 + m)
⊢ (s.drop (k + 1)).get? m = s.get? (k + 1 + m)

Tactic:
simp only [drop, get?_tail]

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop k).get? (m + 1) = s.get? (k + (m + 1))

Tactic:
ih
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
h : k + 1 + m = k + (m + 1)
⊢ (s.drop k).get? (m + 1) = s.get? (k + 1 + m)

Tactic:
convert! ih using 2
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ k + 1 + m = k + (m + 1)

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n m : ℕ
s : Seq α
zero : ∀ {m : ℕ}, (s.drop 0).get? m = s.get? (0 + m)
succ :
  ∀ (k : ℕ) (ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)) {m : ℕ}, (s.drop (k + 1)).get? m = s.get? (k + 1 + m)
⊢ (s.drop n).get? m = s.get? (n + m)

Tactic:
induction n generalizing m with
  | zero => simp [drop]
  | succ k ih =>
    simp only [drop, get?_tail]
    convert! ih using 2
    lia

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
rw : s.tail.drop n = s.drop (1 + n)
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
rw [Nat.add_comm]

Premises used: Nat.add_comm
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
symm : s.drop (1 + n) = s.tail.drop n
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
symm
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Tactic:
apply dropn_add

Premises used: Stream'.Seq.dropn_add
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ (s.drop 0).head = s.get? 0

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
succ : (s.tail.drop n).head = s.tail.get? n
⊢ (s.drop (n + 1)).head = s.get? (n + 1)

Tactic:
rw [← get?_tail, ← dropn_tail]

Premises used: Stream'.Seq.dropn_tail, Stream'.Seq.get?_tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n

Tactic:
apply IH
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
zero : ∀ (s : Seq α), (s.drop 0).head = s.get? 0
succ : ∀ (n : ℕ) (IH : ∀ (s : Seq α), (s.drop n).head = s.get? n) (s : Seq α), (s.drop (n + 1)).head = s.get? (n + 1)
⊢ (s.drop n).head = s.get? n

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n IH => rw [← get?_tail, ← dropn_tail]; apply IH

Premises used: Stream'.Seq.dropn_tail, Stream'.Seq.get?_tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ s.drop 0 = s

Tactic:
rfl

Premises used: Stream'.Seq.drop, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
⊢ (cons x s).drop (n + 1) = s.drop n

Tactic:
simp [← dropn_tail]

Premises used: Stream'.Seq.dropn_tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Seq α) (drop nil 0) nil

Tactic:
simp [drop]

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
m : ℕ
ih : Eq.{u + 1} (α := Seq α) (drop nil m) nil
⊢ Eq.{u + 1} (α := Seq α) (drop nil (m + 1)) nil

Tactic:
simp [← dropn_tail, ih]

Premises used: Stream'.Seq.dropn_tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
zero : Eq.{u + 1} (α := Seq α) (drop nil 0) nil
succ : ∀ (m : ℕ) (ih : Eq.{u + 1} (α := Seq α) (drop nil m) nil), Eq.{u + 1} (α := Seq α) (drop nil (m + 1)) nil
⊢ Eq.{u + 1} (α := Seq α) (drop nil n) nil

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

Premises used: Stream'.Seq.dropn_tail, Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ (s.drop 0).length' = s.length' - (↑0 : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
⊢ length'.{u} (α := α) (drop nil (n + 1)) = length'.{u} (α := α) nil - (↑(n + 1) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
succ : (s.drop n).length' = s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ ((cons x s).drop (n + 1)).length' = (cons x s).length' - (↑(n + 1) : ℕ∞)

Tactic:
simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]

Premises used: Stream'.Seq.drop_succ_cons, Stream'.Seq.length'_cons, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
⊢ (s.drop n).length' = s.length' - (↑n : ℕ∞)

Tactic:
drop_length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
h : s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = s.length' - (↑n : ℕ∞)
⊢ (s.drop n).length' = s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
convert! drop_length' using 1
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
h : ∀ (m : ℕ∞), m + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = m - (↑n : ℕ∞)
⊢ s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = s.length' - (↑n : ℕ∞)

Tactic:
generalize s.length' = m

Premises used: Stream'.Seq.length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
m : ℕ∞
h : ∀ (m : ℕ), m + 1 - (n + 1) = m - n
⊢ m + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = m - (↑n : ℕ∞)

Tactic:
enat_to_nat
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
m : ℕ
⊢ m + 1 - (n + 1) = m - n

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
succ : length'.{u} (α := α) (drop nil (n + 1)) = length'.{u} (α := α) nil - (↑(n + 1) : ℕ∞)
succ₁ : ∀ (x : α) (s : Seq α), ((cons x s).drop (n + 1)).length' = (cons x s).length' - (↑(n + 1) : ℕ∞)
⊢ (s.drop (n + 1)).length' = s.length' - (↑(n + 1) : ℕ∞)

Tactic:
cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia

Premises used: Stream'.Seq.length', Stream'.Seq.drop_succ_cons, Stream'.Seq.length'_cons, Stream'.Seq.nil, Nat.cast_add, Stream'.Seq.cons, Nat.cast_one
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
s : Seq α
zero : (s.drop 0).length' = s.length' - (↑0 : ℕ∞)
succ : ∀ (n : ℕ), (s.drop (n + 1)).length' = s.length' - (↑(n + 1) : ℕ∞)
⊢ (s.drop n).length' = s.length' - (↑n : ℕ∞)

Tactic:
cases n with
  | zero => simp
  | succ n =>
    cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia

Premises used: Stream'.Seq.length', Stream'.Seq.drop_succ_cons, Stream'.Seq.length'_cons, Stream'.Seq.nil, Nat.cast_add, Stream'.Seq.cons, Nat.cast_one
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n m : ℕ
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.drop m (take n s)) i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - m) (s.drop m)) i = some a
⊢ List.drop m (take n s) = take (n - m) (s.drop m)

Tactic:
ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n m i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.drop m (take n s)) i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - m) (s.drop m)) i = some a

Tactic:
grind
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
s' : Seq β
n : ℕ
⊢ (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n)

Tactic:
rfl

Premises used: rfl, Stream'.Seq.get?, Option.map₂
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
t : Seq β
n : ℕ
⊢ (s.zip t).get? n = Option.map₂ Prod.mk (s.get? n) (t.get? n)

Tactic:
get?_zipWith _ _ _ _

Premises used: Stream'.Seq.get?_zipWith, Stream'.Seq.zip
-- Module: Mathlib.Data.Seq.Basic
Goal:
n : ℕ
⊢ nats.get? n = some n

Tactic:
rfl

Premises used: Stream'.nats, Stream'.get, Stream'.map, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.enum.get? n = Option.map (Prod.mk n) (s.get? n)

Tactic:
get?_zip _ _ _

Premises used: Stream'.Seq.enum, Stream'.Seq.get?_zip, Stream'.nats, Stream'.get, Option.map₂
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq β
⊢ zipWith f nil s = nil

Tactic:
rfl

Premises used: Stream'.Seq.zipWith, Stream'.Seq.nil, rfl, Option.map₂
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
h : ∀ (n : ℕ), (zipWith f s nil).get? n = get? nil n
⊢ zipWith f s nil = nil

Tactic:
ext1
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
n : ℕ
⊢ (zipWith f s nil).get? n = get? nil n

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
h : ∀ (n : ℕ), (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n
⊢ zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s')

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
h : (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0
h₁ : ∀ (n : ℕ), (zipWith f (cons x s) (cons x' s')).get? (n + 1) = (cons (f x x') (zipWith f s s')).get? (n + 1)
⊢ (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n

Tactic:
cases n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? (n + 1) = (cons (f x x') (zipWith f s s')).get? (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ Eq (α := Seq (α × α)) (zip nil s) nil

Tactic:
rfl

Premises used: Stream'.Seq.zipWith, Stream'.Seq.nil, rfl, Option.map₂, Stream'.Seq.zip
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ Eq (α := Seq (α × α)) (s.zip nil) nil

Tactic:
zipWith_nil_right

Premises used: Stream'.Seq.zipWith_nil_right, Stream'.Seq.zip
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s s' : Seq α
x x' : α
⊢ (cons x s).zip (cons x' s') = cons (x, x') (s.zip s')

Tactic:
zipWith_cons_cons

Premises used: Stream'.Seq.zipWith_cons_cons, Stream'.Seq.zip
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Seq (ℕ × α)) (enum nil) nil

Tactic:
rfl

Premises used: Stream'.Seq.zipWith, Stream'.Seq.enum, Stream'.Seq.nil, rfl, Option.map₂, Stream'.Seq.zip
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
x : α
h : (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0
h₁ : ∀ (n : ℕ), (cons x s).enum.get? (n + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n + 1)
⊢ (cons x s).enum = cons (0, x) (map (Prod.map Nat.succ id) s.enum)

Tactic:
ext ⟨n⟩ : 1
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
x : α
n : ℕ
h : Option.map (Prod.mk (n + 1)) (s.get? n) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n) (s.get? n)
⊢ (cons x s).enum.get? (n + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n + 1)

Tactic:
simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]

Premises used: Stream'.Seq.get?_enum, Stream'.Seq.get?_cons_succ, Option.map_map, Stream'.Seq.map_get?